Embedded objects are locally mixed

Proposition 2.9 applies to the embedded objects: an object of the small category killed by some Schur functor stays killed after the Ind-embedding, its dual embeds to a dual, and the trichotomy then makes it a mixed sum of the unit and the odd line after base change to some nonzero commutative algebra.

theorem RS.locallyMixed_indOf {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] [CategoryTheory.Abelian C] [CategoryTheory.RigidCategory C] [CategoryTheory.MonoidalPreadditive C] (ψ : ℂ ≃+* CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) (P : SchurPackage) (P₀ : SchurPackage) (Z : C) (lam : YoungDiagram) (hkill : SchurKilled P Z lam) (L : OddLine (CategoryTheory.Ind C)) : ¬CategoryTheory.Limits.IsZero (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) → L.LocallyMixed (indOf.obj Z)

Embedded Schur-killed objects are locally mixed.