Continuity of the transversal word

For a subgroup U of a group G and a map t : G ⧸ U → G, the transversal word ℓᵗ_u(γ) = (t u)⁻¹ * γ * t (γ⁻¹ • u) of TauCeti.lWord is a purely group-theoretic construction. If multiplication on G is separately continuous and U is open, then γ ↦ ℓᵗ_u(γ) is continuous (TauCeti.continuous_lWord). Openness of U makes G ⧸ U discrete, so γ ↦ γ⁻¹ • u, and hence γ ↦ t (γ⁻¹ • u), is locally constant. On each such neighborhood the word has the form γ ↦ c₁ * γ * c₂ for fixed c₁ and c₂, which is continuous by separate continuity of multiplication. No continuity is required of t itself. The variant TauCeti.continuous_lWord_inv_smul lets the coset index itself be translated by a second group variable, which is the shape the degree-two corestriction sum is indexed by.

The continuity results live here, separate from the group-theoretic transversal calculus in TauCeti/GroupTheory/TransversalWord.lean.

theorem TauCeti.continuous_lWord {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (t : G ⧸ U → G) (hU : IsOpen ↑U) (u : G ⧸ U) : Continuous (lWord U t u)

For an open subgroup U the transversal word γ ↦ ℓᵗ_u(γ) is continuous, for any map t at all: the quotient G ⧸ U is discrete, so γ ↦ t (γ⁻¹ • u) is locally constant.

theorem TauCeti.continuous_lWord_inv_smul {G : Type u_1} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] (U : Subgroup G) (t : G ⧸ U → G) (hU : IsOpen ↑U) (u : G ⧸ U) : Continuous fun (q : G × G) => lWord U t (q.1⁻¹ • u) q.2

For an open subgroup U the transversal word is continuous jointly in its group variable and in a coset index translated by a second group variable: (γ, η) ↦ ℓᵗ_{γ⁻¹ • u}(η). Here both γ ↦ t (γ⁻¹ • u) and (γ, η) ↦ t (η⁻¹ • γ⁻¹ • u) are locally constant, again because G ⧸ U is discrete, so no continuity is required of t itself.