Schur-vanishing transport along the embedding C ⥤ Ind C

RS.Classical.Deligne.IndSchur transports the permutation action on tensor powers across the embedding at the permMor level, and RS.Classical.Deligne.ScalarLinear equips Ind C with the ℂ-linear structure induced by a scalar unit ψ : ℂ ≃+* End (𝟙_ C). This file joins the two: under letI := linearOfScalarUnit (indScalarUnit ψ) the whole group-algebra action transports, and Schur vanishing on an embedded object is Schur vanishing downstairs.

• RS.smul_eq_unitConj — a scalar acts by conjugating the unit endomorphism c • 𝟙 through the left unitor;
• RS.dayCoyonedaIso_hom_leftUnitor/RS.dayYonedaIso_hom_leftUnitor — the Day tensor of (co)representables intertwines the left unitor, completing the coherence package of RS.dayCoyonedaIso_hom_braiding/_associator;
• RS.indOf_leftUnitor_hom — the unit comparison and the embedding-tensor comparison satisfy the left unitality of a monoidal functor up to isomorphism;
• RS.indOf_map_smul — the embedding carries the scalar action of C to the scalar action RS.scalarSmul (indScalarUnit ψ);
• RS.permAlg_indOf_conj — the symmetric-group algebra action on the powers of an embedded object is conjugate, under RS.indOfPowIso, to the embedded action;
• RS.schurKilled_indOf_iff — Schur vanishing transports faithfully along C ⥤ Ind C, with the HasScalarUnit instantiation RS.schurKilled_indOf_iff_of_hasScalarUnit.

The scalar action as a unitor conjugate

theorem RS.smul_eq_unitConj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.Linear ℂ D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.MonoidalLinear ℂ D] (c : ℂ) {X Y : D} (f : X ⟶ Y) : c • f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f))

The scalar action is a unitor conjugate: c • f is precomposition with the left-unitor conjugate of the unit endomorphism c • 𝟙.

The Day left unitor on corepresentables

theorem RS.dayUnitIso_hom_app_nu {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] : (CategoryTheory.ConcreteCategory.hom ((dayUnitIso D).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)

The Day unit comparison carries the canonical unit element to the identity.

theorem RS.dayUnitIso_inv_app_id {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] : (CategoryTheory.ConcreteCategory.hom ((dayUnitIso D).inv.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit

The inverse of the Day unit comparison carries the identity to the canonical unit element.

theorem RS.whiskerRight_dayUnitIso_inv_app_unitElt {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.whiskerRight (dayUnitIso D).inv { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }).natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) a))) (dayCoyonedaUnitElt (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) a) = (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v))).η { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D, a))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit, CategoryTheory.CategoryStruct.id a)

Right-whiskering the inverse Day unit comparison carries the canonical element of the Day tensor to the Kan-extension unit evaluated on the canonical unit element.

theorem RS.day_leftUnitor_hom_app_eta {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalCategory.DayFunctor D (Type v)) (y : D) (x : F.functor.obj y) : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.MonoidalCategoryStruct.leftUnitor F).hom.natTrans.app (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) y))) ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.MonoidalCategory.DayFunctor D (Type v))).η F).app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D, y))) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategory.DayFunctor.ν D (Type v))) PUnit.unit, x)) = (CategoryTheory.ConcreteCategory.hom (F.functor.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor y).inv)) x

The Day left unitor, evaluated on a Kan-extension unit element: it strips the canonical unit element and applies the inverse base left unitor.

theorem RS.dayCoyonedaIso_hom_leftUnitor {D : Type v} [CategoryTheory.SmallCategory D] [CategoryTheory.MonoidalCategory D] (a : D) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (dayUnitIso D).hom { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }) (CategoryTheory.CategoryStruct.comp (dayCoyonedaIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) a).hom { natTrans := CategoryTheory.coyoneda.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor a).inv.op }) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor { functor := CategoryTheory.coyoneda.obj (Opposite.op a) }).hom

The Day unit intertwines the left unitor on corepresentables: under the co-Yoneda identifications, the Day left unitor at a corepresentable is precomposition with the inverse base left unitor.

The Yoneda form and the embedded left unitor

theorem RS.dayMkIso_symm_hom_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} (e : A ≅ B) : CategoryTheory.CategoryStruct.comp (dayMkIso e.symm).hom (dayMkIso e).hom = CategoryTheory.CategoryStruct.id { functor := B }

Composing the transports of an isomorphism and of its reverse along RS.dayMkIso, in the reversed order.

theorem RS.dayYonedaIso_hom_leftUnitor {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (x : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp (dayUnitIso Cᵒᵖ).hom (dayMkIso (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).hom) { functor := CategoryTheory.yoneda.obj x }) (CategoryTheory.CategoryStruct.comp (dayYonedaIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) x).hom { natTrans := CategoryTheory.yoneda.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom }) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor { functor := CategoryTheory.yoneda.obj x }).hom

The Day tensor of representables intertwines the left unitor: the Yoneda form of RS.dayCoyonedaIso_hom_leftUnitor. The unit leg is the composite identification of the Day unit with the representable at 𝟙_ C, as in RS.indOfUnitIso.

theorem RS.indToDay_map_indOfUnitIso_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] : indToDay.map indOfUnitIso.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.Monoidal.εIso indToDay).inv (CategoryTheory.CategoryStruct.comp (dayUnitIso Cᵒᵖ).hom (CategoryTheory.CategoryStruct.comp (dayMkIso (CategoryTheory.Coyoneda.objOpOp (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))).hom (indToDayIndOfIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv))

The embedding into the Day presheaf category carries the unit comparison to its Day-level composite.

theorem RS.indOf_leftUnitor_hom {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight indOfUnitIso.hom (indOf.obj X)) (CategoryTheory.CategoryStruct.comp (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).hom (indOf.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))

Left unitality of the embedding comparison: the left unitor of an embedded object factors as the unit comparison, the embedding-tensor comparison, and the embedded left unitor. This is the unit axiom of the monoidal-functor-up-to-isomorphism structure of indOf.

theorem RS.indOf_leftUnitorIso {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) : CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj X) = CategoryTheory.MonoidalCategory.whiskerRightIso indOfUnitIso (indOf.obj X) ≪≫ indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X ≪≫ indOf.mapIso (CategoryTheory.MonoidalCategoryStruct.leftUnitor X)

Iso form of RS.indOf_leftUnitor_hom.

theorem RS.indOf_leftUnitor_inv {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj X)).inv = CategoryTheory.CategoryStruct.comp (indOf.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) (CategoryTheory.CategoryStruct.comp (indOfTensorIso (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight indOfUnitIso.inv (indOf.obj X)))

Inverse form of RS.indOf_leftUnitor_hom.

theorem RS.indOf_map_unitConj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] (X : C) (u : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj X)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp indOfUnitIso.hom (CategoryTheory.CategoryStruct.comp (indOf.map u) indOfUnitIso.inv)) (indOf.obj X)) (CategoryTheory.MonoidalCategoryStruct.leftUnitor (indOf.obj X)).hom) = indOf.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u X) (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))

Transport of unit-endomorphism conjugates: conjugating the indOfUnitIso-transport of a unit endomorphism through the left unitor of an embedded object is the image of the conjugate downstairs.

The scalar transport

theorem RS.indScalarUnit_apply {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 indOfUnitIso.hom (CategoryTheory.CategoryStruct.comp (indOf.map (ψ c)) indOfUnitIso.inv)

The scalar unit of Ind C, evaluated: the indOfUnitIso-conjugate of the embedded unit endomorphism.

theorem RS.indOf_map_smul {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (hψ : ∀ (c : ℂ), ψ c = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (c : ℂ) {X Y : C} (f : X ⟶ Y) : indOf.map (c • f) = scalarSmul (indScalarUnit ψ) c (indOf.map f)

The embedding intertwines the scalar actions: indOf carries c • f to the RS.scalarSmul action of c on the image, for the scalar unit transported by RS.indScalarUnit.

The algebra transport and the summit

theorem RS.permAlg_indOf_conj {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (hψ : ∀ (c : ℂ), ψ c = c • CategoryTheory.CategoryStruct.id (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: under the ℂ-linear structure induced on Ind C by a scalar unit ψ for C, 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_iff {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] (P : SchurPackage) (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (hψ : ∀ (c : ℂ), ψ c = c • CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) {X : C} {μ : YoungDiagram} : SchurKilled P (indOf.obj X) μ ↔ SchurKilled P X μ

Schur-vanishing transport along the embedding C ⥤ Ind C: with the ℂ-linear structure induced on Ind C by a scalar unit for C, a shape kills an embedded object precisely when it kills the object downstairs.

theorem RS.schurKilled_indOf_iff_of_hasScalarUnit {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear ℂ C] [CategoryTheory.Limits.HasFiniteColimits C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear ℂ C] (P : SchurPackage) (hu : HasScalarUnit C) {X : C} {μ : YoungDiagram} : SchurKilled P (indOf.obj X) μ ↔ SchurKilled P X μ

RS.schurKilled_indOf_iff, instantiated at the scalar unit of a category whose unit endomorphisms are exactly the scalars.