Deligne's Proposition 2.1, over a category with an odd line

If every object of a small abelian rigid symmetric monoidal ℂ-linear category with scalar unit endomorphisms is killed by some Schur functor, and its Ind-completion carries an odd line, then there is a nonzero commutative algebra in the Ind-completion whose fibre functor is strong monoidal, exact and faithful.

theorem RS.exists_fibre_functor {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) (L : OddLine (CategoryTheory.Ind C)) (hkill : ∀ (Z : C), ∃ (lam : YoungDiagram), SchurKilled P Z lam) : ∃ (𝔸 : CategoryTheory.Ind C) (x : CategoryTheory.MonObj 𝔸) (x_1 : CategoryTheory.IsCommMonObj 𝔸), CategoryTheory.MonObj.one ≠ 0 ∧ Nonempty (indOf.comp (fibreOver L 𝔸)).Monoidal ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteLimits (indOf.comp (fibreFun L 𝔸))) ∧ Nonempty (CategoryTheory.Limits.PreservesFiniteColimits (indOf.comp (fibreFun L 𝔸))) ∧ (indOf.comp (fibreFun L 𝔸)).Faithful

Deligne's Proposition 2.1 for a category whose Ind-completion carries an odd line.