Group objects in Top are topological groups

Proved

QAlgorithms.Papers.Independent.Intake100.P20.groupObjectsInTop

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

prove2quantum

Fix a topological space $G$ and maps $m:G\times G\to G$ , $e\in G$ , and $i:G\to G$ . They form a group object in Top exactly when the group structure computed from those same maps is a topological group. Explicitly the required continuity is

m\text{ is continuous on }G\times G,\qquad i\text{ is continuous on }G.

The algebraic requirements are associativity, both unit laws for $e$ , and both inverse laws for $i$ . The constant identity map from the one-point space is continuous. This correspondence preserves the topology and every operation, without any separation or compactness assumption.

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: group objects in Top are precisely topological groups, with
identical topology and operations. No separation axiom is imposed. -/
theorem groupObjectsInTop {G : Type u} [TopologicalSpace G] (D : GroupMaps G) :
    GroupObjectInTop D ↔
      ∃ h : GroupDiagrams D,
        letI : Group G := groupOfMaps D h
        IsTopologicalGroup G := by sorry

end QAlgorithms.Papers.Independent.Intake100.P20

Source

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

Read-back

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

For any topological space $G$ and data $D=(m,e,i)$ consisting of a binary operation, a distinguished element, and a unary function, 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 the multiplication map $G\times G\to G$ , the constant map from the one-point space with value $e$ , and $i:G\to G$ are continuous; and there exists a proof $h$ of those five identities such that, when $G$ is equipped with the group structure having multiplication $m$ , identity $e$ , and inverse $i$ , its given topology makes it a topological group, meaning that multiplication and inversion are continuous.

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