The Mackey decomposition as an isomorphism of representations #
Let H and K be subgroups of a group G and let A be a representation of H over a
commutative ring k. Restricting the induced representation Ind_H^G A to K splits it as a
direct sum over the double cosets K \ G / H:
Res_K (Ind_H^G A) ≅ ⨁_{KsH ∈ K \ G / H} Ind_{K ⊓ sHs⁻¹}^K (Res ({}^s A)),
where s is the chosen representative Quotient.out of each double coset. This file proves
that decomposition as a natural isomorphism in Rep k K, refining the character form
TauCeti.character_resFDRep_indFDRep_mackey. No finiteness is assumed: Mathlib's induced
representation is compactly supported, so the decomposition holds for arbitrary G, H and K.
The summands are Rep.mackeySummand, which are Mathlib's Rep.ind of the restriction of
A along TauCeti.mackeyToH : K ⊓ sHs⁻¹ → H, y ↦ s⁻¹ y s; as for the finite-dimensional
TauCeti.mackeySummand, this is the restriction of the conjugate representation {}^s A to the
Mackey subgroup (Rep.mackeySummand_eq_ind_res_conjRep).
In Mathlib's convention Ind_H^G A is the space of coinvariants (k[G] ⊗ A)_H, with
⟦h g ⊗ₜ h a⟧ = ⟦g ⊗ₜ a⟧ for h ∈ H, and x ∈ G acts by ⟦g ⊗ₜ a⟧ ↦ ⟦g x⁻¹ ⊗ₜ a⟧. The summand
of the representative s is included through Rep.mackeyInclusion.
Main definitions #
Rep.mackeySummand: the summandInd_{K ⊓ sHs⁻¹}^K (Res ({}^s A))inRep k K.Rep.mackeyInclusion: its embedding intoRes_K (Ind_H^G A).Rep.mackeyDirectSum: the direct sum of the summands overK \ G / H, andRep.mackeySummandFunctor,Rep.mackeyDirectSumFunctor, the same constructions as functors ofA.Rep.mackeyDecomposition: the Mackey decompositionRes_K (Ind_H^G A) ≅ ⨁_{KsH} Ind_{K ⊓ sHs⁻¹}^K (Res ({}^s A)).Rep.mackeyDecompositionNatIso: the decomposition as a natural isomorphism of functorsRep k H ⥤ Rep k K.
Main statements #
Rep.mackeySummand_eq_ind_res_conjRep: the summand is induced from the restriction of the conjugate representation{}^s A.Rep.mackeyDecomposition_hom_hom_apply_mkandRep.mackeyDecomposition_inv_hom_apply_lof: the two directions of the decomposition on generators.
References #
- J.-P. Serre, Linear Representations of Finite Groups, Section 7.3.
- C. W. Curtis, I. Reiner, Methods of Representation Theory, Vol. I, Section 10.
The classical decidable equality on K \ G / H, used throughout this file: a double coset
quotient carries no canonical one, and DirectSum.lof and DirectSum.linearMap_ext need it.
Equations
Instances For
The Mackey summand attached to s : G, as a representation of K: the representation
A of H, pulled back to the Mackey subgroup K ⊓ sHs⁻¹ along y ↦ s⁻¹ y s, and induced up to
K. This is Ind_{K ⊓ sHs⁻¹}^K (Res ({}^s A))
(Rep.mackeySummand_eq_ind_res_conjRep); TauCeti.mackeySummand is its
finite-dimensional counterpart.
Equations
- Rep.mackeySummand H K s A = Rep.ind ((TauCeti.mackeySubgroup s H K).subgroupOf K).subtype (Rep.res (TauCeti.mackeyToH s H K) A)
Instances For
The Mackey summand is the conjugate representation {}^s A, restricted along the inclusion
of the Mackey subgroup into sHs⁻¹ and induced up to K. The remaining restriction is along the
identification of K ⊓ sHs⁻¹ with its copy inside K.
The embedding of the Mackey summand at s into Res_K (Ind_H^G A),
⟦u ⊗ₜ a⟧ ↦ ⟦s⁻¹ u ⊗ₜ a⟧ (Rep.mackeyInclusion_hom_apply_mk). It is the morphism
corresponding under the induction--restriction adjunction to a ↦ ⟦s⁻¹ ⊗ₜ a⟧.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The embedding of the Mackey summand on generators: ⟦u ⊗ₜ a⟧ ↦ ⟦s⁻¹ u ⊗ₜ a⟧.
The direct sum of the Mackey summands over the double cosets K \ G / H, each built from the
chosen representative Quotient.out.
Equations
- Rep.mackeyDirectSum H K A = Rep.of (Representation.directSum fun (D : DoubleCoset.Quotient ↑K ↑H) => (Rep.mackeySummand H K (Quotient.out D) A).ρ)
Instances For
The Mackey summand at s as a functor of the representation of H: restriction along
TauCeti.mackeyToH followed by induction up to K.
Equations
- Rep.mackeySummandFunctor H K s = (Rep.resFunctor (TauCeti.mackeyToH s H K)).comp (Rep.indFunctor k ((TauCeti.mackeySubgroup s H K).subgroupOf K).subtype)
Instances For
The direct sum of the Mackey summands, as a functor of the representation of H: it sends A
to Rep.mackeyDirectSum H K A (Rep.mackeyDirectSumFunctor_obj) and on morphisms it applies
Rep.mackeySummandFunctor in each summand (Rep.mackeyDirectSumFunctor_map_hom_lof).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The direct sum functor sends a representation of H to the direct sum of its Mackey
summands.
The direct sum of the Mackey summands acts summandwise on morphisms: on the generator
⟦u ⊗ₜ a⟧ of the summand of D it is ⟦u ⊗ₜ f a⟧ in the summand of D.
The Mackey decomposition formula. For subgroups H and K of G and a representation
A of H, restricting the induced representation Ind_H^G A to K gives the direct sum, over
the double cosets K \ G / H, of the Mackey summands
Ind_{K ⊓ sHs⁻¹}^K (Res ({}^s A)) at the chosen representatives s.
On generators, ⟦h s⁻¹ u ⊗ₜ a⟧ ↦ ⟦u ⊗ₜ h⁻¹ a⟧ in the summand of KsH
(Rep.mackeyDecomposition_hom_hom_apply_mk), and backwards ⟦u ⊗ₜ a⟧ ↦ ⟦s⁻¹ u ⊗ₜ a⟧
(Rep.mackeyDecomposition_inv_hom_apply_lof). It is natural in A
(Rep.mackeyDecompositionNatIso).
Equations
Instances For
The Mackey decomposition on generators: ⟦h s⁻¹ u ⊗ₜ a⟧ ↦ ⟦u ⊗ₜ h⁻¹ a⟧ in the summand of the
double coset D, where s = D.out, h ∈ H and u ∈ K. Every element of G can be written in
this form for a unique D.
The inverse of the Mackey decomposition on generators: ⟦u ⊗ₜ a⟧ ↦ ⟦s⁻¹ u ⊗ₜ a⟧ from the
summand of the double coset D, where s = D.out. It is Rep.mackeyInclusion on each
summand.
The Mackey decomposition, naturally in the representation: the functor
A ↦ Res_K (Ind_H^G A) is naturally isomorphic to the direct sum of the Mackey summands.
Equations
- Rep.mackeyDecompositionNatIso H K = (CategoryTheory.NatIso.ofComponents (fun (A : Rep.{?u.1, ?u.1, ?u.1} k ↥H) => A.mackeyDecomposition.symm) ⋯).symm
Instances For
The components of Rep.mackeyDecompositionNatIso are the Mackey decompositions.