import
- ProCGroups.ProC.GroupPredicate
- ProCGroups.ProC.OpenNormalSubgroups.ProCGroup
- Mathlib.GroupTheory.Commutator.Basic
def allFiniteProC : ProCGroupPredicate.{u} where
holds := fun {G} [_] [_] [_] => IsProfiniteGroup GThe all-finite pro-\(C\) predicate is profiniteness.
protected def finiteGroupClassProCPredicate
(C : FiniteGroupClass.{u}) : ProCGroupPredicate where
holds := fun {G} [_] [_] [_] =>
IsProCGroup C GThe canonical topological pro-\(C\) predicate attached to a concrete finite-group class \(C\). This declaration is protected to keep unqualified resolution stable when several pro-\(C\) namespaces are open at once.
@[simp] theorem finiteGroupClassProCPredicate_holds_iff
{C : FiniteGroupClass.{u}}
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
(ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G) ↔
IsProCGroup C GThe two defining conditions are equivalent after unfolding.
Show proof
Iff.rflProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem isProfiniteGroup_of_finiteGroupClassProCPredicate
(C : FiniteGroupClass.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : (ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G)) :
IsProfiniteGroup GA group satisfying the concrete finite-class pro-\(C\) predicate is profinite.
Show proof
hG.isProfiniteProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem finiteGroupClassProCPredicate_mono
{C C' : FiniteGroupClass.{u}}
(hmono :
∀ {G : Type u} [Group G], C' G → C G)
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
(ProCGroups.ProC.finiteGroupClassProCPredicate C') (G := G) →
(ProCGroups.ProC.finiteGroupClassProCPredicate C) (G := G)Concrete class inclusion induces monotonicity of the corresponding pro-\(C\) predicates.
Show proof
by
intro hG
exact ⟨hG.isProfinite, hG.basis.mono hmono⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□structure ProCTheory where
predicate : ProCGroupPredicate.{u}
finiteQuotientClass : FiniteGroupClass.{u}
formation : FiniteGroupClass.Formation finiteQuotientClass
predicate_iff_isProCGroup :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
predicate (G := G) ↔ IsProCGroup finiteQuotientClass GA bundled pro-\(C\) theory: a topological predicate, the finite quotient class that controls it, and the formation data for that finite class. This is the preferred package when a theorem needs to move between an abstract pro-\(C\) predicate and finite quotient closure hypotheses without carrying several unrelated arguments.
structure ProCTheorySound where
predicate : ProCGroupPredicate.{u}
finiteQuotientClass : FiniteGroupClass.{u}
formation : FiniteGroupClass.Formation finiteQuotientClass
sound :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
IsProCGroup finiteQuotientClass G → predicate (G := G)One-directional version of ProCTheory, for predicates known to contain the concrete finite-quotient pro-\(C\) groups but not known to be equivalent to them.
abbrev holds (T : ProCTheory.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop :=
T.predicate (G := G)View a theory as its topological pro-\(C\) predicate.
abbrev IsProCGroup (T : ProCTheory.{u})
(G : Type u) [Group G] [TopologicalSpace G] : Prop :=
ProCGroups.ProC.IsProCGroup T.finiteQuotientClass GThe concrete pro-\(C\) group condition controlled by a theory.
def ofFiniteFormation
(C : FiniteGroupClass.{u}) [hC : FiniteGroupClass.IsFormation C] :
ProCTheory.{u} where
predicate := ProCGroups.ProC.finiteGroupClassProCPredicate C
finiteQuotientClass := C
formation := hC.formation
predicate_iff_isProCGroup := by
intro G _ _ _
exact Iff.rfldef ofPredicate
(ProC : ProCGroupPredicate.{u}) (C : FiniteGroupClass.{u})
(hForm : FiniteGroupClass.Formation C)
(hiff :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
ProC (G := G) ↔ ProCGroups.ProC.IsProCGroup C G) :
ProCTheory.{u} where
predicate := ProC
finiteQuotientClass := C
formation := hForm
predicate_iff_isProCGroup := hiffBuild a pro-\(C\) theory from an abstract predicate, its controlling finite quotient class, and an equivalence with the concrete pro-\(C\) condition.
def ofPredicateSound
(ProC : ProCGroupPredicate.{u}) (C : FiniteGroupClass.{u})
(hForm : FiniteGroupClass.Formation C)
(hsound :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
ProCGroups.ProC.IsProCGroup C G → ProC (G := G)) :
ProCTheorySound.{u} where
predicate := ProC
finiteQuotientClass := C
formation := hForm
sound := hsoundBuild the one-directional pro-\(C\) soundness package from an abstract predicate and a soundness theorem.
theorem holds_iff_isProCGroup (T : ProCTheory.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
T.holds (G := G) ↔ T.IsProCGroup GA theory predicate is equivalent to the concrete pro-\(C\) condition for its finite quotient class.
Show proof
T.predicate_iff_isProCGroupProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem isProCGroup_of_holds (T : ProCTheory.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : T.holds (G := G)) : T.IsProCGroup GThe predicate side of a theory implies the concrete pro-\(C\) condition.
Show proof
(T.holds_iff_isProCGroup).1 hGProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□theorem holds_of_isProCGroup (T : ProCTheory.{u})
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : T.IsProCGroup G) : T.holds (G := G)The concrete pro-\(C\) condition implies the predicate side of a theory.
Show proof
(T.holds_iff_isProCGroup).2 hGProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating. Consequently the two expressions have the same determining coordinates, and the defining extensionality principle for the inverse-limit, quotient, or presentation construction gives the claim in the statement.
□def finiteQuotientFormation (T : ProCTheory.{u}) :
FiniteGroupClass.Formation T.finiteQuotientClass :=
T.formationThe finite quotient class packaged by a theory is a formation.
def quotientClosed (T : ProCTheory.{u}) :
FiniteGroupClass.QuotientClosed T.finiteQuotientClass :=
T.formation.quotientClosedFormation data gives quotient closure for the finite quotient class of a theory.
def isomClosed (T : ProCTheory.{u}) :
FiniteGroupClass.IsomClosed T.finiteQuotientClass :=
T.formation.isomClosedFormation data gives isomorphism closure for the finite quotient class of a theory.
def finiteQuotientClass (ProC : ProCGroupPredicate.{u}) :
FiniteGroupClass.{u} where
pred := fun Q [Group Q] =>
Finite Q ∧
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
ProC (G := Q)
finite_of_mem := fun hQ => hQ.1The discrete finite-quotient class induced by a topological pro-\(C\) predicate.
class DeterminedByFiniteQuotients
(ProC : ProCGroupPredicate.{u}) : Prop where
holds_of_isProCGroup :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
IsProCGroup ProC.finiteQuotientClass G → ProC (G := G)A topological pro-\(C\) predicate is determined by its finite quotient class.
class HasFiniteQuotientFormation
(ProC : ProCGroupPredicate.{u}) : Prop where
formation : FiniteGroupClass.Formation (ProC.finiteQuotientClass)Formation data for the finite quotient class attached to a pro-\(C\) predicate.
class HasFiniteQuotientMelnikovFormation
(ProC : ProCGroupPredicate.{u}) : Prop where
melnikovFormation : FiniteGroupClass.MelnikovFormation (ProC.finiteQuotientClass)The Melnikov formation data for the finite quotient class attached to a pro-\(C\) predicate.
class HasFiniteQuotientFullFormation
(ProC : ProCGroupPredicate.{u}) : Prop where
fullFormation : FiniteGroupClass.FullFormation (ProC.finiteQuotientClass)Full formation data for the finite quotient class attached to a pro-\(C\) predicate.
class HasFiniteQuotientHereditary
(ProC : ProCGroupPredicate.{u}) : Prop where
hereditary : FiniteGroupClass.Hereditary (ProC.finiteQuotientClass)Hereditary data for the finite quotient class attached to a pro-\(C\) predicate.
class HasFiniteQuotientFinite
(ProC : ProCGroupPredicate.{u}) : Prop where
finite : ∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite QFiniteness of the finite quotient class attached to a pro-\(C\) predicate.
class HasFiniteQuotientExtensionClosed
(ProC : ProCGroupPredicate.{u}) : Prop where
extensionClosed : FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass)Extension-closure data for the finite quotient class attached to a pro-\(C\) predicate.
class ClosedUnderCommutatorKernelQuotientsFrom
(Target Source : ProCGroupPredicate.{u}) : Prop where
quotient_by_kernel_commutator :
∀ {E F : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
[Group F] [TopologicalSpace F] [IsTopologicalGroup F]
(φ : E →ₜ* F),
Source (G := E) → Target (G := F) →
Target (G := E ⧸ ⁅φ.toMonoidHom.ker, φ.toMonoidHom.ker⁆)Permanence data for quotienting a Source pro-\(C\) group by the commutator subgroup of the kernel of a continuous homomorphism to a Target pro-\(C\) group. The mixed source/target form is useful for maximal-quotient arguments, where the source is often known to be pro-\(C\)_e while the quotient must be pro-\(C\).
theorem quotient_by_kernel_commutator
(Target Source : ProCGroupPredicate.{u})
[Target.ClosedUnderCommutatorKernelQuotientsFrom Source]
{E F : Type u} [Group E] [TopologicalSpace E] [IsTopologicalGroup E]
[Group F] [TopologicalSpace F] [IsTopologicalGroup F]
(φ : E →ₜ* F)
(hE : Source (G := E)) (hF : Target (G := F)) :
Target (G := E ⧸ ⁅φ.toMonoidHom.ker, φ.toMonoidHom.ker⁆)The quotient by the kernel commutator is compatible with open-normal finite quotients and refinement maps.
Show proof
ClosedUnderCommutatorKernelQuotientsFrom.quotient_by_kernel_commutator φ hE hFProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□def finiteQuotientFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.Formation (ProC.finiteQuotientClass) :=
ProCGroupPredicate.HasFiniteQuotientFormation.formationThe finite quotient class packaged by a theory is a formation.
def finiteQuotientMelnikovFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
FiniteGroupClass.MelnikovFormation (ProC.finiteQuotientClass) :=
ProCGroupPredicate.HasFiniteQuotientMelnikovFormation.melnikovFormationdef finiteQuotientFullFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.FullFormation (ProC.finiteQuotientClass) :=
ProCGroupPredicate.HasFiniteQuotientFullFormation.fullFormationdef finiteQuotientHereditary
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientHereditary] :
FiniteGroupClass.Hereditary (ProC.finiteQuotientClass) :=
ProCGroupPredicate.HasFiniteQuotientHereditary.hereditaryAccessor for hereditary finite quotient data attached to a pro-\(C\) predicate.
def finiteQuotientFinite
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFinite] :
∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite Q :=
ProCGroupPredicate.HasFiniteQuotientFinite.finiteAccessor asserting that every member of the finite quotient class is finite.
def finiteQuotientExtensionClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientExtensionClosed] :
FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass) :=
ProCGroupPredicate.HasFiniteQuotientExtensionClosed.extensionCloseddef finiteQuotientIsomClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.IsomClosed (ProC.finiteQuotientClass) :=
ProC.finiteQuotientFormation.isomClosedFormation data supplies isomorphism closure for the induced finite quotient class.
def finiteQuotientQuotientClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.QuotientClosed (ProC.finiteQuotientClass) :=
ProC.finiteQuotientFormation.quotientClosedFormation data supplies quotient closure for the induced finite quotient class.
def finiteQuotientFiniteProductClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.FiniteProductClosed (ProC.finiteQuotientClass) :=
ProC.finiteQuotientFormation.finiteProductClosedFormation data supplies finite-product closure for the induced finite quotient class.
def finiteQuotientContainsTrivialQuotients
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.ContainsTrivialQuotients (ProC.finiteQuotientClass) :=
ProC.finiteQuotientFormation.containsTrivialQuotientsFormation data supplies the trivial-quotient condition for the induced finite quotient class.
def finiteQuotientFullQuotientClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.QuotientClosed (ProC.finiteQuotientClass) :=
(ProC.finiteQuotientFullFormation).quotientClosedThe full formation data supply quotient closure.
def finiteQuotientFullIsomClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.IsomClosed (ProC.finiteQuotientClass) :=
(ProC.finiteQuotientFullFormation).isomClosedThe full formation data supply isomorphism closure.
def finiteQuotientFullFinite
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
∀ {Q : Type u} [Group Q], ProC.finiteQuotientClass Q → Finite Q :=
(ProC.finiteQuotientFullFormation).finiteOnlyThe full formation data include the fact that all members are finite.
def finiteQuotientFullExtensionClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.ExtensionClosed (ProC.finiteQuotientClass) :=
(ProC.finiteQuotientFullFormation).extensionClosedThe full formation data include closure under extensions.
def finiteQuotientFullHereditary
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.Hereditary (ProC.finiteQuotientClass) :=
(ProC.finiteQuotientFullFormation).hereditaryThe full formation data supply hereditary subgroup closure.
theorem finiteQuotientFullSubgroupClosed
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
FiniteGroupClass.SubgroupClosed (ProC.finiteQuotientClass)The full formation data supply ordinary subgroup closure.
Show proof
(ProC.finiteQuotientFullFormation).subgroupClosedProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□def hasFiniteQuotientFormation_of_melnikovFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
ProC.HasFiniteQuotientFormation where
formation := ProC.finiteQuotientMelnikovFormation.formationA Melnikov formation supplies the underlying formation structure.
def finiteQuotientClass_containsTrivialQuotients_of_formation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFormation] :
FiniteGroupClass.ContainsTrivialQuotients ProC.finiteQuotientClass :=
ProC.finiteQuotientFormation.containsTrivialQuotientsFormation data supplies the trivial-quotient instance for the induced finite quotient class.
def hasFiniteQuotientFinite_of_melnikovFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
ProC.HasFiniteQuotientFinite where
finite := (ProC.finiteQuotientMelnikovFormation).finiteOnlyA Melnikov formation supplies finiteness of members of the induced finite quotient class.
def hasFiniteQuotientExtensionClosed_of_melnikovFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientMelnikovFormation] :
ProC.HasFiniteQuotientExtensionClosed where
extensionClosed := (ProC.finiteQuotientMelnikovFormation).extensionClosedA Melnikov formation supplies extension-closure of the induced finite quotient class.
def hasFiniteQuotientMelnikovFormation_of_fullFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
ProC.HasFiniteQuotientMelnikovFormation where
melnikovFormation := ProC.finiteQuotientFullFormation.melnikovFormationA full formation supplies the underlying Melnikov formation.
def hasFiniteQuotientHereditary_of_fullFormation
(ProC : ProCGroupPredicate.{u}) [ProC.HasFiniteQuotientFullFormation] :
ProC.HasFiniteQuotientHereditary where
hereditary := (ProC.finiteQuotientFullFormation).hereditaryA full formation supplies hereditary closure of the induced finite quotient class.
theorem of_mulEquiv
{C : FiniteGroupClass.{u}} (hiso : FiniteGroupClass.IsomClosed C)
{G K : Type u}
[Group G] [TopologicalSpace G]
[Group K] [TopologicalSpace K]
(e : G ≃* K) (hcont : Continuous e) (hcontinuous_symm : Continuous e.symm)
(hbasis : HasOpenNormalBasisInClass C K) :
HasOpenNormalBasisInClass C GTransport a \(C\)-quotient open-normal basis across a continuous multiplicative equivalence.
Show proof
by
intro W hW h1W
let V : Set K := e.symm ⁻¹' W
have hV : IsOpen V := hW.preimage hcontinuous_symm
have h1V : (1 : K) ∈ V := by
simpa [V] using h1W
rcases hbasis V hV h1V with ⟨U, hUV, hCU⟩
let Ucomap : OpenNormalSubgroup G :=
OpenNormalSubgroup.comap (e : G →* K) hcont U
refine ⟨Ucomap, ?_, ?_⟩
· intro g hg
have heg : e g ∈ ((U : OpenNormalSubgroup K) : Subgroup K) :=
(OpenNormalSubgroup.mem_comap
(f := (e : G →* K)) (hf := hcont) (U := U)).1 hg
have hVmem : e g ∈ V := hUV heg
simpa [V] using hVmem
· have hmap :
((Ucomap : OpenNormalSubgroup G) : Subgroup G).map (e : G →* K) =
((U : OpenNormalSubgroup K) : Subgroup K) := by
ext k
constructor
· rintro ⟨g, hg, rfl⟩
exact
(OpenNormalSubgroup.mem_comap
(f := (e : G →* K)) (hf := hcont) (U := U)).1 hg
· intro hk
refine ⟨e.symm k, ?_, by simp only [MonoidHom.coe_coe, MulEquiv.apply_symm_apply]⟩
exact
(OpenNormalSubgroup.mem_comap
(f := (e : G →* K)) (hf := hcont) (U := U)).2
(by simpa using hk)
exact hiso ⟨(QuotientGroup.congr
(Ucomap : Subgroup G) (U : Subgroup K) e hmap).symm⟩ hCUProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem profiniteGroup_eq_one_of_mem_all_openNormalSubgroups
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : IsProfiniteGroup G) {x : G}
(hx : ∀ U : OpenNormalSubgroup G, x ∈ (U : Subgroup G)) :
x = 1In a profinite group, an element lying in every open normal subgroup is trivial.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
by_contra hxne
let W : Set G := ({x} : Set G)ᶜ
have hW : IsOpen W := by
simp only [isOpen_compl_iff, Set.finite_singleton, Set.Finite.isClosed, W]
have h1W : (1 : G) ∈ W := by
have hx1 : (1 : G) ≠ x := by
intro h1x
exact hxne h1x.symm
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, hx1, not_false_eq_true, W]
rcases ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
(G := G) hW h1W with
⟨U, hUW⟩
have hxW : x ∈ W := hUW (hx U)
simp only [Set.mem_compl_iff, Set.mem_singleton_iff, not_true_eq_false, W] at hxWProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□class ProCGroup (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop where
isProC : ProC (G := G)
isProCGroup : IsProCGroup ProC.finiteQuotientClass GTypeclass form of belonging to an ambient topological pro-\(C\) predicate.
theorem profiniteGroup (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
IsProfiniteGroup GA pro-\(C\) group is profinite.
Show proof
hG.isProCGroup.1Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem isTopologicalGroup (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
IsTopologicalGroup GA pro-\(C\) group is a topological group.
Show proof
hG.isProCGroup.isTopologicalGroupProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem compactSpace (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
CompactSpace GThe compact-space instance on a profinite space.
Show proof
hG.isProCGroup.compactSpaceProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem t2Space (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
T2Space GA pro-\(C\) group is Hausdorff.
Show proof
hG.isProCGroup.t2SpaceProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem t1Space (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
T1Space GA profinite space is \(T_1\).
Show proof
by
letI : T2Space G := ProCGroup.t2Space ProC G
infer_instanceProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. Functoriality and naturality are proved by comparing the two composites after projection to an arbitrary target stage. The source stage is the pullback or refined quotient required by the construction, and both composites are induced by the same quotient homomorphism together with the same coefficient map; hence the coordinate maps agree and so do the completed maps.
□theorem totallyDisconnectedSpace (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
TotallyDisconnectedSpace GA pro-\(C\) group is totally disconnected.
Show proof
hG.isProCGroup.totallyDisconnectedSpaceProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem finite_quotient (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] (U : OpenNormalSubgroup G) :
Finite (G ⧸ (U : Subgroup G))Open normal quotients of a pro-\(C\) group are finite.
Show proof
hG.isProCGroup.finite_quotient UProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem quotient_mem (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] [ProC.HasFiniteQuotientFormation] (U : OpenNormalSubgroup G) :
ProC.finiteQuotientClass (G ⧸ (U : Subgroup G))Open normal quotients of a pro-\(C\) group lie in the induced finite quotient class.
Show proof
hG.isProCGroup.quotient_mem ProC.finiteQuotientFormation UProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem hasOpenNormalBasisInClass (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
HasOpenNormalBasisInClass ProC.finiteQuotientClass GA pro-\(C\) group has an open-normal basis whose quotients lie in the induced finite quotient class.
Show proof
hG.isProCGroup.hasOpenNormalBasisInClassProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem exists_openNormalSubgroupInClass_sub_open_nhds_of_one
(ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G]
{W : Set G} (hW : IsOpen W) (h1W : (1 : G) ∈ W) :
∃ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
(((U.1 : Subgroup G) : Set G)) ⊆ WEvery neighborhood of \(1\) in a pro-\(C\) group contains an open normal subgroup whose quotient lies in the induced finite quotient class.
Show proof
hG.isProCGroup.exists_openNormalSubgroupInClass_sub_open_nhds_of_one hW h1WProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem openNormalSubgroupInClass_nonempty (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
Nonempty (OpenNormalSubgroupInClass ProC.finiteQuotientClass G)The open-normal-in-class family of a pro-\(C\) group is nonempty.
Show proof
hG.isProCGroup.openNormalSubgroupInClass_nonemptyProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem iInf_openNormalSubgroupInClass_eq_bot (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
iInf (fun U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G =>
(U.1 : Subgroup G)) = (⊥ : Subgroup G)The open-normal-in-class subgroups of a pro-\(C\) group have trivial infimum.
Show proof
hG.isProCGroup.iInf_openNormalSubgroupInClass_eq_botProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem iInter_openNormalSubgroupInClass_eq_singleton (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] :
(⋂ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
(((U.1 : Subgroup G) : Set G))) = ({1} : Set G)The open-normal-in-class subgroups of a pro-\(C\) group intersect in the singleton \(\{1\}\).
Show proof
hG.isProCGroup.iInter_openNormalSubgroupInClass_eq_singletonProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem eq_one_of_mem_all_openNormalSubgroupInClass (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] {x : G}
(hx : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
x ∈ (U.1 : Subgroup G)) :
x = 1Membership in every open-normal-in-class subgroup of a pro-\(C\) group forces an element to be trivial.
Show proof
hG.isProCGroup.eq_one_of_mem_all_openNormalSubgroupInClass hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem exists_openNormalSubgroupInClass_not_mem (ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] {x : G} (hx : x ≠ 1) :
∃ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
x ∉ (U.1 : Subgroup G)A nontrivial element of a pro-\(C\) group is omitted by some open-normal-in-class subgroup.
Show proof
hG.isProCGroup.exists_openNormalSubgroupInClass_not_mem hxProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem eq_of_forall_openNormalSubgroupInClass_quotient_eq
(ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] {x y : G}
(hxy : ∀ U : OpenNormalSubgroupInClass ProC.finiteQuotientClass G,
QuotientGroup.mk' (U.1 : Subgroup G) x = QuotientGroup.mk' (U.1 : Subgroup G) y) :
x = yTwo elements of a pro-\(C\) group are equal when they agree in every open-normal-in-class quotient.
Show proof
hG.isProCGroup.eq_of_forall_openNormalSubgroupInClass_quotient_eq hxyProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem eq_of_forall_openNormalSubgroupInClassProj_eq
(ProC : ProCGroupPredicate.{u})
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G] {x y : G}
(hxy : ∀ U : OrderDual (OpenNormalSubgroupInClass ProC.finiteQuotientClass G),
openNormalSubgroupInClassProj (C := ProC.finiteQuotientClass) (G := G) U x =
openNormalSubgroupInClassProj (C := ProC.finiteQuotientClass) (G := G) U y) :
x = yCoordinatewise equality in the canonical open-normal-in-class quotient system forces equality in the ambient pro-\(C\) group.
Show proof
hG.isProCGroup.eq_of_forall_openNormalSubgroupInClassProj_eq hxyProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. Closed-subgroup and subgroup-permanence claims use ambient open-normal approximation: an open normal subgroup of the closed subgroup is refined by the intersection with an ambient open normal subgroup of \(G\). For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem of_isProCGroup
(ProC : ProCGroupPredicate.{u}) [ProC.DeterminedByFiniteQuotients]
(G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : IsProCGroup ProC.finiteQuotientClass G) :
ProCGroup ProC G where
isProCBuild the public pro-\(C\)-group class from the concrete quotient condition.
Show proof
ProCGroupPredicate.DeterminedByFiniteQuotients.holds_of_isProCGroup hG
isProCGroup := hGProof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem of_finiteQuotientClass_mono
{ProC ProD : ProCGroupPredicate.{u}} [ProD.DeterminedByFiniteQuotients]
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
[hG : ProCGroup ProC G]
(hmono :
∀ {Q : Type u} [Group Q],
ProC.finiteQuotientClass Q → ProD.finiteQuotientClass Q) :
ProCGroup ProD GEnlarge the finite quotient class of a bundled pro-\(C\) group.
Show proof
ProCGroup.of_isProCGroup ProD G (hG.isProCGroup.mono hmono)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□theorem allFiniteProC_finiteQuotientClass_of_finite
{Q : Type u} [Group Q] [Finite Q] :
allFiniteProC.finiteQuotientClass QA finite discrete group lies in the finite quotient class induced by allFiniteProC.
Show proof
by
refine ⟨inferInstance, ?_⟩
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
change IsProfiniteGroup Q
exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For pro-\(C\) claims, the finite quotient obtained from the construction remains in \(C\) by the relevant closure axiom, such as closure under subgroups, quotients, finite products, or extensions. The universal or lifting property is then checked on the prescribed generators, and uniqueness follows because the generators are dense or topologically generating.
□theorem allFiniteProC_finiteQuotientClass_iff_finite
{Q : Type u} [Group Q] :
allFiniteProC.finiteQuotientClass Q ↔ Finite QThe finite quotient class induced by allFiniteProC is exactly the all-finite class.
Show proof
by
constructor
· intro hQ
exact hQ.1
· intro hQ
letI : Finite Q := hQ
exact allFiniteProC_finiteQuotientClass_of_finite (Q := Q)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Kernel and image statements are verified after quotienting by sufficiently small open normal subgroups, where they become ordinary finite group calculations. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. Exactness is checked by separating injectivity, kernel containment, and image containment. Injectivity is either coordinatewise injectivity or the injectivity of a subtype inclusion; the kernel-to-image direction is obtained by packaging an element with the required vanishing proof, while the reverse direction is obtained by applying the next boundary or augmentation map and simplifying the defining relation.
□instance allFiniteProC_hasFiniteQuotientFullFormation :
ProCGroupPredicate.HasFiniteQuotientFullFormation allFiniteProC where
fullFormation :=
{ melnikovFormation :=
{ formation :=
{ quotientClosed := by
intro G _ N _ hG
exact allFiniteProC_finiteQuotientClass_iff_finite.2
(FiniteGroupClass.allFinite_quotientClosed N
(allFiniteProC_finiteQuotientClass_iff_finite.1 hG))
finiteSubdirectProductClosed := by
intro ι _ G _ H _ f hf _hsurj hH
exact allFiniteProC_finiteQuotientClass_iff_finite.2
(FiniteGroupClass.allFinite_finiteSubdirectProductClosed f hf _hsurj
(fun i => allFiniteProC_finiteQuotientClass_iff_finite.1 (hH i))) }
normalSubgroupClosed := by
intro Q _ N _ hQ
exact allFiniteProC_finiteQuotientClass_iff_finite.2
(FiniteGroupClass.allFinite_normalSubgroupClosed N
(allFiniteProC_finiteQuotientClass_iff_finite.1 hQ))
extensionClosed := by
intro E _ N _ hN hQ
exact allFiniteProC_finiteQuotientClass_iff_finite.2
(FiniteGroupClass.allFinite_extensionClosed N
(allFiniteProC_finiteQuotientClass_iff_finite.1 hN)
(allFiniteProC_finiteQuotientClass_iff_finite.1 hQ)) }
subgroupClosed := by
intro G _ H hG
exact allFiniteProC_finiteQuotientClass_iff_finite.2
(FiniteGroupClass.allFinite_subgroupClosed H
(allFiniteProC_finiteQuotientClass_iff_finite.1 hG)) }The all-finite pro-\(C\) predicate has a full finite quotient formation.
instance allFiniteProC_determinedByFiniteQuotients :
ProCGroupPredicate.DeterminedByFiniteQuotients allFiniteProC where
holds_of_isProCGroup hG := hG.isProfinitetheorem allFiniteProC_isProCGroup_of_profinite
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : IsProfiniteGroup G) :
IsProCGroup allFiniteProC.finiteQuotientClass GA profinite group is pro-\(C\) for the all-finite predicate in the concrete quotient sense.
Show proof
by
refine ⟨hG, ?_⟩
intro W hW h1W
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
rcases exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W with ⟨U, hUW⟩
have hfinite : Finite (G ⧸ (U : Subgroup G)) := by
exact
Subgroup.quotient_finite_of_isOpen (U : Subgroup G)
(openNormalSubgroup_isOpen (G := G) U)
letI : Finite (G ⧸ (U : Subgroup G)) := hfinite
exact ⟨U, hUW, allFiniteProC_finiteQuotientClass_of_finite (Q := G ⧸ (U : Subgroup G))⟩Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□theorem allFiniteProCGroup_of_profinite
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
(hG : IsProfiniteGroup G) :
ProCGroup allFiniteProC GA profinite group is a bundled pro-\(C\) group for the all-finite predicate.
Show proof
ProCGroup.of_isProCGroup allFiniteProC G (allFiniteProC_isProCGroup_of_profinite hG)Proof. Work with open normal subgroups and finite quotients of the profinite or pro-\(C\) group. Finite quotients separate points, and continuous homomorphisms are determined by their compatible quotient-level maps. For pro-\(C\) claims, the resulting finite quotients lie in \(C\) by the closure property used in the construction: closure under quotients, subgroups, finite products, or extensions. Continuity is checked by composing with all finite quotient projections; each composite is a continuous map between finite or profinite quotient spaces. Compatibility under refinement then assembles the finite-quotient data and proves the required profinite or pro-\(C\) statement. The quotient-level assertions are stable under passing to smaller open normal subgroups, so they define compatible data in the inverse system of finite quotients. For pro-\(C\) permanence, the construction uses only operations for which the chosen finite group class is closed. Hence the finite verification assembles to the desired profinite map, subgroup, or quotient statement. For categorical constructions such as products, pullbacks, and inverse limits, the universal property is checked by composing with the coordinate projections. The uniqueness part follows because any two candidate maps with the same finite quotient composites have the same value on every separating finite quotient. Existence is obtained by assembling the compatible coordinate maps supplied by the finite quotient construction. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument.
□