ProCGroups.ProC.GroupPredicates.Standard
This module sets up the finite-stage and inverse-limit description of the construction. It records the stage maps, projections, and comparison lemmas used to pass back to the completed object.
theorem finiteQuotientClass_finiteGroupClassProCPredicate_iff
{C : FiniteGroupClass.{u}}
(hquot : FiniteGroupClass.QuotientClosed C)
(hiso : FiniteGroupClass.IsomClosed C)
{Q : Type u} [Group Q] [Finite Q] :
(ProCGroups.ProC.finiteGroupClassProCPredicate C).finiteQuotientClass Q ↔ C QOn finite discrete groups, the finite quotient class induced by \(\mathrm{finiteGroupClassProCPredicate}\,C\) recovers \(C\), provided \(C\) is quotient- and isomorphism-closed.
Show proof
by
constructor
· intro hQ
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
change Finite Q ∧ IsProCGroup C Q at hQ
let Ubot : OpenNormalSubgroup Q :=
{ toOpenSubgroup := ⟨⊥, isOpen_discrete _⟩
isNormal' := inferInstance }
exact hiso ⟨QuotientGroup.quotientBot (G := Q)⟩
(IsProCGroup.hasAllOpenNormalQuotientsInClass_of_basis_of_quotientClosed
hiso hquot hQ.2 Ubot)
· intro hQ
letI : TopologicalSpace Q := ⊥
letI : DiscreteTopology Q := ⟨rfl⟩
letI : IsTopologicalGroup Q := inferInstance
exact ⟨FiniteGroupClass.finite hQ,
IsProCGroup.of_finite_discrete (C := C) (G := Q) hquot hQ⟩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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously.
□def finiteQuotientFormation_finiteGroupClassProCPredicate
(C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C) :
(ProCGroups.ProC.finiteGroupClassProCPredicate C).HasFiniteQuotientFormation where
formation := by
refine ⟨?_, ?_⟩
· intro G _ N _ hG
have hfiniteG : Finite G := by
exact FiniteGroupClass.finite hG
letI : Finite G := hfiniteG
have hCG : C G :=
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hG
exact
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed
(Q := G ⧸ N)).2 (hForm.quotientClosed N hCG)
· intro ι _ G _ H _ f hf hsurj hH
have hfiniteH : ∀ i, Finite (H i) := by
intro i
exact FiniteGroupClass.finite (hH i)
letI : ∀ i, Finite (H i) := hfiniteH
have hCH : ∀ i, C (H i) := fun i =>
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1
(hH i)
have hCG : C G := hForm.finiteSubdirectProductClosed f hf hsurj hCH
letI : Finite G := Finite.of_injective f hf
exact
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).2 hCGFormation data transfers from a finite-group class \(C\) to the finite quotient class induced by \(\mathrm{finiteGroupClassProCPredicate}\,C\).
def finiteQuotientFullFormation_finiteGroupClassProCPredicate
(C : FiniteGroupClass.{u}) (hFull : FiniteGroupClass.FullFormation C) :
(ProCGroups.ProC.finiteGroupClassProCPredicate C).HasFiniteQuotientFullFormation where
fullFormation := by
let hForm : FiniteGroupClass.Formation C := hFull.melnikovFormation.formation
refine
{ melnikovFormation :=
{ formation :=
(finiteQuotientFormation_finiteGroupClassProCPredicate C hForm).formation
normalSubgroupClosed := ?_
extensionClosed := ?_ }
subgroupClosed := ?_ }
· intro G _ N _ hG
letI : Finite G := FiniteGroupClass.finite hG
have hCG : C G :=
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hG
have hCN : C N := hFull.melnikovFormation.normalSubgroupClosed N hCG
letI : Finite N := FiniteGroupClass.finite hCN
exact
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).2 hCN
· intro E _ N _ hN hQ
letI : Finite N := FiniteGroupClass.finite hN
letI : Finite (E ⧸ N) := FiniteGroupClass.finite hQ
have hCN : C N :=
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hN
have hCQ : C (E ⧸ N) :=
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hQ
have hCE : C E := hFull.melnikovFormation.extensionClosed N hCN hCQ
letI : Finite E := FiniteGroupClass.finite hCE
exact
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).2 hCE
· intro G _ H hG
letI : Finite G := FiniteGroupClass.finite hG
have hCG : C G :=
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hG
have hCH : C H := hFull.subgroupClosed H hCG
letI : Finite H := FiniteGroupClass.finite hCH
exact
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).2 hCHThis declaration transfers full formation data from a finite-group class \(C\) to the finite quotient class induced by \(\mathrm{finiteGroupClassProCPredicate}\,C\).
def determinedByFiniteQuotients_finiteGroupClassProCPredicate
(C : FiniteGroupClass.{u}) (hForm : FiniteGroupClass.Formation C) :
(ProCGroups.ProC.finiteGroupClassProCPredicate C).DeterminedByFiniteQuotients where
holds_of_isProCGroup := by
intro G _ _ _ hG
refine ⟨hG.isProfinite, ?_⟩
intro W hW h1W
rcases hG.hasOpenNormalBasisInClass W hW h1W with ⟨U, hUW, hCU⟩
have hfinite : Finite (G ⧸ (U : Subgroup G)) := FiniteGroupClass.finite hCU
letI : Finite (G ⧸ (U : Subgroup G)) := hfinite
exact ⟨U, hUW,
(finiteQuotientClass_finiteGroupClassProCPredicate_iff
hForm.quotientClosed hForm.isomClosed).1 hCU⟩A finite-class pro-\(C\) predicate is determined by its finite quotient class whenever \(C\) is a formation.
def procyclicProC : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.cyclicThe standard procyclic predicate defines a pro-\(C\) class.
def proabelianProC : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.abelianThe standard pro-abelian predicate defines a pro-\(C\) class.
def pronilpotentProC : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.nilpotentThe standard pronilpotent predicate defines a pro-\(C\) class.
def prosolvableProC : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate FiniteGroupClass.solvableThe standard prosolvable predicate defines a pro-\(C\) class.
def proPProC (p : ℕ) : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.pGroup p)The standard pro-\(p\) predicate defines a pro-\(C\) class.
def proSigmaProC (sigma : Set ℕ) : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.sigmaGroup sigma)Pro-\(\Sigma\) groups, for a set \(\Sigma\) of primes.
theorem proSigmaProC_finiteQuotientClass_iff
{sigma : Set ℕ} {Q : Type u} [Group Q] [Finite Q] :
(proSigmaProC sigma).finiteQuotientClass Q ↔
FiniteGroupClass.sigmaGroup sigma QOn finite groups, the finite quotient class of \(\mathrm{proSigmaProC}\) is exactly \(\mathrm{sigmaGroup}\).
Show proof
by
simpa [proSigmaProC] using
(ProCGroupPredicate.finiteQuotientClass_finiteGroupClassProCPredicate_iff
(FiniteGroupClass.sigmaGroup_quotientClosed sigma)
(FiniteGroupClass.sigmaGroup_isomClosed sigma)
(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.
□def abelianExponentProC (n : ℕ) : ProCGroupPredicate.{u} :=
ProCGroups.ProC.finiteGroupClassProCPredicate (FiniteGroupClass.abelianExponent n)instance proabelianProC_hasFiniteQuotientFormation :
ProCGroupPredicate.HasFiniteQuotientFormation
(proabelianProC : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
FiniteGroupClass.abelian FiniteGroupClass.abelian_formationThe pro-abelian predicate is stable under the finite-quotient formation operations.
instance proabelianProC_determinedByFiniteQuotients :
ProCGroupPredicate.DeterminedByFiniteQuotients
(proabelianProC : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
FiniteGroupClass.abelian FiniteGroupClass.abelian_formationinstance proPProC_hasFiniteQuotientFormation (p : ℕ) :
ProCGroupPredicate.HasFiniteQuotientFormation
(proPProC p : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
(FiniteGroupClass.pGroup p) (FiniteGroupClass.pGroup_formation p)The pro-\(p\) predicate is stable under the finite-quotient formation operations.
instance proPProC_determinedByFiniteQuotients (p : ℕ) :
ProCGroupPredicate.DeterminedByFiniteQuotients
(proPProC p : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
(FiniteGroupClass.pGroup p) (FiniteGroupClass.pGroup_formation p)The pro-\(p\) predicate is determined by its finite quotients.
instance proSigmaProC_hasFiniteQuotientFormation (sigma : Set ℕ) :
ProCGroupPredicate.HasFiniteQuotientFormation
(proSigmaProC sigma : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
(FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_formation sigma)The pro-\(\Sigma\) predicate is stable under the finite-quotient formation operations.
instance proSigmaProC_hasFiniteQuotientFullFormation (sigma : Set ℕ) :
ProCGroupPredicate.HasFiniteQuotientFullFormation
(proSigmaProC sigma : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.finiteQuotientFullFormation_finiteGroupClassProCPredicate
(FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_fullFormation sigma)The pro-\(\Sigma\) predicate has the full finite quotient formation structure.
instance proSigmaProC_determinedByFiniteQuotients (sigma : Set ℕ) :
ProCGroupPredicate.DeterminedByFiniteQuotients
(proSigmaProC sigma : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
(FiniteGroupClass.sigmaGroup sigma) (FiniteGroupClass.sigmaGroup_formation sigma)The pro-\(\Sigma\) predicate is determined by its finite quotients.
instance abelianExponentProC_hasFiniteQuotientFormation (n : ℕ) :
ProCGroupPredicate.HasFiniteQuotientFormation
(abelianExponentProC n : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.finiteQuotientFormation_finiteGroupClassProCPredicate
(FiniteGroupClass.abelianExponent n) (FiniteGroupClass.abelianExponent_formation n)The bounded-exponent abelian predicate is stable under finite-quotient formation operations.
instance abelianExponentProC_determinedByFiniteQuotients (n : ℕ) :
ProCGroupPredicate.DeterminedByFiniteQuotients
(abelianExponentProC n : ProCGroupPredicate.{u}) :=
ProCGroupPredicate.determinedByFiniteQuotients_finiteGroupClassProCPredicate
(FiniteGroupClass.abelianExponent n) (FiniteGroupClass.abelianExponent_formation n)theorem procyclicProC_holds_iff
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
procyclicProC (G := G) ↔ IsProcyclicGroup GThe named procyclic predicate unfolds to \(\mathrm{IsProcyclicGroup}\).
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. 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 proabelianProC_holds_iff
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
proabelianProC (G := G) ↔ IsProabelianGroup GThe named pro-abelian predicate unfolds to \(\mathrm{IsProabelianGroup}\).
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. 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 pronilpotentProC_holds_iff
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
pronilpotentProC (G := G) ↔ IsPronilpotentGroup GThe named pronilpotent predicate is equivalent to IsPronilpotentGroup.
Show proof
by
constructor
· exact isPronilpotentGroup_of_isProC_nilpotent
· exact IsPronilpotentGroup.toIsProC_nilpotentProof. 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously. 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 prosolvableProC_holds_iff
{G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
prosolvableProC (G := G) ↔ IsProsolvableGroup GThe named prosolvable predicate is equivalent to IsProsolvableGroup.
Show proof
by
constructor
· exact isProsolvableGroup_of_isProC_solvable
· exact IsProsolvableGroup.toIsProC_solvableProof. 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 equivalence and homeomorphism statements, the two comparison maps are composed in both orders and evaluated on the coordinates that determine the source. Each composite reduces to the identity transition or to the chosen representative identity on finite stages, so the algebraic inverse laws and the topological inverse laws follow simultaneously. 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 proPProC_holds_iff
{p : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
proPProC p (G := G) ↔ IsProPGroup p GThe named pro-\(p\) predicate unfolds to \(\mathrm{IsProPGroup}\).
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. 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 proSigmaProC_holds_iff
{sigma : Set ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
proSigmaProC sigma (G := G) ↔ IsProSigmaGroup sigma GThe named pro-\(\Sigma\) predicate unfolds to \(\mathrm{IsProSigmaGroup}\).
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. 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. 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. 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 abelianExponentProC_holds_iff
{n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] :
abelianExponentProC n (G := G) ↔
IsProCGroup (FiniteGroupClass.abelianExponent n) GThe named bounded-exponent abelian predicate unfolds to the corresponding concrete pro-\(C\) condition.
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. 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 isPronilpotentGroup (hG : IsProPGroup p G) : IsPronilpotentGroup GA pro-\(p\) group is pronilpotent.
Show proof
by
letI : IsTopologicalGroup G := hG.isTopologicalGroup
refine ⟨hG.isProfinite, ?_⟩
intro U
exact
(FiniteGroupClass.pGroup_to_nilpotent (p := p)
(hG.quotient_mem (FiniteGroupClass.pGroup_formation p) U)).2Proof. 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 isProsolvableGroup (hG : IsProPGroup p G) : IsProsolvableGroup GA pro-\(p\) group is prosolvable.
Show proof
by
letI : IsTopologicalGroup G := hG.isTopologicalGroup
refine ⟨hG.isProfinite, ?_⟩
intro U
exact
(FiniteGroupClass.pGroup_to_solvable (p := p)
(hG.quotient_mem (FiniteGroupClass.pGroup_formation p) U)).2Proof. 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.
□