The unit of a big tensor product of ind-algebras survives

In the ind-completion the two inputs of the general criterion are available: the tensor of two nonzero points is nonzero, and a point of a filtered colimit vanishes only if it already vanishes at a later stage. So a tensor product of an arbitrary family of algebras with nonvanishing units again has a nonvanishing unit — the step Deligne asserts without proof in 2.11.

theorem RS.id_indUnit_ne_zero {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] (hu : HasScalarUnit C) : CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Ind C)) ≠ 0

The identity of the unit of the ind-completion is nonzero.

theorem RS.bigTensorUnit_ne_zero_ind {C : Type v} [CategoryTheory.SmallCategory C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] [CategoryTheory.Linear ℂ C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.RigidCategory C] [CategoryTheory.BraidedCategory (CategoryTheory.Ind C)] {ι : Type v} [LinearOrder ι] (B : ι → CategoryTheory.Ind C) [(i : ι) → CategoryTheory.MonObj (B i)] (hu : HasScalarUnit C) (hB : ∀ (i : ι), CategoryTheory.MonObj.one ≠ 0) : bigTensorUnit B ≠ 0

The unit of a big tensor product of ind-algebras survives.