Smooth group objects are Lie groups

Proved

QAlgorithms.Papers.Independent.Intake100.P20.groupObjectsInSmoothManifolds

by Gohan · Oct 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G$ be an ordinary finite-dimensional real smooth manifold without boundary, using the Hausdorff and second countable convention, modeled on a finite-dimensional real normed vector space $E$ . Fix multiplication $m$ , identity $e$ , and inverse $i$ . These maps define a group object in smooth manifolds if and only if their computed group structure is a Lie group on the same manifold:

\text{group diagrams and smooth }m,i\quad\Longleftrightarrow\quad G\text{ is a }C^\infty\text{ Lie group with those operations}.

The identity map from the point manifold is automatically smooth. Dimension zero and the one-point group are included. The statement expresses the source's ordinary smooth-manifold correspondence and makes no claim about general locally convex Lie groups.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intake100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intake100.P20

open CategoryTheory

open scoped TensorProduct Manifold ContDiff

universe u v w z

/-- PDF p. 3, footnote 3: group objects in ordinary differentiable manifolds
are Lie groups. Both sides use the SAME finite-dimensional real smooth manifold
without boundary, with the usual Hausdorff and second countable conventions.
Dimension zero is included. -/
theorem groupObjectsInSmoothManifolds
    {E : Type v} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {G : Type u} [TopologicalSpace G] [T2Space G] [SecondCountableTopology G]
    [ChartedSpace E G] [IsManifold (𝓘(ℝ, E)) ∞ G] (D : GroupMaps G) :
    SmoothGroupObject (E := E) D ↔
      ∃ h : GroupDiagrams D,
        letI : Group G := groupOfMaps D h
        LieGroup (𝓘(ℝ, E)) ∞ G := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20

Source

Group Objects and Internal Categories, arXiv:math/0212065v1, PDF p. 3, §1 and footnote 3

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $E$ be a normed additive commutative group equipped with a finite-dimensional real normed vector space structure, including the possibility $\dim_{\mathbb R}E=0$ . Let $G$ be a Hausdorff, second-countable topological space with a charted space structure modeled on $E$ , and assume that this structure makes $G$ a $C^\infty$ manifold for the identity model on $E$ . For every triple $D=(m,e,i)$ consisting of a binary operation, a distinguished element, and a unary function on $G$ , the following are equivalent: the identities $m(m(a,b),c)=m(a,m(b,c))$ for all $a,b,c\in G$ and $m(e,a)=a$ , $m(a,e)=a$ , $m(i(a),a)=e$ , $m(a,i(a))=e$ for all $a\in G$ hold, and both $m:G\times G\to G$ and $i:G\to G$ are $C^\infty$ , using the product identity model for the domain of $m$ and the identity model on $E$ elsewhere; and there exists a proof $h$ of those five identities such that the group structure on $G$ with multiplication $m$ , identity $e$ , and inverse $i$ is a $C^\infty$ Lie group for the given manifold structure and identity model on $E$ .

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph