Properties of objects which hold for a zero object #
Given a category C and P : ObjectProperty C, we define a type class P.ContainsZero
expressing that there exists a zero object for which P holds. (We do not require
that P holds for all zero objects, as in some applications (e.g. triangulated categories),
P may not necessarily be closed under isomorphisms.)
class
CategoryTheory.ObjectProperty.ContainsZero
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
:
Given P : ObjectProperty C, we say that P.ContainsZero if there exists
a zero object for which P holds. When P is closed under isomorphisms,
this holds for any zero object.
- exists_zero : ∃ (Z : C), Limits.IsZero Z ∧ P Z
Instances
theorem
CategoryTheory.ObjectProperty.exists_prop_of_containsZero
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.ContainsZero]
:
∃ (Z : C), Limits.IsZero Z ∧ P Z
theorem
CategoryTheory.ObjectProperty.prop_of_isZero
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.ContainsZero]
[P.IsClosedUnderIsomorphisms]
{Z : C}
(hZ : Limits.IsZero Z)
:
P Z
theorem
CategoryTheory.ObjectProperty.prop_zero
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.ContainsZero]
[P.IsClosedUnderIsomorphisms]
[Limits.HasZeroObject C]
:
P 0
instance
CategoryTheory.ObjectProperty.instContainsZeroTopOfHasZeroObject
{C : Type u}
[Category.{v, u} C]
[Limits.HasZeroObject C]
:
instance
CategoryTheory.ObjectProperty.instContainsZeroMapOfPreservesZeroMorphisms
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(P : ObjectProperty C)
[P.ContainsZero]
[Limits.HasZeroMorphisms C]
[Limits.HasZeroMorphisms D]
(F : Functor C D)
[F.PreservesZeroMorphisms]
:
(P.map F).ContainsZero
instance
CategoryTheory.ObjectProperty.instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject
{C : Type u}
[Category.{v, u} C]
{D : Type u'}
[Category.{v', u'} D]
(P : ObjectProperty C)
[P.ContainsZero]
[P.IsClosedUnderIsomorphisms]
[Limits.HasZeroMorphisms C]
[Limits.HasZeroMorphisms D]
(F : Functor D C)
[F.PreservesZeroMorphisms]
[Limits.HasZeroObject D]
:
(P.inverseImage F).ContainsZero