Documentation

TauCeti.RepresentationTheory.Induction.FiniteDimensional.Projection

The projection formula on finite-dimensional representations #

For a finite-index subgroup S ≤ G over a field k, this file specializes the projection formula TauCeti.indProjection of TauCeti/RepresentationTheory/Induction/Projection.lean to finite-dimensional representations, as

Ind_S^G (A ⊗ Res_S^G B) ≅ (Ind_S^G A) ⊗ B in FDRep k G.

The forgetful functor forget₂ (FDRep k G) (Rep k G) is fully faithful, so the isomorphism is obtained as the preimage of its Rep k G counterpart, conjugated by the comparison TauCeti.indFDRepForgetIso between the small carrier chosen by TauCeti.indFDRep and Mathlib's.

Main definitions #

Main statements #

Implementation notes #

The subgroup has finite index because that is what keeps an induced representation finite-dimensional. The ambient group is confined to the universe of k by the proof route through the Rep-level TauCeti.indProjection, not by the statement: FDRep k G is monoidal for G in any universe, so both sides of the isomorphism elaborate with G free. Lifting the restriction would mean rebuilding the isomorphism at the universe-polymorphic Representation.Equiv level, which needs a tensor-congruence for Representation.Equiv that the library does not have.

source
noncomputable def TauCeti.indFDRepProjection {k G : Type u} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (B : FDRep k G) :
indFDRep (CategoryTheory.MonoidalCategoryStruct.tensorObj A ((Action.res (FGModuleCat k) S.subtype).obj B)) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (indFDRep A) B

The projection formula on finite-dimensional representations, Ind_S^G (A ⊗ Res_S^G B) ≅ (Ind_S^G A) ⊗ B in FDRep k G.

On isomorphism classes this becomes the statement that induction is a homomorphism of modules over the representation ring, TauCeti.repRingInd_mul_repRingRes.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.forget₂_map_indFDRepProjection_hom {k G : Type u} [Field k] [Group G] {S : Subgroup G} [S.FiniteIndex] (A : FDRep k ↥S) (B : FDRep k G) :
    (CategoryTheory.forget₂ (FDRep k G) (Rep.{u, u, u} k G)).map (indFDRepProjection A B).hom = CategoryTheory.CategoryStruct.comp (indFDRepForgetIso (CategoryTheory.MonoidalCategoryStruct.tensorObj A ((Action.res (FGModuleCat k) S.subtype).obj B))).hom (CategoryTheory.CategoryStruct.comp (indProjection S.subtype ((CategoryTheory.forget₂ (FDRep k ↥S) (Rep.{u, u, u} k ↥S)).obj A) ((CategoryTheory.forget₂ (FDRep k G) (Rep.{u, u, u} k G)).obj B)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorIso (indFDRepForgetIso A).symm (CategoryTheory.Iso.refl ((CategoryTheory.forget₂ (FDRep k G) (Rep.{u, u, u} k G)).obj B))).hom (CategoryTheory.eqToHom ⋯)))

    Read through the fully faithful forget₂ (FDRep k G) (Rep k G), the forward direction of TauCeti.indFDRepProjection is the Rep-level projection formula conjugated by the small-carrier comparisons TauCeti.indFDRepForgetIso.