ProCGroups.ProC.Quotients.OpenSubgroupSections
This module supplies the topological part of the construction. It checks continuity and stagewise neighborhood properties so that the completed object inherits the required topology.
import
- Mathlib.Topology.Algebra.ProperAction.Basic
- ProCGroups.ProC.Quotients.ClosedSubgroupNeighborhoods
noncomputable def quotientOpenSubgroupSection (U : Subgroup G) :
(G ⧸ U) → G := by
classical
intro q
exact if hq : q = QuotientGroup.mk (s := U) (1 : G) then 1
else Classical.choose (Quotient.exists_rep q)A normalized set-theoretic section of the quotient map by an open subgroup. Since the quotient is discrete, this section is automatically continuous.
@[simp] theorem quotientOpenSubgroupSection_one
(U : Subgroup G) :
quotientOpenSubgroupSection U (QuotientGroup.mk (s := U) (1 : G)) = 1The normalized set-theoretic section sends the identity coset to the identity.
Show proof
by
classical
simp only [quotientOpenSubgroupSection, ↓reduceDIte]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. 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 quotientOpenSubgroupSection_rightInverse
(U : Subgroup G) :
Function.RightInverse (quotientOpenSubgroupSection U)
(QuotientGroup.mk (s := U))The normalized section is a genuine right inverse to the quotient map.
Show proof
by
classical
intro q
by_cases hq : q = QuotientGroup.mk (s := U) (1 : G)
· subst hq
simp only [quotientOpenSubgroupSection, ↓reduceDIte]
· simpa [quotientOpenSubgroupSection, hq] using
(Classical.choose_spec (Quotient.exists_rep 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. 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 continuous_quotientOpenSubgroupSection
[TopologicalSpace G]
[IsTopologicalGroup G]
(U : Subgroup G) (hU : IsOpen (U : Set G)) :
Continuous (quotientOpenSubgroupSection U)The normalized section by an open subgroup is continuous because the quotient is discrete.
Show proof
by
letI : ContinuousMul G := (‹IsTopologicalGroup G›).toContinuousMul
letI : ContinuousInv G := (‹IsTopologicalGroup G›).toContinuousInv
letI : DiscreteTopology (G ⧸ U) := QuotientGroup.discreteTopology hU
simpa using
(continuous_of_discreteTopology :
Continuous (quotientOpenSubgroupSection U))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. 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. 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. 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 quotient_openNormalSubgroup_hasContinuousSection
[TopologicalSpace G]
[IsTopologicalGroup G]
(U : OpenNormalSubgroup G) :
∃ σ : (G ⧸ (U : Subgroup G)) → G,
Continuous σ ∧
Function.RightInverse σ (QuotientGroup.mk' (U : Subgroup G)) ∧
σ 1 = 1Helper for the finite/open case: the canonical quotient map by an open normal subgroup of a profinite group admits a continuous section normalized by \(s(1)=1\). The actual section data is provided by quotientOpenSubgroupSection.
Show proof
by
let hU : IsOpen ((U : Subgroup G) : Set G) := openNormalSubgroup_isOpen (G := G) U
refine ⟨quotientOpenSubgroupSection (U : Subgroup G), ?_, ?_, ?_⟩
· simpa using continuous_quotientOpenSubgroupSection (G := G) (U : Subgroup G) hU
· simpa [QuotientGroup.mk'] using
quotientOpenSubgroupSection_rightInverse (G := G) (U : Subgroup G)
· simpa using quotientOpenSubgroupSection_one (G := 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. 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. 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. 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 leftQuotientProjection_hasContinuousSection_of_openSubgroup
[TopologicalSpace G]
[IsTopologicalGroup G]
(hG : IsProfiniteGroup G) (K H : ClosedSubgroup G)
(hKH : (K : Subgroup G) ≤ (H : Subgroup G))
(hKopen : IsOpen (((K : Subgroup G).subgroupOf (H : Subgroup G)) : Set H)) :
∃ σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G),
Continuous σ ∧
Function.RightInverse σ
(leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH) ∧
σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
QuotientGroup.mk (s := (K : Subgroup G)) (1 : G)Finite-index case of the section theorem for left quotient projections.
Show proof
by
classical
letI : ContinuousMul G := (‹IsTopologicalGroup G›).toContinuousMul
letI : ContinuousInv G := (‹IsTopologicalGroup G›).toContinuousInv
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : IsClosed (((K : ClosedSubgroup G) : Subgroup G) : Set G) := K.isClosed'
letI : IsClosed (((H : ClosedSubgroup G) : Subgroup G) : Set G) := H.isClosed'
let UH : OpenSubgroup H :=
⟨((K : Subgroup G).subgroupOf (H : Subgroup G)), hKopen⟩
obtain ⟨V, hVHK⟩ :=
exists_openNormalSubgroup_inter_closedSubgroup_le (G := G) hG H UH
have hVcapHK : ((V : Subgroup G) ⊓ (H : Subgroup G)) ≤ (K : Subgroup G) := by
intro x hx
exact hVHK <| show (⟨x, hx.2⟩ : H) ∈
(OpenNormalSubgroup.comap ((H : Subgroup G).subtype) continuous_subtype_val V : Subgroup H)
by simpa using hx.1
let J : Subgroup G := (H : Subgroup G) ⊔ (V : Subgroup G)
have hHJ : (H : Subgroup G) ≤ J := le_sup_left
have hKJ : (K : Subgroup G) ≤ J := hKH.trans hHJ
have hJopen : IsOpen (J : Set G) := by
exact Subgroup.isOpen_of_openSubgroup J (show (V : Subgroup G) ≤ J from le_sup_right)
let ρ : G ⧸ J → G := quotientOpenSubgroupSection J
have hρcont : Continuous ρ := continuous_quotientOpenSubgroupSection J hJopen
have hρright : Function.RightInverse ρ (QuotientGroup.mk (s := J)) :=
quotientOpenSubgroupSection_rightInverse J
let WK : Set (G ⧸ (K : Subgroup G)) :=
(QuotientGroup.mk (s := (K : Subgroup G))) ''
((((V : OpenNormalSubgroup G) : Subgroup G) : Set G))
let BH : Set (G ⧸ (H : Subgroup G)) :=
(QuotientGroup.mk (s := (H : Subgroup G))) ''
((((V : OpenNormalSubgroup G) : Subgroup G) : Set G))
have hVclosed : IsClosed ((((V : OpenNormalSubgroup G) : Subgroup G) : Set G)) :=
openNormalSubgroup_isClosed (G := G) V
have hWKcompact : IsCompact WK := by
exact hVclosed.isCompact.image (QuotientGroup.continuous_mk :
Continuous (QuotientGroup.mk (s := (K : Subgroup G)) : G → G ⧸ (K : Subgroup G)))
have hBHcompact : IsCompact BH := by
exact hVclosed.isCompact.image (QuotientGroup.continuous_mk :
Continuous (QuotientGroup.mk (s := (H : Subgroup G)) : G → G ⧸ (H : Subgroup G)))
have hBHclosed : IsClosed BH := by
exact hBHcompact.isClosed
let πloc : WK → BH := fun x =>
⟨leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH x.1, by
rcases x with ⟨x, hx⟩
rcases hx with ⟨g, hg, rfl⟩
exact ⟨g, hg, rfl⟩⟩
have hπloc_continuous : Continuous πloc := by
exact Continuous.subtype_mk
((continuous_leftQuotientProjection
(K : Subgroup G) (H : Subgroup G) hKH).comp continuous_subtype_val)
(by
rintro ⟨x, hx⟩
rcases hx with ⟨g, hg, rfl⟩
exact ⟨g, hg, rfl⟩)
have hπloc_bij : Function.Bijective πloc := by
constructor
· intro x y hxy
rcases x with ⟨x, hx⟩
rcases y with ⟨y, hy⟩
rcases hx with ⟨gx, hgx, rfl⟩
rcases hy with ⟨gy, hgy, rfl⟩
apply Subtype.ext
apply QuotientGroup.eq.2
have hHmem : gx⁻¹ * gy ∈ (H : Subgroup G) := by
exact QuotientGroup.eq.1 (congrArg Subtype.val hxy)
have hVmem : gx⁻¹ * gy ∈ (V : Subgroup G) := by
exact (V : Subgroup G).mul_mem ((V : Subgroup G).inv_mem hgx) hgy
exact hVcapHK ⟨hVmem, hHmem⟩
· intro y
rcases y with ⟨y, hy⟩
rcases hy with ⟨g, hg, rfl⟩
refine ⟨⟨QuotientGroup.mk (s := (K : Subgroup G)) g, ⟨g, hg, rfl⟩⟩, ?_⟩
apply Subtype.ext
rfl
letI : CompactSpace WK := isCompact_iff_compactSpace.mp hWKcompact
let eTop : WK ≃ₜ BH := hπloc_continuous.homeoOfBijectiveCompactToT2 hπloc_bij
let σB : BH → G ⧸ (K : Subgroup G) := fun y => (eTop.symm y).1
have hσB_continuous : Continuous σB := continuous_subtype_val.comp eTop.continuous_invFun
have hσB_right : ∀ y : BH,
leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σB y) = y.1 := by
intro y
exact congrArg Subtype.val (eTop.right_inv y)
have hσB_one :
σB ⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩ =
QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := by
let y0 : BH :=
⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩
have hσB_mem : σB y0 ∈ WK := (eTop.symm y0).2
have h1_mem : QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) ∈ WK := ⟨1, V.one_mem', rfl⟩
have hs : (⟨σB y0, hσB_mem⟩ : WK) =
⟨QuotientGroup.mk (s := (K : Subgroup G)) (1 : G), h1_mem⟩ := by
apply hπloc_bij.1
apply Subtype.ext
simpa [πloc, y0] using hσB_right y0
exact congrArg Subtype.val hs
let c : G ⧸ (H : Subgroup G) → G ⧸ J :=
leftQuotientProjection (H : Subgroup G) J hHJ
have hc_continuous : Continuous c :=
continuous_leftQuotientProjection (H : Subgroup G) J hHJ
let r : G ⧸ (H : Subgroup G) → G := ρ ∘ c
have hr_continuous : Continuous r := hρcont.comp hc_continuous
let z : G ⧸ (H : Subgroup G) → BH := fun y =>
⟨(r y)⁻¹ • y, by
rcases Quotient.exists_rep y with ⟨g, rfl⟩
change
QuotientGroup.mk (s := (H : Subgroup G))
((r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g) ∈
BH
have hsame :
QuotientGroup.mk (s := J) (r (QuotientGroup.mk (s := (H : Subgroup G)) g)) =
QuotientGroup.mk (s := J) g := by
simpa [r, c, Function.comp] using
hρright (leftQuotientProjection (H : Subgroup G) J hHJ
(QuotientGroup.mk (s := (H : Subgroup G)) g))
have hmemJ :
(r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈ J := by
exact QuotientGroup.eq.1 hsame
have hmemJ' :
(r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈
(H : Subgroup G) ⊔ (V : Subgroup G) := by
simpa [J] using hmemJ
have hmemJ'' :
(r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈
(V : Subgroup G) ⊔ (H : Subgroup G) := by
simpa [sup_comm] using hmemJ'
have hmemSet :
(r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈
((V : Subgroup G) : Set G) * ((H : Subgroup G) : Set G) := by
change (r (QuotientGroup.mk (s := (H : Subgroup G)) g))⁻¹ * g ∈
(((V : Subgroup G) ⊔ (H : Subgroup G) : Subgroup G) : Set G) at hmemJ''
rwa [Subgroup.normal_mul (V : Subgroup G) (H : Subgroup G)] at hmemJ''
rcases hmemSet with ⟨v, hv, h, hh, hEq⟩
refine ⟨v, hv, ?_⟩
rw [← hEq]
exact (QuotientGroup.mk_mul_of_mem v hh).symm⟩
have hz_continuous : Continuous z := by
exact Continuous.subtype_mk ((continuous_inv.comp hr_continuous).smul continuous_id) (by
intro y
exact (z y).2)
let σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G) := fun y =>
r y • σB (z y)
have hσ_continuous : Continuous σ := by
exact hr_continuous.smul (hσB_continuous.comp hz_continuous)
refine ⟨σ, hσ_continuous, ?_, ?_⟩
· intro y
calc
leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σ y)
= r y • leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σB (z y)) := by
simp only [leftQuotientProjection_smul, σ]
_ = r y • (z y).1 := by rw [hσB_right]
_ = y := by
change r y • ((r y)⁻¹ • y) = y
simp only [smul_smul, mul_inv_cancel, one_smul]
· have hc_one :
c (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
QuotientGroup.mk (s := J) (1 : G) := rfl
have hr_one : r (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) = 1 := by
exact quotientOpenSubgroupSection_one J
have hz_one :
z (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
⟨QuotientGroup.mk (s := (H : Subgroup G)) (1 : G), ⟨1, V.one_mem', rfl⟩⟩ := by
apply Subtype.ext
simp only [hr_one, inv_one, one_smul, z]
simp only [hr_one, hz_one, hσB_one, one_smul, σ]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. 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. 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. 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.
□