The unit of the Ind-completion is nonzero #
A scalar unit downstairs makes the identity of the tensor unit nonzero, and the embedding is faithful, so the tensor unit of the Ind-completion is not a zero object. This is the side condition of both Proposition 2.9 and Rappel 2.10 over the Ind-completion.
theorem
RS.not_isZero_unit_ind
{C : Type v}
[CategoryTheory.SmallCategory C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.Abelian C]
[CategoryTheory.Linear ℂ C]
(hu : HasScalarUnit C)
:
The tensor unit of the Ind-completion is not a zero object.