Source: ProCGroups.TopologicalGroups
1import Mathlib.CategoryTheory.ConcreteCategory.Basic
2import Mathlib.Topology.Algebra.ContinuousMonoidHom
4/-!
5# Pro C Groups / Topological Groups
7This module formalizes basic topological-group constructions used by the pro-\(C\) library.
8-/
10open CategoryTheory
11open scoped Topology
13universe u
15namespace ProCGroups
17/-- Bundled topological groups with continuous homomorphisms. -/
18@[pp_with_univ]
19structure TopGrp where
20 /-- The underlying type of the topological group. -/
21 carrier : Type u
22 /-- The group structure on the carrier. -/
23 [group : Group carrier]
24 /-- The topology on the carrier. -/
25 [topologicalSpace : TopologicalSpace carrier]
26 /-- Multiplication and inversion are continuous for the stored topology. -/
27 [isTopologicalGroup : IsTopologicalGroup carrier]
29attribute [instance] TopGrp.group TopGrp.topologicalSpace TopGrp.isTopologicalGroup
31namespace TopGrp
33/-- The category object coerces to its underlying type. -/
34instance instCoeSort : CoeSort TopGrp (Type u) where
35 coe G := G.carrier
37/-- Bundle an unbundled topological group. -/
38abbrev of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : TopGrp where
39 carrier := G
41/-- Morphisms of topological groups are continuous homomorphisms. -/
42@[ext]
43structure Hom (G H : TopGrp.{u}) where
44 /-- The continuous group homomorphism underlying the bundled morphism. -/
45 hom' : G →ₜ* H
47/-- Topological groups form a category. -/
48instance instCategory : Category TopGrp where
49 Hom G H := Hom G H
50 id G := ⟨ContinuousMonoidHom.id G⟩
51 comp f g := ⟨g.hom'.comp f.hom'⟩
53/--
54The category of topological groups has the concrete category structure inherited from its
55underlying type.
56-/
57instance instConcreteCategory : ConcreteCategory TopGrp (fun G H => G →ₜ* H) where
58 hom f := f.hom'
59 ofHom f := ⟨f⟩
61/-- The underlying continuous homomorphism of a morphism. -/
62abbrev Hom.hom {G H : TopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
63 ConcreteCategory.hom (C := TopGrp) f
65/-- A morphism coerces to its underlying continuous homomorphism. -/
66instance instCoeFunHom {G H : TopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
67 coe f := f.hom
69/-- The underlying homomorphism of the identity morphism is the identity continuous homomorphism. -/
70@[simp] theorem hom_id {G : TopGrp.{u}} :
71 (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G :=
72 rfl
74/-- The underlying homomorphism of a composite is the composite of underlying homomorphisms. -/
75@[simp] theorem hom_comp {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
76 (f ≫ g).hom = g.hom.comp f.hom :=
77 rfl
79/--
80The composite map is computed pointwise by applying the constituent coordinate formulas in
81succession.
82-/
83@[simp] theorem comp_apply {G H K : TopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
84 (f ≫ g) x = g (f x) :=
85 rfl
87/-- Morphisms in TopGrp are equal when their underlying continuous homomorphisms are equal. -/
88@[ext] theorem hom_ext {G H : TopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
89 f = g :=
90 Hom.ext h
92/-- Bundle a continuous homomorphism as a topological-group morphism. -/
93abbrev ofHom {G H : Type u}
94 [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
95 [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
96 (f : G →ₜ* H) : of G ⟶ of H :=
97 ConcreteCategory.ofHom f
99end TopGrp
101/-- Bundled commutative topological groups with continuous homomorphisms. -/
102@[pp_with_univ]
103structure CommTopGrp where
104 /-- The underlying type of the commutative topological group. -/
105 carrier : Type u
106 /-- The commutative group structure on the carrier. -/
107 [commGroup : CommGroup carrier]
108 /-- The topology on the carrier. -/
109 [topologicalSpace : TopologicalSpace carrier]
110 /-- Multiplication and inversion are continuous for the stored topology. -/
111 [isTopologicalGroup : IsTopologicalGroup carrier]
113attribute [instance] CommTopGrp.commGroup CommTopGrp.topologicalSpace
114 CommTopGrp.isTopologicalGroup
116namespace CommTopGrp
118/-- The category object coerces to its underlying type. -/
119instance instCoeSort : CoeSort CommTopGrp (Type u) where
120 coe G := G.carrier
122/-- Bundle an unbundled commutative topological group. -/
123abbrev of (G : Type u) [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G] :
124 CommTopGrp where
125 carrier := G
127/-- Morphisms of commutative topological groups are continuous homomorphisms. -/
128@[ext]
129structure Hom (G H : CommTopGrp.{u}) where
130 /-- The continuous homomorphism underlying the bundled morphism. -/
131 hom' : G →ₜ* H
133/-- Commutative topological groups form a category. -/
134instance instCategory : Category CommTopGrp where
135 Hom G H := Hom G H
136 id G := ⟨ContinuousMonoidHom.id G⟩
137 comp f g := ⟨g.hom'.comp f.hom'⟩
139/--
140The category of commutative topological groups has the concrete category structure inherited
141from its underlying type.
142-/
143instance instConcreteCategory : ConcreteCategory CommTopGrp (fun G H => G →ₜ* H) where
144 hom f := f.hom'
145 ofHom f := ⟨f⟩
147/-- The underlying continuous homomorphism of a morphism. -/
148abbrev Hom.hom {G H : CommTopGrp.{u}} (f : G ⟶ H) : G →ₜ* H :=
149 ConcreteCategory.hom (C := CommTopGrp) f
151/-- A morphism coerces to its underlying continuous homomorphism. -/
152instance instCoeFunHom {G H : CommTopGrp.{u}} : CoeFun (G ⟶ H) (fun _ => G → H) where
153 coe f := f.hom
155/-- The underlying homomorphism of the identity morphism is the identity continuous homomorphism. -/
156@[simp] theorem hom_id {G : CommTopGrp.{u}} :
157 (𝟙 G : G ⟶ G).hom = ContinuousMonoidHom.id G :=
158 rfl
160/-- The underlying homomorphism of a composite is the composite of underlying homomorphisms. -/
161@[simp] theorem hom_comp {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) :
162 (f ≫ g).hom = g.hom.comp f.hom :=
163 rfl
165/--
166The composite map is computed pointwise by applying the constituent coordinate formulas in
167succession.
168-/
169@[simp] theorem comp_apply {G H K : CommTopGrp.{u}} (f : G ⟶ H) (g : H ⟶ K) (x : G) :
170 (f ≫ g) x = g (f x) :=
171 rfl
173/-- Morphisms in CommTopGrp are equal when their underlying continuous homomorphisms are equal. -/
174@[ext] theorem hom_ext {G H : CommTopGrp.{u}} {f g : G ⟶ H} (h : f.hom = g.hom) :
175 f = g :=
176 Hom.ext h
178/-- Bundle a continuous homomorphism as a commutative topological-group morphism. -/
179abbrev ofHom {G H : Type u}
180 [CommGroup G] [TopologicalSpace G] [IsTopologicalGroup G]
181 [CommGroup H] [TopologicalSpace H] [IsTopologicalGroup H]
182 (f : G →ₜ* H) : of G ⟶ of H :=
183 ConcreteCategory.ofHom f
185end CommTopGrp
187/-- Forget the commutativity of a bundled commutative topological group. -/
188def commTopGrpForgetToTopGrp : CommTopGrp.{u} ⥤ TopGrp.{u} where
189 obj G := TopGrp.of G
190 map f := TopGrp.ofHom f.hom
191 map_id G := by
192 apply TopGrp.hom_ext
193 rfl
194 map_comp f g := by
195 apply TopGrp.hom_ext
196 rfl
197end ProCGroups