ProCGrp C is the full subcategory of Mathlib's ProfiniteGrp cut out by HasOpenNormalBasisInClass C. Thus the ambient object supplies the group, topological-group, compact, Hausdorff, and totally disconnected structures; the class-restricted open-normal basis is the only additional property.
The canonical object property underlying the category of pro-C groups.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe udef ProCGroups.proCObjectProperty (C : ProCGroups.FiniteGroupClass.{u}) :
ObjectProperty ProfiniteGrp.{u}Pro-\(C\) groups: profinite groups with an open-normal quotient basis in \(C\).
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe uabbrev ProCGrp (C : ProCGroups.FiniteGroupClass.{u})A canonical pro-C object has exactly the carrier of its ambient ProfiniteGrp object.
This is the only carrier coercion installed here. All algebraic and topological instances then come definitionally from G.obj; redeclaring them on ProCGrp would create competing instance paths with the ambient full-subcategory concrete structure.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe u
namespace ProCGrp
variable {C : ProCGroups.FiniteGroupClass.{u}}instance : CoeSort (ProCGrp C) (Type u) where
coe G := G.objConstruct a bundled pro-\(C\) group from a ProfiniteGrp and its open-normal basis property.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe u
namespace ProCGrp
variable {C : ProCGroups.FiniteGroupClass.{u}}def of (C : ProCGroups.FiniteGroupClass.{u})
(G : ProfiniteGrp.{u})
(hBasis : ProCGroups.ProC.HasOpenNormalBasisInClass C G) : ProCGrp CThe continuous homomorphism carried by a full-subcategory morphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe u
namespace ProCGrp
variable {C : ProCGroups.FiniteGroupClass.{u}}abbrev continuousHom {A B : ProCGrp C} (f : A ⟶ B) : A →ₜ* BMorphisms in ProCGrp are equal when their underlying continuous homomorphisms are equal.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe u
namespace ProCGrp
variable {C : ProCGroups.FiniteGroupClass.{u}}theorem hom_ext {A B : ProCGrp C} {f g : A ⟶ B}
(hf : continuousHom f = continuousHom g) :
f = gOn profinite groups the all-finite object property imposes no additional condition.
Surrounding namespaces, section variables, and local commands at this declaration.
open CategoryTheory Topology
universe u
namespace ProCGrp
variable {C : ProCGroups.FiniteGroupClass.{u}}theorem allFinite_property (G : ProfiniteGrp.{u}) :
ProCGroups.proCObjectProperty ProCGroups.FiniteGroupClass.allFinite G