ProCGroups.FreeProC.Constructions
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.
import
theorem maximalQuotientOfPointedFree_is_pointedFree
{ProC' : ProCGroupPredicate}
(hmono :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
ProC' (G := G) → ProC (G := G))
{X : Type u} [TopologicalSpace X] {x0 : X}
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{Q : Type u} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
{ι : X → F}
(hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
(π : F →* Q) (hπ : IsMaximalProCQuotient ProC' π) :
IsPointedFreeProCGroupOn (ProC := ProC') X x0 Q (fun x => π (ι x))A maximal pro-\(C'\) quotient of a pointed free pro-\(C\) group is again pointed free on the same pointed space. This version fixes a chosen maximal quotient map \(\pi : F \to Q\) and includes the explicit class-inclusion hypothesis \(\mathrm{ProC}' \mapsto \mathrm{ProC}\).
Show proof
by
refine ⟨hπ.isProC, hπ.continuous_π.comp hF.continuous_ι, ?_, ?_, ?_⟩
· simp only [hF.map_base, map_one]
· have himage : π '' Set.range ι = Set.range (fun x => π (ι x)) := by
simpa [Function.comp] using (Set.range_comp π ι).symm
simpa [himage] using
(Generation.topologicallyGenerates_image_of_continuousSurjective
(G := F) (H := Q) π hπ.continuous_π hπ.surjective_π hF.generates_range)
· intro G _ _ _ hG φ hφ hφ0 hgen
have hG' : ProC (G := G) := hmono hG
rcases hF.existsUnique_lift hG' φ hφ hφ0 hgen with ⟨f, hfprop, hfuniq⟩
rcases hπ.existsUnique_lift hG f hfprop.1 with ⟨q, hqprop, hquniq⟩
refine ⟨q, ?_, ?_⟩
· refine ⟨hqprop.1, ?_⟩
intro x
have hcomp_eval := congrArg (fun ψ : F →* G => ψ (ι x)) hqprop.2
simpa [MonoidHom.comp_apply, hfprop.2 x] using hcomp_eval
· intro q' hq'
have hq'comp :
q'.comp π = f := by
apply hfuniq
refine ⟨hq'.1.comp hπ.continuous_π, ?_⟩
intro x
simpa [MonoidHom.comp_apply] using hq'.2 x
exact hquniq q' ⟨hq'.1, hq'comp⟩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 kernel_of_pointedFree_map_isPerfect
{ProCe : ProCGroupPredicate}
(hmono :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
ProC (G := G) → ProCe (G := G))
{X : Type u} [TopologicalSpace X] {x0 : X}
{Fe : Type u} [Group Fe] [TopologicalSpace Fe] [IsTopologicalGroup Fe]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ιe : X → Fe} {ι : X → F}
(hFe : IsPointedFreeProCGroupOn (ProC := ProCe) X x0 Fe ιe)
(hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
(φ : Fe →* F) (hφ : Continuous φ)
(hcompat : ∀ x, φ (ιe x) = ι x)
(hquot : ProC (G := Fe ⧸ ⁅φ.ker, φ.ker⁆)) :
ProCGroups.NormalSubgroups.IsPerfectSubgroup φ.kerUnder the explicit quotient hypothesis, the kernel of the natural map from a pointed free pro-\(C_e\) model to a pointed free pro-\(C\) model is perfect.
Show proof
by
let K : Subgroup Fe := φ.ker
let q : Fe →* Fe ⧸ ⁅K, K⁆ := QuotientGroup.mk' ⁅K, K⁆
let ψ : X → Fe ⧸ ⁅K, K⁆ := fun x => q (ιe x)
have hψ : Continuous ψ := continuous_quotient_mk'.comp hFe.continuous_ι
have hψ0 : ψ x0 = 1 := by
simp only [QuotientGroup.mk'_apply, hFe.map_base, QuotientGroup.mk_one, ψ, q]
have himage : q '' Set.range ιe = Set.range ψ := by
simpa [ψ, q, Function.comp] using (Set.range_comp q ιe).symm
have hgenψ : Generation.TopologicallyGenerates (G := Fe ⧸ ⁅K, K⁆) (Set.range ψ) := by
simpa [himage] using
(Generation.topologicallyGenerates_image_of_continuousSurjective
(G := Fe) (H := Fe ⧸ ⁅K, K⁆) q continuous_quotient_mk'
(QuotientGroup.mk'_surjective ⁅K, K⁆) hFe.generates_range)
rcases hF.existsUnique_lift hquot ψ hψ hψ0 hgenψ with ⟨σ, hσ, _⟩
have hquot_e : ProCe (G := Fe ⧸ ⁅K, K⁆) := hmono hquot
rcases hFe.existsUnique_lift hquot_e ψ hψ hψ0 hgenψ with ⟨τ, hτ, hτuniq⟩
have hq_eq : q = τ := by
exact hτuniq q ⟨continuous_quotient_mk', fun x => rfl⟩
have hσφ_eq : σ.comp φ = τ := by
refine hτuniq (σ.comp φ) ⟨hσ.1.comp hφ, ?_⟩
intro x
calc
(σ.comp φ) (ιe x) = σ (ι x) := by
simp only [MonoidHom.comp_apply, hcompat x]
_ = ψ x := hσ.2 x
have hfac : σ.comp φ = q := hσφ_eq.trans hq_eq.symm
have hKle : K ≤ ⁅K, K⁆ := by
intro k hk
have hkφ : φ k = 1 := by
simpa [K, MonoidHom.mem_ker] using hk
have hqk : q k = 1 := by
rw [← DFunLike.congr_fun hfac k]
simp only [MonoidHom.comp_apply, hkφ, map_one]
exact (QuotientGroup.eq_one_iff (N := ⁅K, K⁆) k).1 hqk
simpa [K, ProCGroups.NormalSubgroups.IsPerfectSubgroup] using
(le_antisymm (Subgroup.commutator_le_self K) hKle)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. 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 kernel_of_pointedFree_map_isPerfect_of_closedUnderCommutatorKernelQuotientsFrom
{ProCe : ProCGroupPredicate}
[ProC.ClosedUnderCommutatorKernelQuotientsFrom ProCe]
(hmono :
∀ {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G],
ProC (G := G) → ProCe (G := G))
{X : Type u} [TopologicalSpace X] {x0 : X}
{Fe : Type u} [Group Fe] [TopologicalSpace Fe] [IsTopologicalGroup Fe]
{F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
{ιe : X → Fe} {ι : X → F}
(hFe : IsPointedFreeProCGroupOn (ProC := ProCe) X x0 Fe ιe)
(hF : IsPointedFreeProCGroupOn (ProC := ProC) X x0 F ι)
(φ : Fe →* F) (hφ : Continuous φ)
(hcompat : ∀ x, φ (ιe x) = ι x) :
ProCGroups.NormalSubgroups.IsPerfectSubgroup φ.kerThe perfect-kernel statement using pro-\(C\) permanence data to build the commutator-kernel quotient internally.
Show proof
by
let φₜ : Fe →ₜ* F := { toMonoidHom := φ, continuous_toFun := hφ }
have hquot : ProC (G := Fe ⧸ ⁅φ.ker, φ.ker⁆) := by
simpa [φₜ] using
(ProCGroupPredicate.quotient_by_kernel_commutator
(Target := ProC) (Source := ProCe) φₜ hFe.isProC hF.isProC)
exact
kernel_of_pointedFree_map_isPerfect
(ProC := ProC) (ProCe := ProCe) hmono hFe hF φ hφ hcompat hquotProof. 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. 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.
□