ProCGroups/TopologicalGroups.lean
1import Mathlib.CategoryTheory.ConcreteCategory.Basic
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ProCGroups/TopologicalGroups.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# ProCGroups / TopologicalGroups / Category
15Focused module in the public source tree. It contains declarations used by the library roots and by downstream proof modules.
16-/
18open CategoryTheory
19open scoped Topology
21universe u
23/-- Bundled topological groups with continuous homomorphisms. -/
24@[pp_with_univ]
26 carrier : Type u
27 [group : Group carrier]
28 [topologicalSpace : TopologicalSpace carrier]
29 [isTopologicalGroup : IsTopologicalGroup carrier]
31attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
36 coe G := G.carrier
38/-- Bundle an unbundled topological group. -/
40 carrier := G
42/-- Morphisms of topological groups are continuous homomorphisms. -/
43@[ext]
44structure Hom (G H : TopGrp.{u}) where
45 hom' : G →ₜ* H
48 Hom G H := Hom G H
49 id G := ⟨ContinuousMonoidHom.id G⟩
50 comp f g := ⟨g.hom'.comp f.hom'⟩
53 hom f := f.hom'
54 ofHom f := ⟨f⟩
56/-- The underlying continuous homomorphism of a morphism. -/
57abbrev Hom.hom {G H : TopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
60instance instCoeFunHom {G H : TopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
61 coe f := f.hom
63@[simp] theorem hom_id {G : TopGrp.{u}} :
64 (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G :=
65 rfl
67@[simp] theorem hom_comp {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
68 (f ≫ g).hom = g.hom.comp f.hom :=
69 rfl
71@[simp] theorem comp_apply {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
72 (f ≫ g) x = g (f x) :=
73 rfl
75/-- Morphisms of topological groups are extensional in their underlying continuous homomorphism. -/
76@[ext] theorem hom_ext {G H : TopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
77 f = g :=
78 Hom.ext h
80/-- Typecheck a continuous homomorphism as a bundled topological-group morphism. -/
81abbrev ofHom {G H : Type u}
82 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
83 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
84 (f : G →ₜ* H) : of G ⟶ of H :=
85 ConcreteCategory.ofHom f
89/-- Bundled commutative topological groups with continuous homomorphisms. -/
90@[pp_with_univ]
91structure CommTopGrp where
92 carrier : Type u
93 [commGroup : CommGroup carrier]
94 [topologicalSpace : TopologicalSpace carrier]
95 [isTopologicalGroup : IsTopologicalGroup carrier]
97attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
98 CommTopGrp.isTopologicalGroup
100namespace CommTopGrp
102instance instCoeSort : CoeSort CommTopGrp (Type u) where
103 coe G := G.carrier
105/-- Bundle an unbundled commutative topological group. -/
106abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] :
107 CommTopGrp where
108 carrier := G
110/-- Morphisms of commutative topological groups are continuous homomorphisms. -/
111@[ext]
112structure Hom (G H : CommTopGrp.{u}) where
113 hom' : G →ₜ* H
115instance instCategory : Category CommTopGrp where
116 Hom G H := Hom G H
117 id G := ⟨ContinuousMonoidHom.id G⟩
118 comp f g := ⟨g.hom'.comp f.hom'⟩
120instance instConcreteCategory : ConcreteCategory CommTopGrp (fun G H => G →ₜ* H) where
121 hom f := f.hom'
122 ofHom f := ⟨f⟩
124/-- The underlying continuous homomorphism of a morphism. -/
125abbrev Hom.hom {G H : CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
126 ConcreteCategory.hom (C := CommTopGrp) f
128instance instCoeFunHom {G H : CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
129 coe f := f.hom
131@[simp] theorem hom_id {G : CommTopGrp.{u}} :
132 (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G :=
133 rfl
135@[simp] theorem hom_comp {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
136 (f ≫ g).hom = g.hom.comp f.hom :=
137 rfl
139@[simp] theorem comp_apply {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
140 (f ≫ g) x = g (f x) :=
141 rfl
143/-- Morphisms of commutative topological groups are extensional in their underlying continuous
144homomorphism. -/
145@[ext] theorem hom_ext {G H : CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
146 f = g :=
147 Hom.ext h
149/-- Typecheck a continuous homomorphism as a bundled commutative topological-group morphism. -/
150abbrev ofHom {G H : Type u}
151 [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
152 [CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H]
153 (f : G →ₜ* H) : of G ⟶ of H :=
154 ConcreteCategory.ofHom f
156end CommTopGrp
158/-- Forget the commutativity of a bundled commutative topological group. -/
159def commTopGrpForgetToTopGrp : CommTopGrp.{u} ⥤ TopGrp.{u} where
161 map f := TopGrp.ofHom f.hom
162 map_id G := by
163 apply TopGrp.hom_ext
164 rfl
165 map_comp f g := by
166 apply TopGrp.hom_ext
167 rfl