Double cosets: the left-coset decomposition

A double coset HaK decomposes as the union of the left cosets (h * a) • K, where h ranges over representatives of the quotient of H by the stabiliser H ∩ aKa⁻¹. The decomposition indexes the left cosets inside a double coset and underlies the finiteness of Hecke coset decompositions in TauCeti.NumberTheory.HeckeRing.Basic.

This file also records how the stabiliser (gKg⁻¹).subgroupOf H responds to moving the base point g: right multiplication by anything normalising K leaves it alone, and left multiplication by anything normalising H conjugates it. TauCeti.NumberTheory.HeckeRing. StabConjugation turns those into equivalences of decomposition quotients.

Vendored from the in-review mathlib4 PR #41253 (Chris Birkbeck), per the ModularForms roadmap's dependency policy; migrate to Mathlib and delete this file when that stack merges.

theorem DoubleCoset.doubleCoset_eq_iUnion_leftCosets {G : Type u_1} [Group G] (H K : Subgroup G) (a : G) : doubleCoset a ↑H ↑K = ⋃ (i : ↥H ⧸ (ConjAct.toConjAct a • K).subgroupOf H), (↑(Quotient.out i) * a) • ↑K

A double coset HaK is the union of the left cosets (h * a) • K where h ranges over representatives of the quotient of H by the stabiliser H ∩ aKa⁻¹, with no repeated cosets; compare DoubleCoset.doubleCoset_union_leftCoset, which is indexed by all of H.

theorem DoubleCoset.conjAct_smul_mul_right_of_mem_normalizer {G : Type u_1} [Group G] (Γ : Subgroup G) (g : G) {h : G} (hh : h ∈ Subgroup.normalizer ↑Γ) : ConjAct.toConjAct (g * h) • Γ = ConjAct.toConjAct g • Γ

Conjugation only sees g modulo the normalizer on the right: (gh)Γ(gh)⁻¹ = gΓg⁻¹ whenever h normalizes Γ. Membership in Γ itself is the special case Subgroup.le_normalizer.

theorem DoubleCoset.subgroupOf_conjAct_smul_mul_right_of_mem_normalizer {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) {h : G} (hh : h ∈ Subgroup.normalizer ↑Γ₂) : (ConjAct.toConjAct (g * h) • Γ₂).subgroupOf Γ₁ = (ConjAct.toConjAct g • Γ₂).subgroupOf Γ₁

The stabilizer cut out inside Γ₁ is unchanged by right multiplication of the base point by anything normalizing Γ₂.

theorem DoubleCoset.subgroupOf_conjAct_smul_mul_left_of_mem_normalizer {G : Type u_1} [Group G] (Γ₁ Γ₂ : Subgroup G) (g : G) (h : ↥(Subgroup.normalizer ↑Γ₁)) : (ConjAct.toConjAct (↑h * g) • Γ₂).subgroupOf Γ₁ = Subgroup.map (MulEquiv.toMonoidHom (Γ₁.normalizerMonoidHom h)) ((ConjAct.toConjAct g • Γ₂).subgroupOf Γ₁)

Left multiplication of the base point by anything normalizing Γ₁ conjugates the stabilizer by it: x stabilizes hg exactly when h⁻¹xh stabilizes g. Membership in Γ₁ itself is the special case Subgroup.le_normalizer.

The conjugating automorphism of ↥Γ₁ is Subgroup.normalizerMonoidHom, which is defined for exactly this: MulAut.conj h would need h to be an element of Γ₁.

theorem DoubleCoset.mul_mem_doubleCoset_iff {G : Type u_1} [Group G] {H K : Subgroup G} {b : G} (hb : b ∈ H) {a z : G} : b * z ∈ doubleCoset a ↑H ↑K ↔ z ∈ doubleCoset a ↑H ↑K

Membership in a double coset is invariant under left multiplication by the left subgroup.

theorem DoubleCoset.inv_mul_mem_doubleCoset_iff_of_mem {G : Type u_1} [Group G] {H K : Subgroup G} {w x d g : G} (h : x⁻¹ * w ∈ H) : x⁻¹ * d ∈ doubleCoset g ↑H ↑K ↔ w⁻¹ * d ∈ doubleCoset g ↑H ↑K

Translating an inverse along a left coset. If w and x lie in the same left coset of H, then x⁻¹ d and w⁻¹ d lie in the same double coset H g K.

theorem DoubleCoset.mem_doubleCoset_of_quotient_eq {G : Type u_1} [Group G] {H K : Subgroup G} {w x l : G} (hl : l ∈ H) (h : ↑w = ↑(l * x)) : w ∈ doubleCoset x ↑H ↑K

Recognising a double coset from a quotient equation. If w agrees with l x modulo K for some l ∈ H, then w lies in the double coset H x K.