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) : Prop

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

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

@[instance 100]

instance CategoryTheory.ObjectProperty.instNonemptyOfContainsZero {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.ContainsZero] : P.Nonempty

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] : ⊤.ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroIsZeroOfHasZeroObject {C : Type u} [Category.{v, u} C] [Limits.HasZeroObject C] : ContainsZero Limits.IsZero

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

instance CategoryTheory.ObjectProperty.instContainsZeroIsoClosure {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.ContainsZero] : P.isoClosure.ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroMinOfIsClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms] [Q.ContainsZero] : (P ⊓ Q).ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroOppositeOp {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.ContainsZero] : P.op.ContainsZero

instance CategoryTheory.ObjectProperty.instContainsZeroUnopOfOpposite {C : Type u} [Category.{v, u} C] (P : ObjectProperty Cᵒᵖ) [P.ContainsZero] : P.unop.ContainsZero

instance CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) [P.ContainsZero] : Limits.HasZeroObject P.FullSubcategory

instance CategoryTheory.ObjectProperty.instContainsZeroMinOfIsClosedUnderIsomorphisms_1 {C : Type u} [Category.{v, u} C] (P Q : ObjectProperty C) [P.ContainsZero] [Q.ContainsZero] [Q.IsClosedUnderIsomorphisms] : (P ⊓ Q).ContainsZero

@[reducible, inline]

abbrev CategoryTheory.Functor.kernel {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] (F : Functor C D) : ObjectProperty C

Given a functor F : C ⥤ D, this is the property of objects of C satisfied by those X : C such that IsZero (F.obj X).

Equations

• F.kernel = CategoryTheory.ObjectProperty.inverseImage CategoryTheory.Limits.IsZero F