Finiteness of the double-coset quotient

A double coset HgK is a union of left cosets of K, so the double cosets H \ G / K are a quotient of G ⧸ K: the map gK ↦ HgK is well defined and surjective (TauCeti.doubleCosetMk_out_mk is the well-definedness, in the form the surjection uses). Consequently H \ G / K is finite as soon as K has finite index, with no finiteness assumption on G itself.

This is the instance that lets a sum be taken over H \ G / K; the Mackey decomposition (TauCeti.RepresentationTheory.Induction.Mackey.Basic) is its first consumer, where the index of the subgroup being induced from is the only finiteness available.

The double cosets partition G, so for finite G their sizes add up to the order of G (Subgroup.sum_card_quotToDoubleCoset).

A sum over H \ G / K of values at chosen representatives often comes with a proof that it does not depend on the choice; TauCeti.eq_of_sum_doubleCoset_rep_eq extracts from this that each value depends only on its double coset.

Main statements

• TauCeti.finite_doubleCosetQuotient: H \ G / K is finite when K has finite index in G.
• Subgroup.sum_card_quotToDoubleCoset: the sizes of the double cosets add up to |G|.
• Subgroup.sum_card_quotToDoubleCoset_div_card_eq_index: the numbers |HgK| / |H| add up to the index of H.
• TauCeti.eq_of_sum_doubleCoset_rep_eq: a value whose sum over double-coset representatives is independent of the representatives is itself constant on double cosets.

theorem TauCeti.doubleCosetMk_out_mk {G : Type u_1} [Group G] (H K : Subgroup G) (g : G) : DoubleCoset.mk H K (Quotient.out ↑g) = DoubleCoset.mk H K g

Replacing an element by the chosen representative of its left K-coset does not change its double coset.

instance TauCeti.finite_doubleCosetQuotient {G : Type u_1} [Group G] (H K : Subgroup G) [K.FiniteIndex] : Finite (DoubleCoset.Quotient ↑H ↑K)

The double cosets H \ G / K are finite when K has finite index: they are the image of the finite set G ⧸ K under gK ↦ HgK.

theorem TauCeti.eq_of_sum_doubleCoset_rep_eq {G : Type u_1} [Group G] {A : Type u_2} [AddCancelCommMonoid A] (H K : Subgroup G) [Fintype (DoubleCoset.Quotient ↑H ↑K)] (T : G → A) (hT : ∀ (r : DoubleCoset.Quotient ↑H ↑K → G), (∀ (D : DoubleCoset.Quotient ↑H ↑K), DoubleCoset.mk H K (r D) = D) → ∑ D : DoubleCoset.Quotient ↑H ↑K, T (r D) = ∑ D : DoubleCoset.Quotient ↑H ↑K, T (Quotient.out D)) {s s' : G} (h : DoubleCoset.mk H K s = DoubleCoset.mk H K s') : T s = T s'

A value at a double-coset representative is determined by its double coset if the sum is: if the sum over H \ G / K of the values of T at representatives does not depend on the choice of representatives, then T s = T s' whenever s and s' lie in the same double coset. Comparing the canonical choice Quotient.out with the ones that replace the representative of a single double coset by s, resp. s', leaves only the terms at s and s'.

theorem Subgroup.sum_card_quotToDoubleCoset {G : Type u_1} [Group G] [Finite G] (H K : Subgroup G) [Fintype (DoubleCoset.Quotient ↑H ↑K)] : ∑ q : DoubleCoset.Quotient ↑H ↑K, Nat.card ↑(DoubleCoset.quotToDoubleCoset H K q) = Nat.card G

The double cosets partition the group: for finite G, the sizes of the double cosets HgK add up to the order of G.

theorem Subgroup.sum_card_quotToDoubleCoset_div_card_eq_index {G : Type u_1} [Group G] [Finite G] (H K : Subgroup G) [Fintype (DoubleCoset.Quotient ↑H ↑K)] : ∑ q : DoubleCoset.Quotient ↑H ↑K, Nat.card ↑(DoubleCoset.quotToDoubleCoset H K q) / Nat.card ↥H = H.index

The double cosets count the right cosets: each double coset HsK of a finite group is a union of |HsK| / |H| right cosets of H, and these numbers add up, over H \ G / K, to the index of H.