Double cosets as orbits

For subgroups H and K of a group G, a double coset is an orbit in two ways.

The double coset KsH is the preimage in G of the K-orbit of the coset sH (TauCeti.preimage_orbit_eq_doubleCoset), so the partition of G ⧸ H into K-orbits is the partition of G into K-H double cosets.

Globally, the diagonal action of G on (G ⧸ H) × (G ⧸ K) has orbits in bijection with the double cosets H \ G / K: the orbit of (aH, bK) is recorded by the double coset H a⁻¹ b K, and every orbit meets the slice {(H, gK) | g : G}.

Combining that bijection with Burnside's lemma counts double cosets by a sum of fixed-point numbers, which is the group-theoretic half of the statement that the permutation character of G on G ⧸ H pairs with the permutation character on G ⧸ K to #(H \ G / K).

Main definitions

• TauCeti.doubleCosetEquivOrbitQuotient: the bijection H \ G / K ≃ ((G ⧸ H) × (G ⧸ K)) / G.
• TauCeti.orbitOfCosetTranslate: the 𝒢-orbit a class in ℋ ⧸ 𝒢.subgroupOf ℋ translates a point into — the index map along which a coset sum is regrouped into an orbit sum.

Main statements

• TauCeti.mem_doubleCoset_iff_mk_mem_orbit: an element lies in KsH exactly when its coset lies in the K-orbit of sH.
• TauCeti.orbitRel_smul_iff_mem_doubleCoset_stabilizer: the same for an arbitrary action — two translates of a point share a K-orbit exactly when the translating elements share a K-stabilizer double coset.
• TauCeti.orbitOfCosetTranslate_eq_iff: the fibres of that index map are the orbits of stabilizer ℋ p on ℋ ⧸ 𝒢.subgroupOf ℋ, so a fibre count is an orbit-stabiliser count.
• TauCeti.card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_coset: that count, carried out — the fibre size times the order of the stabiliser of the class inside stabilizer ℋ p is the order of stabilizer ℋ p.
• TauCeti.card_fiber_orbitOfCosetTranslate_mul_cardStabilizerOnOrbit: the multiplicity identity behind regrouping a sum over ℋ ⧸ 𝒢.subgroupOf ℋ into a sum over 𝒢-orbits — the fibre size times the stabiliser order on the orbit is |stabilizer ℋ p|, with TauCeti.card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_inv_smul its form at a chosen representative. Stated multiplicatively, so it holds also when the stabilisers are infinite (Nat.card = 0).
• TauCeti.card_fiber_orbitOfCosetTranslate_eq_relIndex: the fibre size itself, as the relative index of the stabilisers of the translate h⁻¹ • p in 𝒢 and in ℋ; this determines the fibre also when the stabilisers are infinite.
• TauCeti.preimage_orbit_eq_doubleCoset: the double coset KsH is the preimage of the K-orbit of sH.
• TauCeti.card_doubleCosetQuotient_eq_card_orbitQuotient: the two sides of that bijection have the same cardinality.
• TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_doubleCosetQuotient_mul_card_group: Burnside's lemma read through that bijection, ∑ g, |(G ⧸ H)^g| * |(G ⧸ K)^g| = #(H \ G / K) * |G|.

Implementation notes

Mathlib's DoubleCoset.Quotient (H : Set G) K takes the two subgroups as sets, and its representatives multiply as h * a * k. The bijection below is built from the slice map g ↦ orbit of (H, gK), which is surjective because a • (H, a⁻¹bK) = (aH, bK), and injective because the pair (aH, bK) determines H a⁻¹ b K.

References

This supplies the "⟨Ind_H^G 1, Ind_H^G 1⟩_G = #(H \ G / H)" item of Layer 2 in TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md with its group-theoretic input.

orbitOfCosetTranslate and its fibre count instead serve Layer 1 of TauCetiRoadmap/ModularForms/README.md, "General level — by the coset norm", whose orbit/stabiliser bookkeeping regroups a sum over a coset space into a sum over orbits.

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.3.

@[simp]

theorem TauCeti.mem_doubleCoset_iff_mk_mem_orbit {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) {x : G} : x ∈ DoubleCoset.doubleCoset s ↑K ↑H ↔ ↑x ∈ MulAction.orbit ↥K ↑s

The double coset KsH consists exactly of those x whose class in G ⧸ H lies in the K-orbit of the class of s.

theorem TauCeti.preimage_orbit_eq_doubleCoset {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : QuotientGroup.mk ⁻¹' MulAction.orbit ↥K ↑s = DoubleCoset.doubleCoset s ↑K ↑H

The double coset KsH is the preimage, under G → G ⧸ H, of the K-orbit of the coset sH. So the partition of G into K-H double cosets is the partition of G ⧸ H into K-orbits.

def TauCeti.doubleCosetOrbit {G : Type u_1} [Group G] (H K : Subgroup G) (g : G) : MulAction.orbitRel.Quotient G ((G ⧸ H) × G ⧸ K)

The orbit of the pair of cosets (H, gK) under the diagonal action of G on (G ⧸ H) × (G ⧸ K). Every orbit is of this form, and doubleCosetOrbit_eq_iff says that the double coset HgK is a complete invariant of it.

Equations

• TauCeti.doubleCosetOrbit H K g = Quotient.mk'' (↑1, ↑g)

@[simp]

theorem TauCeti.doubleCosetOrbit_eq_iff {G : Type u_1} [Group G] {H K : Subgroup G} {a b : G} : doubleCosetOrbit H K a = doubleCosetOrbit H K b ↔ DoubleCoset.mk H K a = DoubleCoset.mk H K b

Two points of the slice {(H, gK) | g : G} lie in the same orbit exactly when their labels lie in the same double coset.

noncomputable def TauCeti.doubleCosetEquivOrbitQuotient {G : Type u_1} [Group G] (H K : Subgroup G) : DoubleCoset.Quotient ↑H ↑K ≃ MulAction.orbitRel.Quotient G ((G ⧸ H) × G ⧸ K)

Double cosets are orbits. The double cosets H \ G / K are in bijection with the orbits of G acting diagonally on (G ⧸ H) × (G ⧸ K), the double coset of g corresponding to the orbit of (H, gK).

Equations

• TauCeti.doubleCosetEquivOrbitQuotient H K = Equiv.ofBijective (Quotient.lift (TauCeti.doubleCosetOrbit H K) ⋯) ⋯

@[simp]

theorem TauCeti.doubleCosetEquivOrbitQuotient_apply_mk {G : Type u_1} [Group G] (H K : Subgroup G) (g : G) : (doubleCosetEquivOrbitQuotient H K) (DoubleCoset.mk H K g) = doubleCosetOrbit H K g

theorem TauCeti.card_doubleCosetQuotient_eq_card_orbitQuotient {G : Type u_1} [Group G] (H K : Subgroup G) : Nat.card (DoubleCoset.Quotient ↑H ↑K) = Nat.card (MulAction.orbitRel.Quotient G ((G ⧸ H) × G ⧸ K))

The number of double cosets H \ G / K is the number of orbits of G on (G ⧸ H) × (G ⧸ K).

theorem TauCeti.orbitRel_smul_iff_mem_doubleCoset_stabilizer {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] (K : Subgroup G) (p : α) (x y : G) : (MulAction.orbitRel (↥K) α) (x • p) (y • p) ↔ x ∈ DoubleCoset.doubleCoset y ↑K ↑(MulAction.stabilizer G p)

Two translates of a point lie in one K-orbit exactly when the translating elements lie in one double coset. For K ≤ G acting on α and a point p, the K-orbits inside the G-orbit of p are indexed by the K-stabilizer G p double cosets.

This is the companion of mem_doubleCoset_iff_mk_mem_orbit for an arbitrary action rather than the action on G ⧸ H: taking H = stabilizer G p there and transporting along MulAction.orbitEquivQuotientStabilizer gives the same statement.

noncomputable def TauCeti.orbitOfCosetTranslate {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (p : α) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : MulAction.orbitRel.Quotient (↥𝒢) α

The 𝒢-orbit that a coset translates a point into. For 𝒢 ≤ ℋ ≤ G acting on α and a point p, a class in ℋ ⧸ 𝒢.subgroupOf ℋ determines the 𝒢-orbit of h⁻¹ • p, independently of the representative h.

Well-definedness is the content: another representative is h * g with g ∈ 𝒢, and (h * g)⁻¹ • p = g⁻¹ • (h⁻¹ • p) lies in the same 𝒢-orbit. This is the index map along which a sum over the coset space ℋ ⧸ 𝒢.subgroupOf ℋ is regrouped into a sum over 𝒢-orbits, with orbitRel_smul_iff_mem_doubleCoset_stabilizer identifying its fibres as double cosets.

Equations

• TauCeti.orbitOfCosetTranslate p q = Quotient.liftOn' q (fun (h : ↥ℋ) => Quotient.mk'' ((↑h)⁻¹ • p)) ⋯

@[simp]

theorem TauCeti.orbitOfCosetTranslate_mk {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (p : α) (h : ↥ℋ) : orbitOfCosetTranslate p ⟦h⟧ = Quotient.mk'' ((↑h)⁻¹ • p)

Evaluating orbitOfCosetTranslate on the class of h gives the orbit of h⁻¹ • p.

theorem TauCeti.orbitOfCosetTranslate_eq_iff {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (q r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : orbitOfCosetTranslate p q = orbitOfCosetTranslate p r ↔ q ∈ MulAction.orbit (↥(MulAction.stabilizer (↥ℋ) p)) r

The fibres of orbitOfCosetTranslate are the stabilizer ℋ p-orbits. Two classes have the same image exactly when they lie in one orbit of the stabilizer of p, acting on the coset space by left translation.

This is the fibre description the definition exists for: it turns a fibre of that index map into an orbit, so that a fibre count becomes an orbit-stabiliser count via MulAction.index_stabilizer.

hle : 𝒢 ≤ ℋ is what puts the translating element back inside ℋ: the witness orbitRel_smul_iff_mem_doubleCoset_stabilizer produces lies in 𝒢, and the stabilising factor is an element of ℋ only once 𝒢 is.

theorem TauCeti.card_fiber_orbitOfCosetTranslate_eq_index_stabilizer {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : Nat.card { r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ // orbitOfCosetTranslate p r = orbitOfCosetTranslate p q } = (MulAction.stabilizer (↥(MulAction.stabilizer (↥ℋ) p)) q).index

The fibre size as an index. The number of coset classes that translate p into the same orbit as q does is the index of the stabiliser of q inside stabilizer ℋ p.

q ranges over arbitrary classes, and no finiteness is assumed: unlike the multiplicative form card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_coset below, this determines the fibre size even when the stabilisers are infinite. For a chosen representative, see card_fiber_orbitOfCosetTranslate_eq_relIndex.

theorem TauCeti.card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_coset {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : Nat.card { r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ // orbitOfCosetTranslate p r = orbitOfCosetTranslate p q } * Nat.card ↥(MulAction.stabilizer (↥(MulAction.stabilizer (↥ℋ) p)) q) = Nat.card ↥(MulAction.stabilizer (↥ℋ) p)

Orbit-stabiliser for the fibres of orbitOfCosetTranslate. The number of coset classes that translate p into the same orbit as q does, times the order of the stabiliser of q inside stabilizer ℋ p, is the order of stabilizer ℋ p.

q ranges over arbitrary classes rather than classes of a chosen representative, so a consumer already holding a class can apply this directly, with no QuotientGroup.induction_on step and no representative to discharge afterwards. Use ..._inv_smul below when a representative is what is in hand instead.

Carries no finiteness hypothesis, and holds verbatim in the infinite case under Nat.card's convention that an infinite type has cardinality 0 — so it may be used without first establishing that any of the three groups is finite.

theorem TauCeti.card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_inv_smul {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (h : ↥ℋ) : Nat.card { r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ // orbitOfCosetTranslate p r = orbitOfCosetTranslate p ↑h } * Nat.card ↥(MulAction.stabilizer (↥𝒢) (h⁻¹ • p)) = Nat.card ↥(MulAction.stabilizer (↥ℋ) p)

The multiplicity identity at a chosen representative. For h : ℋ, the number of coset classes translating p into the same orbit as the class of h does, times the order of the stabiliser of the translate h⁻¹ • p inside 𝒢, is the order of the stabiliser of p inside ℋ.

The orbit-indexed form, which is what a consumer summing over orbits wants, is card_fiber_orbitOfCosetTranslate_mul_cardStabilizerOnOrbit below.

This is the form to reach for when a representative h : ℋ is what is in hand rather than a class, and when the stabiliser weight is wanted in 𝒢 itself rather than in 𝒢.subgroupOf ℋ — the shape a coset-indexed sum over 𝒢-stabilisers needs. For an arbitrary class, and for the weight in 𝒢.subgroupOf ℋ, use card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_coset above.

theorem TauCeti.card_fiber_orbitOfCosetTranslate_eq_relIndex {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (h : ↥ℋ) : Nat.card { r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ // orbitOfCosetTranslate p r = orbitOfCosetTranslate p ↑h } = (𝒢.subgroupOf ℋ).relIndex (MulAction.stabilizer (↥ℋ) (h⁻¹ • p))

The fibre size as a relative index. The representative specialisation of card_fiber_orbitOfCosetTranslate_eq_index_stabilizer: for h : ℋ, the number of coset classes translating p into the same 𝒢-orbit as the class of h is the relative index of 𝒢 in the stabiliser of the translate h⁻¹ • p in ℋ, that is, [stabilizer ℋ (h⁻¹ • p) : stabilizer 𝒢 (h⁻¹ • p)].

The multiplicative identity card_fiber_orbitOfCosetTranslate_mul_card_stabilizer_inv_smul degenerates to 0 = 0 when the stabilisers are infinite; this form determines the fibre size in every case, for instance for the infinite cyclic stabilisers of cusps of Fuchsian groups.

theorem TauCeti.card_fiber_orbitOfCosetTranslate_mul_cardStabilizerOnOrbit {G : Type u_1} [Group G] {α : Type u_2} [MulAction G α] {𝒢 ℋ : Subgroup G} (hle : 𝒢 ≤ ℋ) (p : α) (q : ↥ℋ ⧸ 𝒢.subgroupOf ℋ) : Nat.card { r : ↥ℋ ⧸ 𝒢.subgroupOf ℋ // orbitOfCosetTranslate p r = orbitOfCosetTranslate p q } * cardStabilizerOnOrbit (orbitOfCosetTranslate p q) = Nat.card ↥(MulAction.stabilizer (↥ℋ) p)

The orbit-indexed form, which is the one a consumer wants: the weight is TauCeti.cardStabilizerOnOrbit, a function of the orbit rather than of a representative.

A sum over MulAction.orbitRel.Quotient 𝒢 α weights each orbit once, and the roadmap sum Σ_P (1/e_P) reads e_P off the orbit, so a use site holding a class q can apply this directly instead of doing QuotientGroup.induction_on and rewriting the order into orbit form by hand.

theorem TauCeti.sum_card_fixedBy_mul_card_fixedBy_eq_card_doubleCosetQuotient_mul_card_group {G : Type u_1} [Group G] [Fintype G] (H K : Subgroup G) : ∑ g : G, Nat.card ↑(MulAction.fixedBy (G ⧸ H) g) * Nat.card ↑(MulAction.fixedBy (G ⧸ K) g) = Nat.card (DoubleCoset.Quotient ↑H ↑K) * Nat.card G

Double cosets are counted by fixed cosets. For a finite group G and subgroups H and K, the sum over g : G of the number of cosets of H fixed by g times the number of cosets of K fixed by g is the number of double cosets H \ G / K, times the order of G.