Double cosets at a normalizing element

A double coset ΓgΓ is in general a union of several cosets on either side. When g normalizes Γ it is a single coset, and the two sides agree:

ΓgΓ = Γ(gΓg⁻¹)g = ΓΓg = Γg.

This file records that collapse, together with the observation that a double coset at a normalizing element consists of normalizing elements. Both are used wherever a Hecke double coset attached to an element of the normalizer has to be recognised as a single coset — for Γ₁(N) ⊴ Γ₀(N), this is what makes the diamond operators double-coset operators.

Main results

• DoubleCoset.doubleCoset_eq_rightCoset_of_mem_normalizer: ΓgΓ = Γg for g normalizing Γ.
• DoubleCoset.mem_normalizer_of_mem_doubleCoset: every element of such a ΓgΓ again normalizes Γ, so the collapse propagates to any representative of the double coset.
• DoubleCoset.mem_rightCoset_conj_iff_of_mem_normalizer, DoubleCoset.conj_mem_doubleCoset_conj_iff_of_mem_normalizer: conjugation by g in the normalizer carries the right cosets Γa and the double cosets HaK (g normalizing H and K) to the right and double cosets of the conjugate g⁻¹ag.

theorem DoubleCoset.doubleCoset_eq_rightCoset_of_mem_normalizer {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑Γ) : doubleCoset g ↑Γ ↑Γ = MulOpposite.op g • ↑Γ

A double coset at a normalizing element is a single right coset. For g in the normalizer of Γ the two flanking copies of Γ merge: the right-hand factor b of a * g * b is absorbed by rewriting g * b = (g * b * g⁻¹) * g.

The left-coset form is the same statement, Γ g Γ = g Γ, read through gΓ = Γg; only the right-coset form is stated, because that is the handedness in which Hecke operators decompose a double coset.

theorem DoubleCoset.mem_normalizer_of_mem_doubleCoset {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑Γ) {x : G} (hx : x ∈ doubleCoset g ↑Γ ↑Γ) : x ∈ Subgroup.normalizer ↑Γ

A double coset at a normalizing element consists of normalizing elements. Every a * g * b with a, b ∈ Γ lies in the normalizer of Γ, which contains both Γ and g. Consequently doubleCoset_eq_rightCoset_of_mem_normalizer applies to any representative of the double coset, not only to the chosen g.

theorem DoubleCoset.mem_rightCoset_conj_iff_of_mem_normalizer {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} (hg : g ∈ Subgroup.normalizer ↑Γ) (a x : G) : x ∈ MulOpposite.op (g⁻¹ * a * g) • ↑Γ ↔ g * x * g⁻¹ ∈ MulOpposite.op a • ↑Γ

Conjugation by a normalizing element carries right cosets to right cosets: x ∈ Γ(g⁻¹ag) exactly when gxg⁻¹ ∈ Γa.

theorem DoubleCoset.conj_mem_doubleCoset_conj_iff_of_mem_normalizer {G : Type u_1} [Group G] {g : G} {H K : Subgroup G} (hH : g ∈ Subgroup.normalizer ↑H) (hK : g ∈ Subgroup.normalizer ↑K) (a x : G) : g⁻¹ * x * g ∈ doubleCoset (g⁻¹ * a * g) ↑H ↑K ↔ x ∈ doubleCoset a ↑H ↑K

Conjugation by an element normalizing both flanks carries double cosets to double cosets: g⁻¹xg ∈ H(g⁻¹ag)K exactly when x ∈ HaK.