ProCGroups.ProC.Quotients.LeftQuotientProjectionSections
This module studies left quotient projection sections for pro cgroups. If an intermediate closed subgroup is not contained in the base subgroup, one can choose an element in the set-theoretic difference. This is the witness extraction used in the Zorn maximality argument.
import
theorem exists_mem_of_not_le {G : Type u} [Group G] [TopologicalSpace G] {K L : ClosedSubgroup G}
(hnotle : ¬ (L : Subgroup G) ≤ (K : Subgroup G)) :
∃ x : G, x ∈ (L : Subgroup G) ∧ x ∉ (K : Subgroup G)If an intermediate closed subgroup is not contained in the base subgroup, one can choose an element in the set-theoretic difference. This is the witness extraction used in the Zorn maximality argument.
Show proof
by
by_contra hNo
apply hnotle
intro x hxL
by_cases hxK : x ∈ (K : Set G)
· exact hxK
· exact False.elim (hNo ⟨x, hxL, hxK⟩)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. 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 exists_openNormalSubgroup_not_mem
(hG : IsProfiniteGroup G) {x : G} (hx : x ≠ 1) :
∃ U : OpenNormalSubgroup G, x ∉ (U : Subgroup G)For any nontrivial element of a profinite group, there is an open normal subgroup that does not contain it.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
let W : Set G := ({x} : Set G)ᶜ
have hW : IsOpen W := by
simp only [isOpen_compl_iff, finite_singleton, Finite.isClosed, W]
have h1W : (1 : G) ∈ W := by
simpa [W] using hx.symm
obtain ⟨U, hUW⟩ :=
exists_openNormalSubgroup_sub_open_nhds_of_one (G := G) hW h1W
refine ⟨U, ?_⟩
intro hxU
exact hx <| by
have hxW : x ∈ W := hUW hxU
simp only [mem_compl_iff, 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. 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 exists_openSubgroup_ge_closedSubgroup_not_mem
(hG : IsProfiniteGroup G) (K : ClosedSubgroup G) {x : G} (hx : x ∉ (K : Set G)) :
∃ U : OpenSubgroup G, (K : Subgroup G) ≤ (U : Subgroup G) ∧ x ∉ (U : Set G)A point outside a closed subgroup of a profinite group is omitted by some open subgroup containing that closed subgroup.
Show proof
by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : TotallyDisconnectedSpace G := IsProfiniteGroup.totallyDisconnectedSpace hG
have hxInf :
x ∉ sInf {N : Subgroup G | IsOpen (N : Set G) ∧ (K : Subgroup G) ≤ N} := by
rw [← closedSubgroup_eq_sInf_open (G := G) K]
exact hx
rw [Subgroup.mem_sInf] at hxInf
push_neg at hxInf
rcases hxInf with ⟨U, hU, hxU⟩
exact ⟨⟨U, hU.1⟩, hU.2, hxU⟩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. 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.
□noncomputable def closedSubgroupOfOpenSubgroup
(hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
ClosedSubgroup G where
toSubgroup := (N : Subgroup T).map ((T : Subgroup G).subtype)
isClosed' := by
letI : IsTopologicalGroup ↥(T : Subgroup G) := by infer_instance
let hT : IsProfiniteGroup T := IsProfiniteGroup.of_closedSubgroup (G := G) hG T
letI : CompactSpace T := IsProfiniteGroup.compactSpace hT
letI : T2Space G := IsProfiniteGroup.t2Space hG
have hNclosed : IsClosed ((N : Subgroup T) : Set T) :=
Subgroup.isClosed_of_isOpen (N : Subgroup T) N.isOpen'
have hNcompact : IsCompact ((N : Subgroup T) : Set T) := hNclosed.isCompact
have hEq :
((T : Subgroup G).subtype '' ((N : Subgroup T) : Set T)) =
(((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G) := by
ext x
constructor <;> rintro ⟨y, hy, rfl⟩ <;> exact ⟨y, hy, rfl⟩
change IsClosed ((((N : Subgroup T).map ((T : Subgroup G).subtype) : Subgroup G) : Set G))
rw [← hEq]
exact hNcompact.image continuous_subtype_val |>.isClosedAn open subgroup of a closed subgroup of a profinite group, viewed again as a closed subgroup of the ambient group.
@[simp] theorem mem_closedSubgroupOfOpenSubgroup
(hG : IsProfiniteGroup G) {T : ClosedSubgroup G} {N : OpenSubgroup T} {x : T} :
(x : G) ∈ (closedSubgroupOfOpenSubgroup (G := G) hG T N : Subgroup G) ↔
x ∈ (N : Subgroup T)Membership in the ambient closed subgroup induced by an open subgroup is tested inside the original subgroup.
Show proof
by
constructor
· intro hx
rcases hx with ⟨y, hy, hyx⟩
have : y = x := Subtype.ext hyx
simpa [this] using hy
· intro hx
exact ⟨x, hx, rfl⟩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\). 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 closedSubgroupOfOpenSubgroup_le
(hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
(closedSubgroupOfOpenSubgroup (G := G) hG T N : Subgroup G) ≤ (T : Subgroup G)The ambient closed subgroup attached to an open subgroup of T still lies inside T.
Show proof
by
intro x hx
rcases hx with ⟨y, hy, rfl⟩
exact y.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. 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.
□@[simp 900] theorem closedSubgroupOfOpenSubgroup_subgroupOf_eq
(hG : IsProfiniteGroup G) (T : ClosedSubgroup G) (N : OpenSubgroup T) :
(((closedSubgroupOfOpenSubgroup (G := G) hG T N : ClosedSubgroup G) : Subgroup G).subgroupOf
(T : Subgroup G)) = (N : Subgroup T)The closed subgroup obtained inside an open subgroup agrees with the corresponding subgroup of the ambient group.
Show proof
by
ext x
simp only [Subgroup.mem_subgroupOf, mem_closedSubgroupOfOpenSubgroup, OpenSubgroup.mem_toSubgroup]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\). 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.
□noncomputable def quotientBotHomeomorph (hG : IsProfiniteGroup G) :
G ≃ₜ G ⧸ (⊥ : Subgroup G) := by
letI : CompactSpace G := IsProfiniteGroup.compactSpace hG
letI : T2Space G := IsProfiniteGroup.t2Space hG
letI : IsClosed (((⊥ : Subgroup G) : Set G)) := by
change IsClosed ({(1 : G)} : Set G)
simp only [finite_singleton, Finite.isClosed]
exact Continuous.homeoOfBijectiveCompactToT2
(f := QuotientGroup.mk (s := (⊥ : Subgroup G)))
(by
simpa using
(QuotientGroup.continuous_mk : Continuous
(QuotientGroup.mk (s := (⊥ : Subgroup G)) : G → G ⧸ (⊥ : Subgroup G))))
(by
constructor
· intro x y hxy
have hmem : x⁻¹ * y ∈ (⊥ : Subgroup G) := QuotientGroup.eq.1 hxy
exact inv_mul_eq_one.mp <| by simpa using hmem
· intro q
rcases Quotient.exists_rep q with ⟨g, rfl⟩
exact ⟨g, rfl⟩)The canonical quotient map \(G \to G/\bot\) is a homeomorphism for profinite groups.
@[simp 900] theorem quotientBotHomeomorph_apply (hG : IsProfiniteGroup G) (g : G) :
quotientBotHomeomorph (G := G) hG g = QuotientGroup.mk (s := (⊥ : Subgroup G)) gThe continuous equivalence is evaluated by the corresponding comparison formula.
Show proof
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. 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.
□structure LeftQuotientSectionData (K H : ClosedSubgroup G) where
L : ClosedSubgroup G
hKL : (K : Subgroup G) ≤ (L : Subgroup G)
hLH : (L : Subgroup G) ≤ (H : Subgroup G)
σ : G ⧸ (H : Subgroup G) → G ⧸ (L : Subgroup G)
continuous_σ : Continuous σ
rightInv : Function.RightInverse σ
(leftQuotientProjection (L : Subgroup G) (H : Subgroup G) hLH)
one_eq :
σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G)) =
QuotientGroup.mk (s := (L : Subgroup G)) (1 : G)Data of a normalized continuous section of a left quotient projection \(G/L \to G/H\), ordered so that smaller intermediate subgroups correspond to larger elements. This is the Zorn package used for the closed-subgroup section theorem.
instance instLELeftQuotientSectionData : LE (LeftQuotientSectionData (G := G) K H) where
le a b :=
∃ hba : (b.L : Subgroup G) ≤ (a.L : Subgroup G),
leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba ∘ b.σ = a.σThe order relation is the refinement relation on the corresponding data.
instance instPreorderLeftQuotientSectionData : Preorder (LeftQuotientSectionData (G := G) K H) where
le_refl a := by
refine ⟨le_rfl, ?_⟩
funext x
simp only [leftQuotientProjection_id, Function.comp_apply, id_eq]
le_trans a b c hab hbc := by
rcases hab with ⟨hba, hbaσ⟩
rcases hbc with ⟨hcb, hcbσ⟩
refine ⟨hcb.trans hba, ?_⟩
funext x
calc
leftQuotientProjection (c.L : Subgroup G) (a.L : Subgroup G) (hcb.trans hba) (c.σ x)
= leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba
(leftQuotientProjection (c.L : Subgroup G) (b.L : Subgroup G) hcb (c.σ x)) := by
convert
(leftQuotientProjection_comp_apply
(K := (c.L : Subgroup G)) (H := (b.L : Subgroup G))
(L := (a.L : Subgroup G)) hcb hba (c.σ x)).symm
_ = leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba (b.σ x) := by
exact congrArg (leftQuotientProjection (b.L : Subgroup G) (a.L : Subgroup G) hba)
(congrFun hcbσ x)
_ = a.σ x := congrFun hbaσ xThe preorder is induced by refinement of the corresponding data.
def top (hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
LeftQuotientSectionData (G := G) K H where
L := H
hKL := hKH
hLH := le_rfl
σ := id
continuous_σ := continuous_id
rightInv := by
intro x
simp only [id_eq, leftQuotientProjection_id]
one_eq := rflThe maximal element of the Zorn poset, given by the identity section over H itself.
theorem exists_upperBound_of_chain
(hG : IsProfiniteGroup G) (c : Set (LeftQuotientSectionData (G := G) K H))
(hc : IsChain (· ≤ ·) c) (hcn : c.Nonempty) :
∃ ub : LeftQuotientSectionData (G := G) K H, ∀ a ∈ c, a ≤ ubAny nonempty chain of partial sections admits an upper bound obtained by descending to the infimum subgroup. This is the Zorn step in the section argument.
Show proof
by
classical
let I : Type u := {a : LeftQuotientSectionData (G := G) K H // a ∈ c}
have hI_nonempty : Nonempty I := by
rcases hcn with ⟨a, ha⟩
exact ⟨⟨a, ha⟩⟩
letI : Nonempty I := hI_nonempty
let L : I → ClosedSubgroup G := fun i => i.1.L
have hL : ∀ {i j : I}, i ≤ j → (L j : Subgroup G) ≤ (L i : Subgroup G) := by
intro i j hij
rcases hij with ⟨hji, -⟩
exact hji
have hdir : Directed (· ≤ ·) (id : I → I) := by
intro i j
by_cases hij : i = j
· subst hij
exact ⟨i, le_rfl, le_rfl⟩
· have hcmp := hc i.2 j.2 (by
intro hij'
apply hij
exact Subtype.ext hij')
rcases hcmp with hij' | hji'
· exact ⟨j, hij', le_rfl⟩
· exact ⟨i, le_rfl, hji'⟩
obtain ⟨ηinf, hηinf_continuous, hηinf_fac, hηinf_one⟩ :=
exists_continuous_leftQuotient_lift_of_directed (G := G) hG L hL hdir
(η := fun i => i.1.σ) (hηcont := fun i => i.1.continuous_σ)
(hηcompat := by
intro i j hij
rcases hij with ⟨hji, hσ⟩
exact hσ)
(QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))
(by
intro i
exact i.1.one_eq)
let Linf : ClosedSubgroup G := closedSubgroup_sInf L
have hKinf : (K : Subgroup G) ≤ (Linf : Subgroup G) := by
intro x hx
change x ∈ iInf fun i => (L i : Subgroup G)
rw [Subgroup.mem_iInf]
intro i
exact i.1.hKL hx
let i0 : I := Classical.choice hI_nonempty
have hInfH : (Linf : Subgroup G) ≤ (H : Subgroup G) := by
exact (closedSubgroup_sInf_le (L := L) i0).trans i0.1.hLH
refine ⟨{ L := Linf
hKL := hKinf
hLH := hInfH
σ := ηinf
continuous_σ := hηinf_continuous
rightInv := by
intro y
calc
leftQuotientProjection (Linf : Subgroup G) (H : Subgroup G) hInfH (ηinf y)
= leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH
(leftQuotientProjection (Linf : Subgroup G) (i0.1.L : Subgroup G)
(closedSubgroup_sInf_le (L := L) i0) (ηinf y)) := by
convert
(leftQuotientProjection_comp_apply
(K := (Linf : Subgroup G)) (H := (i0.1.L : Subgroup G))
(L := (H : Subgroup G)) (closedSubgroup_sInf_le (L := L) i0)
i0.1.hLH (ηinf y)).symm
_ = leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH
(i0.1.σ y) := by
exact congrArg
(leftQuotientProjection (i0.1.L : Subgroup G) (H : Subgroup G) i0.1.hLH)
(congrFun (hηinf_fac i0) y)
_ = y := i0.1.rightInv y
one_eq := hηinf_one }, ?_⟩
intro a ha
refine ⟨closedSubgroup_sInf_le (L := L) ⟨a, ha⟩, ?_⟩
exact hηinf_fac ⟨a, ha⟩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. Projection and transition formulas are proved at an arbitrary finite stage. Both sides use the same quotient map on the support and the same coefficient map on the coefficient, so they agree on singleton basis elements; finite support and linearity extend the equality to the whole finite-stage group algebra.
□theorem leftQuotientProjection_hasContinuousSection
(hG : IsProfiniteGroup G) (K H : ClosedSubgroup G)
(hKH : (K : Subgroup G) ≤ (H : Subgroup G)) :
∃ σ : 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)General section theorem for left quotient projections between closed subgroups of a profinite group.
Show proof
by
classical
let P := LeftQuotientSectionData (G := G) K H
letI : Nonempty P := ⟨LeftQuotientSectionData.top (G := G) hKH⟩
obtain ⟨m, hmmax⟩ := zorn_le_nonempty (α := P) <| by
intro c hc hcn
rcases LeftQuotientSectionData.exists_upperBound_of_chain (G := G) (K := K) (H := H)
hG c hc hcn with ⟨ub, hub⟩
exact ⟨ub, hub⟩
have hmLK : m.L = K := by
by_contra hne
have hnotle : ¬ (m.L : Subgroup G) ≤ (K : Subgroup G) := by
intro hmK
apply hne
ext x
change x ∈ (m.L : Subgroup G) ↔ x ∈ (K : Subgroup G)
exact ⟨fun hx => hmK hx, fun hx => m.hKL hx⟩
rcases exists_mem_of_not_le (G := G) (K := K) (L := m.L) hnotle with ⟨x, hxL, hxK⟩
let hT : IsProfiniteGroup ↥(m.L : Subgroup G) :=
IsProfiniteGroup.of_closedSubgroup (G := G) hG m.L
let KT : ClosedSubgroup ↥(m.L : Subgroup G) := {
toSubgroup := (K : Subgroup G).subgroupOf (m.L : Subgroup G)
isClosed' := by
change IsClosed (((↑) : ↥(m.L : Subgroup G) → G) ⁻¹' (K : Set G))
simpa [Subgroup.coe_subgroupOf] using K.isClosed'.preimage continuous_subtype_val }
let xT : ↥(m.L : Subgroup G) := ⟨x, hxL⟩
have hxTK : xT ∉ (KT : Set ↥(m.L : Subgroup G)) := by
simpa [KT, Subgroup.mem_subgroupOf] using hxK
obtain ⟨N, hKTN, hxN⟩ :=
exists_openSubgroup_ge_closedSubgroup_not_mem (G := ↥(m.L : Subgroup G)) hT KT hxTK
let L' : ClosedSubgroup G := closedSubgroupOfOpenSubgroup (G := G) hG m.L N
have hL'm : (L' : Subgroup G) ≤ (m.L : Subgroup G) :=
closedSubgroupOfOpenSubgroup_le (G := G) hG m.L N
have hKL' : (K : Subgroup G) ≤ (L' : Subgroup G) := by
intro g hg
have hgT : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (KT : Subgroup ↥(m.L : Subgroup G)) := by
simpa [KT, Subgroup.mem_subgroupOf] using hg
have hgN : (⟨g, m.hKL hg⟩ : ↥(m.L : Subgroup G)) ∈ (N : Subgroup ↥(m.L : Subgroup G)) :=
hKTN hgT
exact (mem_closedSubgroupOfOpenSubgroup (G := G) hG (T := m.L) (N := N)
(x := ⟨g, m.hKL hg⟩)).2 hgN
have hL'H : (L' : Subgroup G) ≤ (H : Subgroup G) := hL'm.trans m.hLH
have hL'open :
IsOpen (((L' : Subgroup G).subgroupOf (m.L : Subgroup G)) : Set ↥(m.L : Subgroup G)) := by
rw [closedSubgroupOfOpenSubgroup_subgroupOf_eq (G := G) hG m.L N]
exact N.isOpen'
have hxL' : x ∉ (L' : Subgroup G) := by
intro hxL'
have : xT ∈ (N : Subgroup ↥(m.L : Subgroup G)) := by
exact (mem_closedSubgroupOfOpenSubgroup (G := G) hG (T := m.L) (N := N)
(x := xT)).1 (by simpa [xT] using hxL')
exact hxN this
obtain ⟨ξ, hξcont, hξright, hξone⟩ :=
leftQuotientProjection_hasContinuousSection_of_openSubgroup (G := G) hG L' m.L hL'm hL'open
let m' : P :=
{ L := L'
hKL := hKL'
hLH := hL'H
σ := ξ ∘ m.σ
continuous_σ := hξcont.comp m.continuous_σ
rightInv := by
intro y
calc
leftQuotientProjection (L' : Subgroup G) (H : Subgroup G) hL'H ((ξ ∘ m.σ) y)
= leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH
(leftQuotientProjection (L' : Subgroup G) (m.L : Subgroup G) hL'm
(ξ (m.σ y))) := by
convert
(leftQuotientProjection_comp_apply
(K := (L' : Subgroup G)) (H := (m.L : Subgroup G))
(L := (H : Subgroup G)) hL'm m.hLH (ξ (m.σ y))).symm
_ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by
rw [hξright (m.σ y)]
_ = y := m.rightInv y
one_eq := by
change ξ (m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) =
QuotientGroup.mk (s := (L' : Subgroup G)) (1 : G)
rw [m.one_eq]
exact hξone }
have hmm' : m ≤ m' := by
refine ⟨hL'm, ?_⟩
funext y
exact hξright (m.σ y)
have hm'm : m' ≤ m := hmmax hmm'
rcases hm'm with ⟨hm'mL, -⟩
exact hxL' (hm'mL hxL)
have hLKsub : (m.L : Subgroup G) = (K : Subgroup G) := congrArg ClosedSubgroup.toSubgroup hmLK
have hmLleK : (m.L : Subgroup G) ≤ (K : Subgroup G) := by
intro x hx
simpa [hLKsub] using hx
let σ : G ⧸ (H : Subgroup G) → G ⧸ (K : Subgroup G) :=
leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK ∘ m.σ
refine ⟨σ, (continuous_leftQuotientProjection
(K := (m.L : Subgroup G)) (H := (K : Subgroup G)) hmLleK).comp m.continuous_σ, ?_, ?_⟩
· intro y
have hproof : hmLleK.trans hKH = m.hLH := Subsingleton.elim _ _
calc
leftQuotientProjection (K : Subgroup G) (H : Subgroup G) hKH (σ y) =
leftQuotientProjection
(m.L : Subgroup G)
(H : Subgroup G)
(hmLleK.trans hKH)
(m.σ y) := by
simpa only [σ, Function.comp] using
(leftQuotientProjection_comp_apply
(K := (m.L : Subgroup G)) (H := (K : Subgroup G))
(L := (H : Subgroup G)) hmLleK hKH (m.σ y))
_ = leftQuotientProjection (m.L : Subgroup G) (H : Subgroup G) m.hLH (m.σ y) := by
rw [hproof]
_ = y := m.rightInv y
· calc
σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))
= leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK
(m.σ (QuotientGroup.mk (s := (H : Subgroup G)) (1 : G))) := by
rfl
_ = leftQuotientProjection (m.L : Subgroup G) (K : Subgroup G) hmLleK
(QuotientGroup.mk (s := (m.L : Subgroup G)) (1 : G)) := by
rw [m.one_eq]
_ = QuotientGroup.mk (s := (K : Subgroup G)) (1 : G) := 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. 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 exists_continuousSection_quotientMk_of_isClosed
(H : Subgroup G) :
IsProfiniteGroup G →
IsClosed (H : Set G) →
∃ σ : (G ⧸ H) → G,
Continuous σ ∧
Function.RightInverse σ (QuotientGroup.mk (s := H)) ∧
σ (QuotientGroup.mk (s := H) (1 : G)) = 1A quotient by a closed normal subgroup of a profinite group admits a continuous section that sends the identity coset to the identity.
Show proof
by
intro hG hH
letI : T2Space G := IsProfiniteGroup.t2Space hG
let K0 : ClosedSubgroup G := ⟨⊥, by
change IsClosed ({(1 : G)} : Set G)
simp only [finite_singleton, Finite.isClosed]⟩
let HC : ClosedSubgroup G := ⟨H, hH⟩
have hbotH : (⊥ : Subgroup G) ≤ H := by
intro x hx
have hx1 : x = 1 := by
simpa [Subgroup.mem_bot] using hx
simp only [hx1, one_mem]
obtain ⟨σ0, hσ0cont, hσ0right, hσ0one⟩ :=
leftQuotientProjection_hasContinuousSection (G := G) hG K0 HC hbotH
let e : G ≃ₜ G ⧸ (⊥ : Subgroup G) := quotientBotHomeomorph (G := G) hG
refine ⟨e.symm ∘ σ0, e.symm.continuous.comp hσ0cont, ?_, ?_⟩
· intro y
calc
QuotientGroup.mk (s := H) ((e.symm ∘ σ0) y)
= leftQuotientProjection (⊥ : Subgroup G) H hbotH
(e ((e.symm ∘ σ0) y)) := by
rfl
_ = leftQuotientProjection (⊥ : Subgroup G) H hbotH (σ0 y) := by
exact congrArg (leftQuotientProjection (⊥ : Subgroup G) H hbotH) (e.right_inv (σ0 y))
_ = y := hσ0right y
· change e.symm (σ0 (QuotientGroup.mk (s := H) (1 : G))) = 1
rw [hσ0one]
change e.symm (e (1 : G)) = 1
exact e.left_inv (1 : 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.
□