Schur vanishing and exact pairings across C ⥤ Ind C

RS.Classical.Deligne.IndSchur transports the symmetric-group action on tensor powers along the embedding RS.indOf : C ⥤ Ind C at the level of single permutations, and RS.Classical.Deligne.IndOfMonoidal packages the comparison data as a strong (braided) monoidal structure on indOf. RS.Classical.Deligne.ScalarLinear turns a scalar unit ψ : ℂ ≃+* End (𝟙_ C) into ℂ-linear structures on C and on Ind C. This file joins the three.

• RS.monoidalMap_unitConj — a strong monoidal functor carries the left-unitor conjugate of a unit endomorphism to the left-unitor conjugate of its comparison transport;
• RS.exactPairingMap — a strong monoidal functor carries an exact pairing to an exact pairing, with the coevaluation ε ≫ F h ≫ δ and the evaluation μ ≫ F ε_ ≫ η; Mathlib has only the converse (CategoryTheory.ExactPairing.ofFaithful, which reflects a pairing along a faithful monoidal functor), so the two triangle identities are proved here from the oplax coherences;
• RS.exactPairingIndOf — duals transport: the embedding C ⥤ Ind C carries an exact pairing to an exact pairing;
• RS.indOf_map_scalarSmul and RS.permAlg_indOf_conj_scalarUnit — the embedding intertwines the scalar actions induced by ψ and by RS.indScalarUnit ψ, hence the whole group-algebra action;
• RS.schurKilled_indOf — Schur vanishing transports: for the ℂ-linear structures induced by a single scalar unit ψ on C and on Ind C, a shape kills an embedded object exactly when it kills the object downstairs.

Both linear structures are installed by letI inside the statements, as in the acceptance section of RS.Classical.Deligne.ScalarLinear: RS.linearOfScalarUnit is deliberately not an instance, and taking both structures from the same ψ is what makes the two sides of RS.schurKilled_indOf comparable — no compatibility hypothesis between ψ and an ambient linear structure is needed.

Strong monoidal functors: unit conjugates and duals

theorem RS.monoidalMap_unitConj {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {B : Type u'} [CategoryTheory.Category.{v', u'} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.Functor A B) [F.Monoidal] (X : A) (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit A) : F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (CategoryTheory.CategoryStruct.comp (F.map u) (CategoryTheory.Functor.OplaxMonoidal.η F))) (F.obj X)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom)

Transport of unit-endomorphism conjugates: a strong monoidal functor carries the left-unitor conjugate of a unit endomorphism u to the left-unitor conjugate of the comparison transport of u.

@[implicit_reducible]

def RS.exactPairingMap {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.MonoidalCategory A] {B : Type u'} [CategoryTheory.Category.{v', u'} B] [CategoryTheory.MonoidalCategory B] (F : CategoryTheory.Functor A B) [F.Monoidal] {X Y : A} [CategoryTheory.ExactPairing X Y] : CategoryTheory.ExactPairing (F.obj X) (F.obj Y)

A strong monoidal functor carries an exact pairing to an exact pairing: the coevaluation is the unit comparison followed by the image of the coevaluation and the cotensorator, the evaluation is the tensorator followed by the image of the evaluation and the counit comparison. Both triangle identities descend from the corresponding identities downstairs, whose image is expanded by the oplax coherences of CategoryTheory.Functor.Monoidal.

Equations

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

Duals along the embedding

@[instance_reducible]

noncomputable instance RS.exactPairingIndOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.ExactPairing (indOf.obj X) (indOf.obj Y)

Duals transport along the embedding C ⥤ Ind C: the embedding is strong monoidal (RS.indOfMonoidal), and a strong monoidal functor preserves exact pairings.

Equations

• RS.exactPairingIndOf X Y = RS.exactPairingMap RS.indOf

The scalar action along the embedding

theorem RS.scalarHom_indScalarUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (c : ℂ) : scalarHom (indScalarUnit ψ) c = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε indOf) (CategoryTheory.CategoryStruct.comp (indOf.map (ψ c)) (CategoryTheory.Functor.OplaxMonoidal.η indOf))

The scalar unit of Ind C is the comparison transport of the scalar unit of C along the strong monoidal embedding.

theorem RS.indOf_map_scalarSmul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (c : ℂ) {X Y : C} (f : X ⟶ Y) : indOf.map (scalarSmul ψ c f) = scalarSmul (indScalarUnit ψ) c (indOf.map f)

The embedding intertwines the scalar actions: indOf carries the action of c induced by ψ to the action of c induced by RS.indScalarUnit ψ. No compatibility with an ambient linear structure is asked: both actions come from the same ψ.

The group-algebra action and Schur vanishing

theorem RS.permAlg_indOf_conj_scalarUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (X : C) {n : ℕ} (x : SymGroupAlgebra n) : CategoryTheory.CategoryStruct.comp ((permAlg (indOf.obj X) n) x) (indOfPowIso X n).hom = CategoryTheory.CategoryStruct.comp (indOfPowIso X n).hom (indOf.map ((permAlg X n) x))

Transport of the group-algebra action: for the ℂ-linear structures induced on C and on Ind C by one scalar unit ψ, the action of the symmetric-group algebra on the tensor powers of an embedded object is conjugate, under RS.indOfPowIso, to the embedded action.

theorem RS.schurKilled_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (P : SchurPackage) (X : C) (μ : YoungDiagram) : SchurKilled P (indOf.obj X) μ ↔ SchurKilled P X μ

Schur vanishing transports along the embedding C ⥤ Ind C: with the ℂ-linear structures induced on C and on Ind C by one scalar unit ψ, a shape kills an embedded object exactly when it kills the object downstairs.

Acceptance