Yamaguchi Lean 4 Library
ProCGroups/ProC/Category/Basic.lean
ProCGroups/ProC/Category/Basic/Source

ProCGroups/ProC/Category/Basic.lean

1import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
2import ProCGroups.ProC.Subgroups.Closed
3import ProCGroups.Profinite.MathlibBridge
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/ProCGroups/ProC/Category/Basic.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Pro-C groups and open normal quotients
16Defines pro-C conditions from finite group classes, C-open normal subgroups, pro-C categories, products, pullbacks, pushouts, and maximal pro-C quotients.
17-/
19open CategoryTheory Topology
21universe u v
23/-- The category of pro-`C` groups for a fixed topological pro-`C` predicate. -/
24@[pp_with_univ]
25structure ProCGrp (ProC : ProCGroups.ProC.ProCGroupPredicate.{u}) where
26 /-- The underlying Mathlib profinite group. -/
27 toProfiniteGrp : ProfiniteGrp.{u}
28 /-- The pro-`C` structure on the underlying profinite group. -/
31attribute [instance] ProCGrp.proCGroup
33namespace ProCGrp
35variable {ProC : ProCGroups.ProC.ProCGroupPredicate.{u}}
37/-- A bundled pro-`C` group coerces to its carrier type. -/
38instance instCoeSort : CoeSort (ProCGrp ProC) (Type u) where
39 coe G := G.toProfiniteGrp
41/-- A bundled pro-`C` group inherits the group structure of its underlying profinite group. -/
42instance instGroup (G : ProCGrp ProC) : Group G :=
43 inferInstanceAs (Group G.toProfiniteGrp)
45/-- A bundled pro-`C` group inherits the topology of its underlying profinite group. -/
46instance instTopologicalSpace (G : ProCGrp ProC) : TopologicalSpace G :=
47 inferInstanceAs (TopologicalSpace G.toProfiniteGrp)
49/-- A bundled pro-`C` group inherits the topological group structure of its underlying profinite
50group. -/
51instance instIsTopologicalGroup (G : ProCGrp ProC) : IsTopologicalGroup G :=
52 inferInstanceAs (IsTopologicalGroup G.toProfiniteGrp)
54/-- A bundled pro-`C` group inherits compactness from its underlying profinite group. -/
55instance instCompactSpace (G : ProCGrp ProC) : CompactSpace G :=
56 inferInstanceAs (CompactSpace G.toProfiniteGrp)
58/-- A bundled pro-`C` group inherits the Hausdorff property from its underlying profinite group. -/
59instance instT2Space (G : ProCGrp ProC) : T2Space G :=
60 inferInstanceAs (T2Space G.toProfiniteGrp)
62/-- A bundled pro-`C` group inherits total disconnectedness from its underlying profinite group. -/
63instance instTotallyDisconnectedSpace (G : ProCGrp ProC) : TotallyDisconnectedSpace G :=
64 inferInstanceAs (TotallyDisconnectedSpace G.toProfiniteGrp)
66/-- A bundled pro-`C` group carries its registered pro-`C` structure. -/
67instance instProCGroup (G : ProCGrp ProC) : ProCGroups.ProC.ProCGroup ProC G :=
68 inferInstanceAs (ProCGroups.ProC.ProCGroup ProC G.toProfiniteGrp)
70/-- Construct a bundled pro-`C` group from an unbundled topological group with a `ProCGroup`
71instance. -/
72abbrev of (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
73 (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
74 [ProCGroups.ProC.ProCGroup ProC G] : ProCGrp ProC where
76 letI : CompactSpace G := ProCGroups.ProC.ProCGroup.compactSpace ProC G
77 letI : TotallyDisconnectedSpace G :=
79 exact ProfiniteGrp.of G
80 proCGroup := inferInstance
82/-- The carrier of a freshly bundled pro-`C` group is the original type. -/
83@[simp] theorem coe_of (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
85 (of ProC G : Type u) = G :=
86 rfl
88/-- The type of morphisms in `ProCGrp`. -/
89@[ext]
90structure Hom (A B : ProCGrp ProC) where
91 /-- The underlying continuous monoid homomorphism. -/
92 hom' : A →ₜ* B
94/-- Bundled pro-`C` groups form a category with continuous homomorphisms. -/
95instance instCategory : Category (ProCGrp ProC) where
96 Hom A B := Hom A B
97 id A := ⟨ContinuousMonoidHom.id A⟩
98 comp f g := ⟨g.hom'.comp f.hom'⟩
100/-- The category of bundled pro-`C` groups is concrete via continuous homomorphisms. -/
101instance instConcreteCategory : ConcreteCategory (ProCGrp ProC) (fun X Y => X →ₜ* Y) where
102 hom f := f.hom'
103 ofHom f := ⟨f⟩
105/-- The underlying continuous monoid homomorphism. -/
106abbrev Hom.hom {A B : ProCGrp ProC} (f : A ⟶ B) : A →ₜ* B :=
107 ConcreteCategory.hom (C := ProCGrp ProC) f
109/-- Morphisms of bundled pro-`C` groups coerce to functions. -/
110instance instCoeFunHom {A B : ProCGrp ProC} : CoeFun (A ⟶ B) (fun _ => A → B) where
111 coe f := f.hom
113/-- The underlying homomorphism of the identity morphism is the identity continuous homomorphism. -/
114@[simp] theorem hom_id {A : ProCGrp ProC} :
115 (𝟙 A : A ⟶ A).hom = ContinuousMonoidHom.id A :=
116 rfl
118/-- The identity morphism acts as the identity function. -/
119@[simp] theorem id_apply (A : ProCGrp ProC) (a : A) :
120 (𝟙 A : A ⟶ A) a = a := by
121 simp only [hom_id, ContinuousMonoidHom.id_toFun]
123/-- The underlying homomorphism of a composite is the composite of underlying homomorphisms. -/
124@[simp] theorem hom_comp {A B C : ProCGrp ProC} (f : A ⟶ B) (g : B ⟶ C) :
125 (f ≫ g).hom = g.hom.comp f.hom :=
126 rfl
128/-- Composition of morphisms agrees with composition of functions. -/
129@[simp] theorem comp_apply {A B C : ProCGrp ProC} (f : A ⟶ B) (g : B ⟶ C) (a : A) :
130 (f ≫ g) a = g (f a) := by
131 rfl
133/-- Morphisms of pro-`C` groups are extensional in their underlying continuous homomorphisms. -/
134@[ext] theorem hom_ext {A B : ProCGrp ProC} {f g : A ⟶ B} (hf : f.hom = g.hom) :
135 f = g :=
136 Hom.ext hf
138/-- Typecheck a continuous monoid homomorphism as a morphism in `ProCGrp`. -/
139abbrev ofHom {X Y : Type u}
140 [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
142 [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
144 (f : X →ₜ* Y) : of ProC X ⟶ of ProC Y :=
145 ConcreteCategory.ofHom f
147/-- `ofHom` has the prescribed underlying continuous homomorphism. -/
148@[simp] theorem hom_ofHom {X Y : Type u}
149 [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
151 [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
153 (f : X →ₜ* Y) : (ofHom (ProC := ProC) f).hom = f :=
154 rfl
156/-- Reconstructing a morphism from its underlying continuous homomorphism gives the original
157morphism. -/
158@[simp] theorem ofHom_hom {A B : ProCGrp ProC} (f : A ⟶ B) :
159 ConcreteCategory.ofHom (C := ProCGrp ProC) f.hom = f :=
160 rfl
162/-- `ofHom` sends the identity continuous homomorphism to the identity morphism. -/
163@[simp] theorem ofHom_id {X : Type u}
164 [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
166 ofHom (ProC := ProC) (ContinuousMonoidHom.id X) = 𝟙 (of ProC X) :=
167 rfl
169/-- `ofHom` sends composition of continuous homomorphisms to categorical composition. -/
170@[simp] theorem ofHom_comp {X Y Z : Type u}
171 [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
173 [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
175 [Group Z] [TopologicalSpace Z] [IsTopologicalGroup Z]
177 (f : X →ₜ* Y) (g : Y →ₜ* Z) :
178 ofHom (ProC := ProC) (g.comp f) = ofHom (ProC := ProC) f ≫ ofHom (ProC := ProC) g :=
179 rfl
181/-- Applying a morphism built by `ofHom` is applying the original continuous homomorphism. -/
182@[simp] theorem ofHom_apply {X Y : Type u}
183 [Group X] [TopologicalSpace X] [IsTopologicalGroup X]
185 [Group Y] [TopologicalSpace Y] [IsTopologicalGroup Y]
187 (f : X →ₜ* Y) (x : X) :
188 ofHom (ProC := ProC) f x = f x :=
189 rfl
191/-- Forget a bundled pro-`C` group to its underlying profinite group. -/
192instance instHasForgetToProfiniteGrp : HasForget₂ (ProCGrp ProC) ProfiniteGrp where
193 forget₂ :=
194 { obj := fun G => G.toProfiniteGrp
195 map := fun f => ProfiniteGrp.ofHom f.hom }
197/-- Forget a bundled pro-`C` group to its underlying abstract group. -/
198instance instHasForgetToGrpCat : HasForget₂ (ProCGrp ProC) GrpCat where
199 forget₂ :=
200 { obj := fun G => GrpCat.of G
201 map := fun f => GrpCat.ofHom f.hom.toMonoidHom }
203/-- The forgetful functor from pro-`C` groups to profinite groups is faithful. -/
204instance instFaithfulForgetToProfiniteGrp : (forget₂ (ProCGrp ProC) ProfiniteGrp).Faithful where
205 map_injective := by
206 intro X Y f g h
207 ext x
208 exact CategoryTheory.congr_fun h x
210/-- Every Mathlib profinite group is a pro-`C` group for the all-finite predicate. -/
211instance allFiniteProCGroup (G : ProfiniteGrp.{u}) :
217/-- A finite group in the finite quotient class of `ProC`, with the discrete topology, is a
218bundled pro-`C` group. -/
220 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
221 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
222 (G : FiniteGrp.{u}) (hG : ProC.finiteQuotientClass G) : ProCGrp ProC := by
223 letI : TopologicalSpace G := ⊥
224 letI : DiscreteTopology G := ⟨rfl⟩
225 letI : IsTopologicalGroup G := inferInstance
228 exact of ProC G
230/-- Closed subgroups of pro-`C` groups are pro-`C`. -/
232 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
233 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
234 [ProC.DeterminedByFiniteQuotients]
235 (G : ProCGrp ProC) (H : ClosedSubgroup G) : ProCGrp ProC where
236 toProfiniteGrp := ProfiniteGrp.ofClosedSubgroup (G := G.toProfiniteGrp) H
237 proCGroup := by
238 simpa using
240 (G := G) ProC H)
242/-- Transport a pro-`C` group structure across a continuous multiplicative equivalence. -/
243noncomputable def ofContinuousMulEquiv
244 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
245 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
246 (G : ProCGrp ProC) {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
247 (e : G ≃ₜ* H) : ProCGrp ProC := by
250 exact of ProC H
252/-- Products of pro-`C` groups are pro-`C` when the finite quotient class is a formation. -/
253def pi
254 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
255 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
256 {α : Type u} (β : α → ProCGrp ProC) : ProCGrp ProC := by
257 let Pβ : α → ProfiniteGrp.{u} := fun a => (β a).toProfiniteGrp
258 letI : ProCGroups.ProC.ProCGroup ProC ((a : α) → β a) :=
259 ProCGroups.ProC.ProCGroup.pi (β := fun a => (β a : Type u)) ProC
260 exact
261 { toProfiniteGrp := ProfiniteGrp.pi Pβ
262 proCGroup := by
263 simpa [Pβ, ProfiniteGrp.pi] using
264 (inferInstance : ProCGroups.ProC.ProCGroup ProC ((a : α) → β a)) }
266/-- Quotients by open normal subgroups of pro-`C` groups are pro-`C`. -/
268 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
269 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
270 (G : ProCGrp ProC) (U : OpenNormalSubgroup G) : ProCGrp ProC := by
271 letI : ProCGroups.ProC.ProCGroup ProC (G ⧸ (U : Subgroup G)) :=
273 (G := G) ProC U
274 exact of ProC (G ⧸ (U : Subgroup G))
276/-- Quotients by open normal subgroups from the finite-quotient class family are pro-`C`. -/
278 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
279 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
280 (G : ProCGrp ProC)
281 (U : ProCGroups.ProC.OpenNormalSubgroupInClass ProC.finiteQuotientClass G) :
282 ProCGrp ProC :=
285/-- Quotients by closed normal subgroups of pro-`C` groups are pro-`C`. -/
287 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
288 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.DeterminedByFiniteQuotients]
289 (G : ProCGrp ProC) (K : Subgroup G) [K.Normal] (hK : IsClosed (K : Set G)) :
290 ProCGrp ProC := by
291 letI : ProCGroups.ProC.ProCGroup ProC (G ⧸ K) :=
293 (G := G) ProC K hK
294 exact of ProC (G ⧸ K)
296/-- The range of a morphism of pro-`C` groups, with its induced topology, is pro-`C`. -/
297def range
298 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
299 [ProC.HasFiniteQuotientFormation] [ProC.DeterminedByFiniteQuotients]
300 {A B : ProCGrp ProC} (f : A ⟶ B) : ProCGrp ProC := by
301 letI : ProCGroups.ProC.ProCGroup ProC f.hom.toMonoidHom.range :=
303 (G := A) (H := B) ProC f.hom
304 exact of ProC f.hom.toMonoidHom.range
306/-- The kernel subgroup of a morphism of pro-`C` groups, with its induced topology, is pro-`C`. -/
307def kernel
308 (ProC : ProCGroups.ProC.ProCGroupPredicate.{u})
309 [ProC.HasFiniteQuotientMelnikovFormation] [ProC.HasFiniteQuotientHereditary]
310 [ProC.DeterminedByFiniteQuotients]
311 {A B : ProCGrp ProC} (f : A ⟶ B) : ProCGrp ProC := by
312 let K : Subgroup A := f.hom.toMonoidHom.ker
313 have hK : IsClosed (K : Set A) := by
314 dsimp [K]
315 exact f.hom.isClosed_ker
318 (G := A) ProC K hK
319 exact of ProC K