Continuous sections of profinite quotients

Let G be a profinite group — compact, totally disconnected, and topological, in the unbundled classes — and let H be a closed subgroup. This module proves that the quotient map G → G ⧸ H admits a continuous section normalized at the identity coset, and deduces the same for the projection G ⧸ K → G ⧸ H attached to a pair of subgroups K ≤ H.

The proof produces a closed left transversal: a closed set meeting every left coset of H exactly once. Zorn's lemma, applied to the pairs (K, C) where C is a closed set meeting every left coset of H in exactly one coset of the subgroup K ≤ H, yields a minimal such pair; the refinement step shows a minimal pair has K = ⊥, which is exactly the transversal condition. That step is where the topology enters: an element h ≠ 1 of K is separated from 1 by an open normal subgroup N, and the N-cosets inside a K-coset xK biject with the cosets of the image of K in the finite group G ⧸ N, so choosing one representative per coset there thins C down along a clopen condition, which preserves closedness. Passing to a chain also uses compactness: Cantor's intersection theorem shows that the intersection of a chain of such C's still meets every coset.

Main results

• Subgroup.exists_isClosed_isComplement_left: a closed subgroup of a profinite group has a closed left transversal, in Mathlib's sense Subgroup.IsComplement.
• TauCeti.exists_continuous_section: the normalized continuous section G ⧸ H → G.
• TauCeti.exists_continuous_section_of_le: the continuous section of G ⧸ K → G ⧸ H for K ≤ H.
• TauCeti.exists_continuous_rightCosetFactorization: the right-coset form, g = w g * r g with w g ∈ H and r g depending only on the right coset H * g, both continuous, and normalized by w 1 = 1.

Implementation notes

The nearby false statement is that G ⧸ H is a projective object, so that every continuous surjection onto it splits: profinite spaces are projective only when they are extremally disconnected, and the section below genuinely uses the group structure of the fibres. None of this is needed when H is open: then G ⧸ H is discrete and Quotient.out is already continuous, which is how Subgroup.exists_continuous_rightCosetFactorization_of_isOpen is proved in the general quotient section module.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Proposition 2.2.2.

theorem Subgroup.exists_isClosed_isComplement_left {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : ∃ (C : Set G), IsClosed C ∧ IsComplement C ↑H

A closed subgroup of a profinite group has a closed left transversal. The set C produced here meets every left coset of H in exactly one point and is closed, hence compact; that is what makes the induced bijection C ≃ G ⧸ H a homeomorphism in TauCeti.exists_continuous_section.

theorem TauCeti.exists_continuous_section {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : ∃ (s : G ⧸ H → G), Continuous s ∧ (∀ (x : G ⧸ H), ↑(s x) = x) ∧ s ↑1 = 1

Continuous sections of profinite quotients (Ribes-Zalesskii, Proposition 2.2.2). For a closed subgroup H of a profinite group G the quotient map G → G ⧸ H has a continuous section sending the identity coset to 1. This is the statement that the transgression of a five-term exact sequence, the exactness of coinduction and the inverse in Shapiro's lemma all lift through; for an open subgroup the finite transversal Quotient.out already suffices, and this statement is not needed.

theorem TauCeti.exists_continuous_section_of_le {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {K H : Subgroup G} (hKH : K ≤ H) (hH : IsClosed ↑H) : ∃ (s : G ⧸ H → G ⧸ K), Continuous s ∧ (∀ (x : G ⧸ H), Subgroup.quotientMapOfLE hKH (s x) = x) ∧ s ↑1 = ↑1

The continuous section of a projection between quotients of a profinite group. For subgroups K ≤ H of a profinite group with H closed, the projection G ⧸ K → G ⧸ H has a continuous section normalized at the identity coset.

theorem TauCeti.exists_continuous_rightCosetFactorization {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : ∃ (w : G → ↥H) (r : G → G), Continuous w ∧ Continuous r ∧ (∀ (g : G), ↑(w g) * r g = g) ∧ (∀ (h : ↥H) (g : G), w (↑h * g) = h * w g) ∧ (∀ (h : ↥H) (g : G), r (↑h * g) = r g) ∧ w 1 = 1

The right-coset form of the continuous section. For a closed subgroup H of a profinite group G, every g : G factors as g = w g * r g with w g ∈ H, where r g is a representative of the right coset H * g depending only on that coset and w is the resulting H-valued cocycle; both are continuous. The factorization is normalized: w 1 = 1, inherited from the normalization of TauCeti.exists_continuous_section.

Mathlib's quotient G ⧸ H is the space of left cosets, so TauCeti.exists_continuous_section produces a continuous choice of representatives of g H. Inverting exchanges the two sides: r g = (s ⟦g⁻¹⟧)⁻¹ lies in H * g and depends only on H * g. This is the shape the coinduced module of Layer 7 consumes, since its defining equivariance f (h * g) = h • f g is along right cosets.