Continuous right-coset factorizations

A continuous section of G → G ⧸ H gives continuous maps w : G → H and r : G → G with g = w g * r g, where w is H-equivariant and r is constant on right cosets. For an open subgroup the quotient is discrete, so Quotient.out supplies such a section.

Main results

• Subgroup.exists_continuous_rightCosetFactorization_of_section: factorization from any continuous section of the quotient map.
• Subgroup.exists_continuous_rightCosetFactorization_of_isOpen: factorization for an open subgroup of any topological group.

theorem Subgroup.exists_continuous_rightCosetFactorization_of_section {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) (s : G ⧸ H → G) (hs_cont : Continuous s) (hs_sec : ∀ (x : G ⧸ H), ↑(s x) = x) : ∃ (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) = s ↑1

The right-coset factorization attached to a continuous section s of G → G ⧸ H: w g = g * s ⟦g⁻¹⟧ ∈ H and r g = (s ⟦g⁻¹⟧)⁻¹, with w 1 = s ⟦1⟧. Inverting exchanges left and right cosets, so r g lies in H * g and depends only on that right coset.

theorem Subgroup.exists_continuous_rightCosetFactorization_of_isOpen {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) (hH : IsOpen ↑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

The right-coset factorization for an open subgroup. For an open subgroup H of a topological group G, every g : G factors as g = w g * r g with w g ∈ H, where r g depends only on the right coset H * g, and both w and r are continuous. No compactness is needed: the coset space G ⧸ H is discrete, so the choice of representatives Quotient.out is already a continuous section. The factorization need not be normalized at 1.