ProCGroups.FreeProC.SolvableQuotients
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
noncomputable def collapseToFinsetQuot
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
(S : Finset ι) (m : ℕ) :
MaxSolvQuot F m →ₜ* MaxSolvQuot F m :=
ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinset S) mThe endomorphism induced by collapseToFinset on a maximal solvable quotient.
theorem comp_collapseToFinsetQuot_eq_of_eq_one_outside
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
{H : Type w} [TopologicalSpace H] [Group H] [IsTopologicalGroup H] [T2Space H]
(S : Finset ι) (m : ℕ) (φ : MaxSolvQuot F m →ₜ* H)
(hφ : ∀ j, j ∉ S → φ (continuousToMaxSolvQuot F m (X j)) = 1) :
φ.comp (collapseToFinsetQuot X hFree S m) = φOn the quotient, composing with \(\mathrm{collapseToFinsetQuot}\) leaves a map that is trivial outside \(S\) unchanged.
Show proof
by
let ψ : F →ₜ* H := φ.comp (continuousToMaxSolvQuot F m)
have hψ :
ψ.comp (hFree.collapseToFinset S) = ψ := by
exact
hFree.comp_collapseToFinset_eq_of_eq_one_outside ψ S (by
intro j hj
exact hφ j hj)
ext q
obtain ⟨x, rfl⟩ := continuousToMaxSolvQuot_surjective (G := F) m q
change ψ (hFree.collapseToFinset S x) = ψ x
exact congrArg (fun f : F →ₜ* H => f x) hψ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. 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.
□noncomputable def finsetSupportRangeQuot
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
(S : Finset ι) (m : ℕ) :
MaxSolvQuot F m →ₜ* MaxSolvQuot (hFree.FinsetSupportRetract S) m :=
ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinsetRange S) mnoncomputable def finsetSupportInclusionQuot
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
(S : Finset ι) (m : ℕ) :
MaxSolvQuot (hFree.FinsetSupportRetract S) m →ₜ* MaxSolvQuot F m :=
ProCGroups.FiniteStepSolvableQuotients.topMaxSolvQuotMap (hFree.collapseToFinsetInclusion S) mtheorem finsetSupportRangeQuot_apply
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
(S : Finset ι) (m : ℕ) (x : F) :
finsetSupportRangeQuot X hFree S m (continuousToMaxSolvQuot F m x) =
continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m
(hFree.collapseToFinsetRange S x)The map is evaluated on an element by its defining coordinate formula.
Show proof
by
change
QuotientGroup.map
(N := topDerivedTop F m)
(M := topDerivedTop (hFree.FinsetSupportRetract S) m)
(f := (hFree.collapseToFinsetRange S : F →* hFree.FinsetSupportRetract S))
(ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_le_comap
(G := F) (Q := hFree.FinsetSupportRetract S) (f := hFree.collapseToFinsetRange S) m)
((QuotientGroup.mk' (topDerivedTop F m)) x) =
(QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m))
(hFree.collapseToFinsetRange S x)
rw [QuotientGroup.map_mk']
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. 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 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 finsetSupportInclusionQuot_apply
{ι : Type v} [DecidableEq ι] (X : ι → F)
(hFree : IsFreeProCGroupOnConvergingSet
(ProC := ProCGroups.ProC.finiteGroupClassProCPredicate C) ι F X)
(S : Finset ι) (m : ℕ) (x : hFree.FinsetSupportRetract S) :
finsetSupportInclusionQuot X hFree S m
(continuousToMaxSolvQuot (hFree.FinsetSupportRetract S) m x) =
continuousToMaxSolvQuot F m (hFree.collapseToFinsetInclusion S x)The map is evaluated on an element by its defining coordinate formula.
Show proof
by
change
QuotientGroup.map
(N := topDerivedTop (hFree.FinsetSupportRetract S) m)
(M := topDerivedTop F m)
(f := (hFree.collapseToFinsetInclusion S : hFree.FinsetSupportRetract S →* F))
(ProCGroups.FiniteStepSolvableQuotients.topDerivedTop_le_comap
(G := hFree.FinsetSupportRetract S) (Q := F)
(f := hFree.collapseToFinsetInclusion S) m)
((QuotientGroup.mk' (topDerivedTop (hFree.FinsetSupportRetract S) m)) x) =
(QuotientGroup.mk' (topDerivedTop F m)) (hFree.collapseToFinsetInclusion S x)
rw [QuotientGroup.map_mk']
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. 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 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.
□