The Mackey decomposition formula

Let H and K be subgroups of a group G, with H of finite index. Restricting to K a representation induced from H decomposes as a sum indexed by the double cosets K \ G / H: the summand attached to a representative s is the conjugate {}^s A, a representation of sHs⁻¹, restricted to the Mackey subgroup K ⊓ sHs⁻¹ and induced back up to K.

This file proves that decomposition on characters, and on the class functions underneath them. The combinatorial spine is TauCeti.mackeyQuotientEquiv: the left cosets G ⧸ H are the disjoint union, over the double cosets K \ G / H, of the K-orbits, and the orbit of sH is a copy of K ⧸ (K ⊓ sHs⁻¹) because K ⊓ sHs⁻¹ is the stabilizer of sH (TauCeti.stabilizer_eq_mackeySubgroup_subgroupOf). Sorting the induced-character sum TauCeti.character_indFDRep_sum_quotient along that bijection is the whole proof: the coset u s H contributes χ(s⁻¹ u⁻¹ x u s) exactly when u⁻¹ x u lies in the Mackey subgroup, which is the summand of the induced class function on K.

Counting the same bijection instead of summing over it gives the classical index formula [G : H] = ∑_{KsH} [K : K ⊓ sHs⁻¹] (TauCeti.index_eq_sum_relIndex_mackeySubgroup), the dimension shadow of the decomposition.

The summands are built from the fixed representatives Quotient.out: no representative-independent summand is asserted, only that a different representative gives a conjugate Mackey subgroup (TauCeti.mackeySubgroup_conj). The splitting TauCeti.mackeyQuotientEquiv itself accepts any choice of representatives.

Main definitions

• TauCeti.mackeyCoset: the injection K ⧸ (K ⊓ sHs⁻¹) → G ⧸ H, u ↦ u s H, whose image is the K-orbit of sH.
• TauCeti.mackeyQuotientEquiv: the resulting bijection (Σ KsH ∈ K \ G / H, K ⧸ (K ⊓ sHs⁻¹)) ≃ G ⧸ H.
• TauCeti.mackeyToH: the homomorphism K ⊓ sHs⁻¹ → H, y ↦ s⁻¹ y s, along which the Mackey summand pulls a representation of H back to the Mackey subgroup.
• TauCeti.mackeyClassFun: the conjugated function y ↦ f (s⁻¹ y s) on the Mackey subgroup; it is a class function as soon as f is one, and inducing it up to K gives the character of the Mackey summand when f is a character.
• TauCeti.mackeyClassFunction: the same conjugated class function, bundled as an element of TauCeti.ClassFunction.
• TauCeti.mackeySummand: the Mackey summand Ind_{K ⊓ sHs⁻¹}^K Res ({}^s A) as an FDRep k K.

Main statements

• TauCeti.index_eq_sum_relIndex_mackeySubgroup: [G : H] = ∑_{KsH} [K : K ⊓ sHs⁻¹].
• TauCeti.mackeyClassFun_mem_classFunction: the conjugate of a class function is one.
• Subgroup.indClassFun_mackey: the Mackey decomposition for induced class functions.
• Subgroup.comap_subtype_indClassFunction_mackey: the same decomposition as an identity of bundled class functions.
• TauCeti.character_resFDRep_indFDRep_mackey: the Mackey decomposition for the character of Res_K (Ind_H^G A).

Implementation notes

The formulas summed over K \ G / H are stated with H of finite index and no finiteness hypothesis on G or K: that is all the induced class function needs, it makes K \ G / H finite (TauCeti.finite_doubleCosetQuotient) and the Mackey subgroup of finite index in K (TauCeti.instIsFiniteRelIndexMackeySubgroup), and it is the hypothesis the induced-character formula carries. An individual summand needs less: TauCeti.mackeySummand and its companions assume only [(mackeySubgroup s H K).IsFiniteRelIndex K], the finiteness that inducing from the Mackey subgroup up to K actually uses.

The Mackey subgroup K ⊓ sHs⁻¹ is a subgroup of G; inducing from it up to K means inducing along the subtype of (K ⊓ sHs⁻¹).subgroupOf K : Subgroup ↥K, so that is the subgroup the sums below are indexed by. TauCeti.mackeyToH absorbs the passage back and forth, and TauCeti.mackeySummand_eq_indFDRep_res_conjFDRep records that the summand really is the restriction of the conjugate representation.

Only the character form is proved here; the isomorphism of representations Res_K (Ind_H^G A) ≅ ⨁_{KsH} Ind_{K ⊓ sHs⁻¹}^K Res ({}^s A) refining it is Rep.mackeyDecomposition, in TauCeti.RepresentationTheory.Induction.Mackey.Decomposition.

References

• J.-P. Serre, Linear Representations of Finite Groups, Chapter 7.3.
• I. M. Isaacs, Character Theory of Finite Groups, Chapter 5.

def TauCeti.mackeyCoset {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : ↥K ⧸ (mackeySubgroup s H K).subgroupOf K → G ⧸ H

The left cosets of H in the double coset KsH, indexed by the Mackey subgroup: u (K ⊓ sHs⁻¹) ↦ u s H. It is well defined because K ⊓ sHs⁻¹ is the stabilizer of sH for the translation action of K on G ⧸ H (TauCeti.stabilizer_eq_mackeySubgroup_subgroupOf).

Equations

• TauCeti.mackeyCoset s H K = Quotient.map' (fun (u : ↥K) => ↑u * s) ⋯

@[simp]

theorem TauCeti.mackeyCoset_mk {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) (u : ↥K) : mackeyCoset s H K ↑u = ↑(↑u * s)

theorem TauCeti.mackeyCoset_out {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) (u : ↥K ⧸ (mackeySubgroup s H K).subgroupOf K) : mackeyCoset s H K u = ↑(↑(Quotient.out u) * s)

TauCeti.mackeyCoset evaluated at the chosen representative of a coset.

theorem TauCeti.mackeyCoset_smul {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) (k : ↥K) (u : ↥K ⧸ (mackeySubgroup s H K).subgroupOf K) : mackeyCoset s H K (k • u) = ↑k • mackeyCoset s H K u

TauCeti.mackeyCoset is K-equivariant for the translation actions of K on K ⧸ (K ⊓ sHs⁻¹) and on G ⧸ H.

noncomputable def TauCeti.mackeyQuotientEquiv {G : Type u_1} [Group G] (H K : Subgroup G) (r : DoubleCoset.Quotient ↑K ↑H → G) (hr : ∀ (D : DoubleCoset.Quotient ↑K ↑H), DoubleCoset.mk K H (r D) = D) : (D : DoubleCoset.Quotient ↑K ↑H) × ↥K ⧸ (mackeySubgroup (r D) H K).subgroupOf K ≃ G ⧸ H

The double-coset splitting of G ⧸ H. Sorting the left cosets of H by the double coset they lie in, G ⧸ H is the disjoint union over K \ G / H of the K-orbits, and the orbit of sH is a copy of K ⧸ (K ⊓ sHs⁻¹).

This is the combinatorial content of the Mackey decomposition. The representatives are any choice r D ∈ D of one element in each double coset; Quotient.out with DoubleCoset.out_eq' is the canonical one.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.mackeyQuotientEquiv_apply {G : Type u_1} [Group G] (H K : Subgroup G) (r : DoubleCoset.Quotient ↑K ↑H → G) (hr : ∀ (D : DoubleCoset.Quotient ↑K ↑H), DoubleCoset.mk K H (r D) = D) (p : (D : DoubleCoset.Quotient ↑K ↑H) × ↥K ⧸ (mackeySubgroup (r D) H K).subgroupOf K) : (mackeyQuotientEquiv H K r hr) p = mackeyCoset (r p.fst) H K p.snd

theorem TauCeti.smul_mackeyQuotientEquiv {G : Type u_1} [Group G] (H K : Subgroup G) (r : DoubleCoset.Quotient ↑K ↑H → G) (hr : ∀ (D : DoubleCoset.Quotient ↑K ↑H), DoubleCoset.mk K H (r D) = D) (k : ↥K) (D : DoubleCoset.Quotient ↑K ↑H) (u : ↥K ⧸ (mackeySubgroup (r D) H K).subgroupOf K) : ↑k • (mackeyQuotientEquiv H K r hr) ⟨D, u⟩ = (mackeyQuotientEquiv H K r hr) ⟨D, k • u⟩

TauCeti.mackeyQuotientEquiv is K-equivariant: translation by k ∈ K keeps the double coset of an index and translates its coset of the Mackey subgroup.

theorem TauCeti.sum_mackeyQuotientEquiv {G : Type u_1} [Group G] {A : Type u_2} [AddCommMonoid A] (H K : Subgroup G) (r : DoubleCoset.Quotient ↑K ↑H → G) (hr : ∀ (D : DoubleCoset.Quotient ↑K ↑H), DoubleCoset.mk K H (r D) = D) [Fintype (G ⧸ H)] [Fintype (DoubleCoset.Quotient ↑K ↑H)] [(D : DoubleCoset.Quotient ↑K ↑H) → Fintype (↥K ⧸ (mackeySubgroup (r D) H K).subgroupOf K)] (F : G ⧸ H → A) : ∑ q : G ⧸ H, F q = ∑ D : DoubleCoset.Quotient ↑K ↑H, ∑ u : ↥K ⧸ (mackeySubgroup (r D) H K).subgroupOf K, F ((mackeyQuotientEquiv H K r hr) ⟨D, u⟩)

Sorting a sum over G ⧸ H by double cosets. Along TauCeti.mackeyQuotientEquiv, a sum over the left cosets G ⧸ H is the sum over the double cosets K \ G / H of the sums over the K-orbits K ⧸ (K ⊓ sHs⁻¹).

theorem TauCeti.index_eq_sum_relIndex_mackeySubgroup {G : Type u_1} [Group G] (H K : Subgroup G) [H.FiniteIndex] : H.index = ∑ D : DoubleCoset.Quotient ↑K ↑H, (mackeySubgroup (Quotient.out D) H K).relIndex K

The double-coset index formula [G : H] = ∑_{KsH ∈ K \ G / H} [K : K ⊓ sHs⁻¹], obtained by counting TauCeti.mackeyQuotientEquiv. It is the dimension shadow of the Mackey decomposition: applying TauCeti.character_resFDRep_indFDRep_mackey at the identity recovers it, multiplied by finrank k A.

def TauCeti.mackeyToH {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) : ↥((mackeySubgroup s H K).subgroupOf K) →* ↥H

The homomorphism K ⊓ sHs⁻¹ → H, y ↦ s⁻¹ y s, along which the Mackey summand pulls a representation of H back to the Mackey subgroup: the Mackey subgroup sits inside sHs⁻¹ (TauCeti.mackeyToConjH) and TauCeti.conjSubgroupEquiv carries sHs⁻¹ back to H.

Its source is (K ⊓ sHs⁻¹).subgroupOf K, the Mackey subgroup read as a subgroup of K, since that is the subgroup the Mackey summand is induced along.

Equations

• TauCeti.mackeyToH s H K = ((TauCeti.conjSubgroupEquiv s H).toMonoidHom.comp (TauCeti.mackeyToConjH s H K)).comp (Subgroup.subgroupOfEquivOfLe ⋯).toMonoidHom

@[simp]

theorem TauCeti.coe_mackeyToH_apply {G : Type u_1} [Group G] (s : G) (H K : Subgroup G) (y : ↥((mackeySubgroup s H K).subgroupOf K)) : ↑((mackeyToH s H K) y) = s⁻¹ * ↑↑y * s

def TauCeti.mackeyClassFun {k : Type u_1} {G : Type u_2} [Group G] (s : G) (H K : Subgroup G) (f : ↥H → k) : ↥((mackeySubgroup s H K).subgroupOf K) → k

The function on the Mackey subgroup obtained from an arbitrary function f on H by conjugating: y ↦ f (s⁻¹ y s), that is, the pullback of f along TauCeti.mackeyToH.

It is a class function whenever f is one (TauCeti.mackeyClassFun_mem_classFunction), and when f is the character of a representation A its induction to K is the character of the Mackey summand attached to s (TauCeti.character_mackeySummand); nothing is assumed of f here.

Equations

• TauCeti.mackeyClassFun s H K f = f ∘ ⇑(TauCeti.mackeyToH s H K)

@[simp]

theorem TauCeti.mackeyClassFun_apply {k : Type u_1} {G : Type u_2} [Group G] (s : G) (H K : Subgroup G) (f : ↥H → k) (y : ↥((mackeySubgroup s H K).subgroupOf K)) : mackeyClassFun s H K f y = f ((mackeyToH s H K) y)

theorem TauCeti.mackeyClassFun_mem_classFunction {k : Type u_1} [Semiring k] {G : Type u_2} [Group G] (s : G) (H K : Subgroup G) {f : ↥H → k} (hf : f ∈ ClassFunction k ↥H) : mackeyClassFun s H K f ∈ ClassFunction k ↥((mackeySubgroup s H K).subgroupOf K)

Conjugating a class function on H gives a class function on the Mackey subgroup: it is the pullback of f along the homomorphism TauCeti.mackeyToH.

def TauCeti.mackeyClassFunction {k : Type u_1} [Semiring k] {G : Type u_2} [Group G] (s : G) (H K : Subgroup G) (f : ↥(ClassFunction k ↥H)) : ↥(ClassFunction k ↥((mackeySubgroup s H K).subgroupOf K))

The conjugated class function TauCeti.mackeyClassFun on the Mackey subgroup, bundled as an element of TauCeti.ClassFunction.

Equations

• TauCeti.mackeyClassFunction s H K f = ⟨TauCeti.mackeyClassFun s H K ↑f, ⋯⟩

@[simp]

theorem TauCeti.mackeyClassFunction_coe {k : Type u_1} [Semiring k] {G : Type u_2} [Group G] (s : G) (H K : Subgroup G) (f : ↥(ClassFunction k ↥H)) : ↑(mackeyClassFunction s H K f) = mackeyClassFun s H K ↑f

theorem Subgroup.indClassFun_mackey {k : Type u_1} [Semiring k] {G : Type u_2} [Group G] (H : Subgroup G) {K : Subgroup G} [H.FiniteIndex] {f : ↥H → k} (hf : f ∈ TauCeti.ClassFunction k ↥H) (x : ↥K) : H.indClassFun f ↑x = ∑ D : DoubleCoset.Quotient ↑K ↑H, ((TauCeti.mackeySubgroup (Quotient.out D) H K).subgroupOf K).indClassFun (TauCeti.mackeyClassFun (Quotient.out D) H K f) x

The Mackey decomposition formula for class functions. For a class function f on a finite-index subgroup H and an element x of a subgroup K, the induced class function Ind_H^G f evaluated at x is the sum, over the double cosets K \ G / H, of the class functions induced to K from the Mackey subgroups.

The character form is TauCeti.character_resFDRep_indFDRep_mackey.

theorem Subgroup.comap_subtype_indClassFunction_mackey {k : Type u_1} [Semiring k] {G : Type u_2} [Group G] (K : Subgroup G) {H : Subgroup G} [H.FiniteIndex] (f : ↥(TauCeti.ClassFunction k ↥H)) : (TauCeti.ClassFunction.comap K.subtype) (H.indClassFunction f) = ∑ D : DoubleCoset.Quotient ↑K ↑H, ((TauCeti.mackeySubgroup (Quotient.out D) H K).subgroupOf K).indClassFunction (TauCeti.mackeyClassFunction (Quotient.out D) H K f)

The Mackey decomposition of a restricted induced class function. Restricting to K a class function induced from H gives the sum, over the double cosets K \ G / H, of the class functions induced to K from the Mackey subgroups.

This is Subgroup.indClassFun_mackey rewritten as an identity of bundled class functions, which is the form the character pairing consumes.

noncomputable def TauCeti.mackeySummand {k G : Type u} [Field k] [Group G] {H K : Subgroup G} (s : G) [(mackeySubgroup s H K).IsFiniteRelIndex K] (A : FDRep k ↥H) : FDRep k ↥K

The Mackey summand attached to a representative s of a double coset in K \ G / H: the conjugate representation {}^s A of sHs⁻¹, restricted to the Mackey subgroup K ⊓ sHs⁻¹ and induced back up to K.

The restriction and the conjugation are packaged into the single homomorphism TauCeti.mackeyToH; TauCeti.mackeySummand_eq_indFDRep_res_conjFDRep unfolds it into the two steps.

Only the Mackey subgroup is assumed of finite index in K, which is what inducing up to K uses; H of finite index in G gives that for every s (TauCeti.instIsFiniteRelIndexMackeySubgroup).

Equations

• TauCeti.mackeySummand s A = TauCeti.indFDRep ((Action.res (FGModuleCat k) (TauCeti.mackeyToH s H K)).obj A)

theorem TauCeti.mackeySummand_eq_indFDRep_res_conjFDRep {k G : Type u} [Field k] [Group G] {H K : Subgroup G} (s : G) [(mackeySubgroup s H K).IsFiniteRelIndex K] (A : FDRep k ↥H) : mackeySummand s A = indFDRep ((Action.res (FGModuleCat k) (Subgroup.subgroupOfEquivOfLe ⋯).toMonoidHom).obj ((Action.res (FGModuleCat k) (mackeyToConjH s H K)).obj (conjFDRep s A)))

The Mackey summand is what its name says: restrict the conjugate representation {}^s A along the inclusion of the Mackey subgroup into sHs⁻¹, then induce up to K. The remaining restriction is along the identification of K ⊓ sHs⁻¹ with its copy inside K.

@[simp]

theorem TauCeti.character_res_mackeyToH {k G : Type u} [Field k] [Group G] {H K : Subgroup G} (s : G) (A : FDRep k ↥H) : FDRep.character ((Action.res (FGModuleCat k) (mackeyToH s H K)).obj A) = mackeyClassFun s H K A.character

The character of the representation the Mackey summand is induced from: pulling A back along TauCeti.mackeyToH conjugates its character, y ↦ χ_A (s⁻¹ y s). Naming this identification keeps Action.res out of the character computations below.

@[simp]

theorem TauCeti.character_mackeySummand {k G : Type u} [Field k] [Group G] {H K : Subgroup G} (s : G) [(mackeySubgroup s H K).IsFiniteRelIndex K] (A : FDRep k ↥H) (x : ↥K) : (mackeySummand s A).character x = ((mackeySubgroup s H K).subgroupOf K).indClassFun (mackeyClassFun s H K A.character) x

The character of a Mackey summand is the induced class function of the conjugated character.

theorem TauCeti.character_resFDRep_indFDRep_mackey {k G : Type u} [Field k] [Group G] {H K : Subgroup G} [H.FiniteIndex] (A : FDRep k ↥H) (x : ↥K) : (K.resFDRep (indFDRep A)).character x = ∑ D : DoubleCoset.Quotient ↑K ↑H, (mackeySummand (Quotient.out D) A).character x

The Mackey decomposition formula, character form. For a finite-dimensional representation A of a finite-index subgroup H and an element x of a subgroup K, the character of Res_K (Ind_H^G A) at x is the sum, over the double cosets K \ G / H, of the characters of the Mackey summands.

The character of Ind_H^G A at x : K, read on G, is the same number: FDRep.character_actionRes is a simp lemma rewriting the left-hand side into it.