The Mackey decomposition of intertwining spaces

The representation-level Mackey decomposition and the two induction–restriction adjunctions identify the intertwining space between two induced representations with a product of intertwining spaces over the double-coset intersections. This holds over a commutative ring, without semisimplicity or a restriction on the characteristic. For finite-dimensional representations over a field it gives an equality of natural-number dimensions, rather than an equality of their casts into the field.

The direction of Hom matters: Hom(Ind A, Ind B) corresponds to Hom(Res A, Res ({}^s B)) over H ∩ sKs⁻¹. In modular characteristic reversing both Hom spaces requires additional hypotheses, whereas the equivalence here does not.

References

• J.-P. Serre, Linear Representations of Finite Groups, §7.3–7.4.
• C. W. Curtis and I. Reiner, Methods of Representation Theory, Vol. I, §10.

noncomputable def Rep.indHomMackeyLinearEquiv {k G : Type u} [CommRing k] [Group G] [Finite G] {H K : Subgroup G} (A : Rep.{u, u, u} k ↥H) (B : Rep.{u, u, u} k ↥K) : (ind H.subtype A ⟶ ind K.subtype B) ≃ₗ[k] (D : DoubleCoset.Quotient ↑H ↑K) → res ((TauCeti.mackeySubgroup (Quotient.out D) K H).subgroupOf H).subtype A ⟶ res (TauCeti.mackeyToH (Quotient.out D) K H) B

The intertwining space between induced representations decomposes over double cosets, without any semisimplicity assumption.

Equations

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

@[simp]

theorem Rep.indHomMackeyLinearEquiv_apply {k G : Type u} [CommRing k] [Group G] [Finite G] {H K : Subgroup G} (A : Rep.{u, u, u} k ↥H) (B : Rep.{u, u, u} k ↥K) (φ : ind H.subtype A ⟶ ind K.subtype B) (D : DoubleCoset.Quotient ↑H ↑K) : (A.indHomMackeyLinearEquiv B) φ D = (resCoindHomEquiv.{u, u, u, u} ((TauCeti.mackeySubgroup (Quotient.out D) K H).subgroupOf H).subtype A (res (TauCeti.mackeyToH (Quotient.out D) K H) B)).symm (CategoryTheory.CategoryStruct.comp ((A.homDirectSumLinearEquiv fun (E : DoubleCoset.Quotient ↑H ↑K) => mackeySummand K H (Quotient.out E) B) (CategoryTheory.CategoryStruct.comp ((indResHomEquiv H.subtype A (ind K.subtype B)) φ) B.mackeyDecomposition.hom) D) (res (TauCeti.mackeyToH (Quotient.out D) K H) B).indCoindIso.hom)

A double-coset component is obtained by Frobenius reciprocity, the Mackey decomposition, projection onto that summand, and the finite-index induction–coinduction adjunction.

noncomputable def FDRep.indHomMackeyLinearEquiv {k G : Type u} [Field k] [Group G] [Finite G] {H K : Subgroup G} (A : FDRep k ↥H) (B : FDRep k ↥K) : (TauCeti.indFDRep A ⟶ TauCeti.indFDRep B) ≃ₗ[k] (D : DoubleCoset.Quotient ↑H ↑K) → ((TauCeti.mackeySubgroup (Quotient.out D) K H).subgroupOf H).resFDRep A ⟶ (Action.res (FGModuleCat k) (TauCeti.mackeyToH (Quotient.out D) K H)).obj B

The finite-dimensional Mackey decomposition of intertwining spaces, over every field.

Equations

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

@[simp]

theorem FDRep.indHomMackeyLinearEquiv_apply {k G : Type u} [Field k] [Group G] [Finite G] {H K : Subgroup G} (A : FDRep k ↥H) (B : FDRep k ↥K) (φ : TauCeti.indFDRep A ⟶ TauCeti.indFDRep B) (D : DoubleCoset.Quotient ↑H ↑K) : (A.indHomMackeyLinearEquiv B) φ D = ((((TauCeti.mackeySubgroup (Quotient.out D) K H).subgroupOf H).resFDRep A).forget₂HomLinearEquiv ((Action.res (FGModuleCat k) (TauCeti.mackeyToH (Quotient.out D) K H)).obj B)) ((((CategoryTheory.forget₂ (FDRep k ↥H) (Rep.{u, u, u} k ↥H)).obj A).indHomMackeyLinearEquiv ((CategoryTheory.forget₂ (FDRep k ↥K) (Rep.{u, u, u} k ↥K)).obj B)) (CategoryTheory.CategoryStruct.comp (TauCeti.indFDRepForgetIso A).inv (CategoryTheory.CategoryStruct.comp (((TauCeti.indFDRep A).forget₂HomLinearEquiv (TauCeti.indFDRep B)).symm φ) (TauCeti.indFDRepForgetIso B).hom)) D)

Each finite-dimensional component is the corresponding Rep component, transported through the forgetful Hom equivalence and the induced-model comparison isomorphisms.