theorem
CategoryTheory.isZero_of_isZero_rightDual
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Preadditive C]
[MonoidalPreadditive C]
{X : C}
[HasRightDual X]
(h : Limits.IsZero Xᘁ)
:
In a preadditive monoidal category, an object whose right dual is zero is itself zero.
theorem
CategoryTheory.isZero_rightDual_of_isZero
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Preadditive C]
[MonoidalPreadditive C]
{X : C}
[HasRightDual X]
(h : Limits.IsZero X)
:
In a preadditive monoidal category, the right dual of a zero object is zero.
theorem
CategoryTheory.isZero_of_isZero_leftDual
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Preadditive C]
[MonoidalPreadditive C]
{X : C}
[HasLeftDual X]
(h : Limits.IsZero ᘁX)
:
In a preadditive monoidal category, an object whose left dual is zero is itself zero.
theorem
CategoryTheory.isZero_leftDual_of_isZero
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
[Preadditive C]
[MonoidalPreadditive C]
{X : C}
[HasLeftDual X]
(h : Limits.IsZero X)
:
In a preadditive monoidal category, the left dual of a zero object is zero.