Source: ProCGroups.ProC.Category.Basic
1import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
2import ProCGroups.ProC.Subgroups.Closed
4/-!
5# The category of pro-\(C\) groups
7`ProCGrp C` is the full subcategory of Mathlib's `ProfiniteGrp` cut out by
8`HasOpenNormalBasisInClass C`. Thus the ambient object supplies the group, topological-group,
9compact, Hausdorff, and totally disconnected structures; the class-restricted open-normal basis is
10the only additional property.
11-/
13open CategoryTheory Topology
15universe u
17/-- The canonical object property underlying the category of pro-`C` groups. -/
18def ProCGroups.proCObjectProperty (C : ProCGroups.FiniteGroupClass.{u}) :
19 ObjectProperty ProfiniteGrp.{u} :=
20 fun G => ProCGroups.ProC.HasOpenNormalBasisInClass C G
22/-- Pro-\(C\) groups: profinite groups with an open-normal quotient basis in \(C\). -/
23@[pp_with_univ]
24abbrev ProCGrp (C : ProCGroups.FiniteGroupClass.{u}) :=
25 (ProCGroups.proCObjectProperty C).FullSubcategory
29namespace ProCGrp
31variable {C : ProCGroups.FiniteGroupClass.{u}}
33/-- A canonical pro-`C` object has exactly the carrier of its ambient `ProfiniteGrp` object.
35This is the only carrier coercion installed here. All algebraic and topological instances then
36come definitionally from `G.obj`; redeclaring them on `ProCGrp` would create competing instance
37paths with the ambient full-subcategory concrete structure. -/
38instance : CoeSort (ProCGrp C) (Type u) where
39 coe G := G.obj
41/-- Construct a bundled pro-\(C\) group from a `ProfiniteGrp` and its open-normal basis property. -/
42def of (C : ProCGroups.FiniteGroupClass.{u})
43 (G : ProfiniteGrp.{u})
44 (hBasis : ProCGroups.ProC.HasOpenNormalBasisInClass C G) : ProCGrp C :=
45 ⟨G, hBasis⟩
47/-- The continuous homomorphism carried by a full-subcategory morphism. -/
48abbrev continuousHom {A B : ProCGrp C} (f : A ⟶ B) : A →ₜ* B :=
49 ConcreteCategory.hom (C := ProCGrp C) f
51/-- Morphisms in ProCGrp are equal when their underlying continuous homomorphisms are equal. -/
52@[ext] theorem hom_ext {A B : ProCGrp C} {f g : A ⟶ B}
53 (hf : continuousHom f = continuousHom g) :
54 f = g :=
55 ConcreteCategory.ext hf
57/-- On profinite groups the all-finite object property imposes no additional condition. -/
58@[simp] theorem allFinite_property (G : ProfiniteGrp.{u}) :
60 intro W hW h1W
62 (G := G) hW h1W with ⟨U, hUW⟩
63 exact ⟨U, hUW, ProCGroups.openNormalSubgroup_finiteQuotient (G := G) U⟩
65end ProCGrp