Zero morphisms and zero objects

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism. (Notice this is extra structure, not merely a property.)

A category "has a zero object" if it has an object which is both initial and terminal. Having a zero object provides zero morphisms, as the unique morphisms factoring through the zero object.

References

• https://en.wikipedia.org/wiki/Zero_morphism
• [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]

class CategoryTheory.Limits.HasZeroMorphisms (C : Type u) [Category.{v, u} C] : Type (max u v)

A category "has zero morphisms" if there is a designated "zero morphism" in each morphism space, and compositions of zero morphisms with anything give the zero morphism.

• zero (X Y : C) : Zero (X ⟶ Y)

  Every morphism space has zero

• comp_zero {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryStruct.comp f 0 = 0

  f composed with 0 is 0

• zero_comp (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryStruct.comp 0 f = 0

  0 composed with f is 0

@[simp]

theorem CategoryTheory.Limits.comp_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} : CategoryStruct.comp f 0 = 0

@[simp]

theorem CategoryTheory.Limits.zero_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : Y ⟶ Z} : CategoryStruct.comp 0 f = 0

@[implicit_reducible]

instance CategoryTheory.Limits.hasZeroMorphismsPEmpty : HasZeroMorphisms (Discrete PEmpty.{u_1 + 1})

@[implicit_reducible]

instance CategoryTheory.Limits.hasZeroMorphismsPUnit : HasZeroMorphisms (Discrete PUnit.{u_1 + 1})

theorem CategoryTheory.Limits.HasZeroMorphisms.ext {C : Type u} [Category.{v, u} C] (I J : HasZeroMorphisms C) : I = J

If you're tempted to use this lemma "in the wild", you should probably carefully consider whether you've made a mistake in allowing two instances of HasZeroMorphisms to exist at all.

See, particularly, the note on zeroMorphismsOfZeroObject below.

instance CategoryTheory.Limits.HasZeroMorphisms.instSubsingleton {C : Type u} [Category.{v, u} C] : Subsingleton (HasZeroMorphisms C)

@[implicit_reducible]

instance CategoryTheory.Limits.hasZeroMorphismsOpposite {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] : HasZeroMorphisms Cᵒᵖ

@[simp]

theorem CategoryTheory.Limits.op_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) : Quiver.Hom.op 0 = 0

@[simp]

theorem CategoryTheory.Limits.unop_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : Cᵒᵖ) : Quiver.Hom.unop 0 = 0

theorem CategoryTheory.Limits.zero_of_comp_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : CategoryStruct.comp f g = 0) : f = 0

theorem CategoryTheory.Limits.zero_of_epi_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : CategoryStruct.comp f g = 0) : g = 0

theorem CategoryTheory.Limits.eq_zero_of_image_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasImage f] (w : image.ι f = 0) : f = 0

theorem CategoryTheory.Limits.nonzero_image_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasImage f] (w : f ≠ 0) : image.ι f ≠ 0

@[implicit_reducible]

instance CategoryTheory.Limits.instHasZeroMorphismsFunctor {C : Type u} [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [HasZeroMorphisms D] : HasZeroMorphisms (Functor C D)

@[simp]

theorem CategoryTheory.Limits.zero_app {C : Type u} [Category.{v, u} C] (D : Type u') [Category.{v', u'} D] [HasZeroMorphisms D] (F G : Functor C D) (j : C) : NatTrans.app 0 j = 0

theorem CategoryTheory.Limits.IsZero.eq_zero_of_src {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (o : IsZero X) (f : X ⟶ Y) : f = 0

theorem CategoryTheory.Limits.IsZero.eq_zero_of_tgt {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (o : IsZero Y) (f : X ⟶ Y) : f = 0

theorem CategoryTheory.Limits.IsZero.iff_id_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X : C) : IsZero X ↔ CategoryStruct.id X = 0

theorem CategoryTheory.Limits.IsZero.of_mono_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [Mono 0] : IsZero X

theorem CategoryTheory.Limits.IsZero.of_epi_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [Epi 0] : IsZero Y

theorem CategoryTheory.Limits.IsZero.of_mono_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) : IsZero X

theorem CategoryTheory.Limits.IsZero.of_epi_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Epi f] (h : f = 0) : IsZero Y

theorem CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsZero X ↔ f = 0

theorem CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZero Y ↔ f = 0

theorem CategoryTheory.Limits.IsZero.of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Mono f] (i : IsZero Y) : IsZero X

theorem CategoryTheory.Limits.IsZero.of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Epi f] (i : IsZero X) : IsZero Y

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.IsZero.hasZeroMorphisms {C : Type u} [Category.{v, u} C] {O : C} (hO : IsZero O) : HasZeroMorphisms C

A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zeroMorphismsOfZeroObject will then be incompatible with these categories because the HasZeroMorphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObject.

@[implicit_reducible]

noncomputable def CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject {C : Type u} [Category.{v, u} C] [HasZeroObject C] : HasZeroMorphisms C

A category with a zero object has zero morphisms.

It is rarely a good idea to use this. Many categories that have a zero object have zero morphisms for some other reason, for example from additivity. Library code that uses zeroMorphismsOfZeroObject will then be incompatible with these categories because the HasZeroMorphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of HasZeroMorphisms separately, even if it already asks for an instance of HasZeroObject.

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).hom = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).inv = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).hom = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).inv = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasInitial C] : zeroIsoInitial.hom = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasInitial C] : zeroIsoInitial.inv = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasTerminal C] : zeroIsoTerminal.hom = 0

@[simp]

theorem CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] [HasTerminal C] : zeroIsoTerminal.inv = 0

instance CategoryTheory.Limits.HasZeroObject.instFunctor {C : Type u} [Category.{v, u} C] [HasZeroObject C] {B : Type u_1} [Category.{v_1, u_1} B] : HasZeroObject (Functor B C)

@[simp]

theorem CategoryTheory.Limits.IsZero.map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroObject D] [HasZeroMorphisms D] {F : Functor C D} (hF : IsZero F) {X Y : C} (f : X ⟶ Y) : F.map f = 0

@[simp]

theorem CategoryTheory.Functor.zero_obj {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroObject D] (X : C) : Limits.IsZero (obj 0 X)

@[simp]

theorem CategoryTheory.zero_map {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroObject D] [Limits.HasZeroMorphisms D] {X Y : C} (f : X ⟶ Y) : Functor.map 0 f = 0

@[simp]

theorem CategoryTheory.Limits.id_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] : CategoryStruct.id 0 = 0

theorem CategoryTheory.Limits.zero_of_to_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (f : X ⟶ 0) : f = 0

An arrow ending in the zero object is zero

theorem CategoryTheory.Limits.zero_of_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : f = 0

theorem CategoryTheory.Limits.zero_of_from_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (f : 0 ⟶ X) : f = 0

An arrow starting at the zero object is zero

theorem CategoryTheory.Limits.zero_of_source_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0

theorem CategoryTheory.Limits.zero_of_source_iso_zero' {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic X 0) : f = 0

theorem CategoryTheory.Limits.zero_of_target_iso_zero' {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic Y 0) : f = 0

theorem CategoryTheory.Limits.mono_of_source_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : Mono f

theorem CategoryTheory.Limits.epi_of_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : Epi f

noncomputable def CategoryTheory.Limits.idZeroEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) : CategoryStruct.id X = 0 ≃ (X ≅ 0)

An object X has 𝟙 X = 0 if and only if it is isomorphic to the zero object.

Because X ≅ 0 contains data (even if a subsingleton), we express this ↔ as an ≃.

@[simp]

theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) (h : CategoryStruct.id X = 0) : ((idZeroEquivIsoZero X) h).hom = 0

@[simp]

theorem CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] (X : C) (h : CategoryStruct.id X = 0) : ((idZeroEquivIsoZero X) h).inv = 0

noncomputable def CategoryTheory.Limits.isoZeroOfMonoZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} : Mono 0 → (X ≅ 0)

If 0 : X ⟶ Y is a monomorphism, then X ≅ 0.

@[simp]

theorem CategoryTheory.Limits.isoZeroOfMonoZero_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Mono 0) : (isoZeroOfMonoZero x✝).inv = 0

@[simp]

theorem CategoryTheory.Limits.isoZeroOfMonoZero_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Mono 0) : (isoZeroOfMonoZero x✝).hom = 0

noncomputable def CategoryTheory.Limits.isoZeroOfEpiZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} : Epi 0 → (Y ≅ 0)

If 0 : X ⟶ Y is an epimorphism, then Y ≅ 0.

@[simp]

theorem CategoryTheory.Limits.isoZeroOfEpiZero_inv {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Epi 0) : (isoZeroOfEpiZero x✝).inv = 0

@[simp]

theorem CategoryTheory.Limits.isoZeroOfEpiZero_hom {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} (x✝ : Epi 0) : (isoZeroOfEpiZero x✝).hom = 0

noncomputable def CategoryTheory.Limits.isoZeroOfMonoEqZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Mono f] (h : f = 0) : X ≅ 0

If a monomorphism out of X is zero, then X ≅ 0.

noncomputable def CategoryTheory.Limits.isoZeroOfEpiEqZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [Epi f] (h : f = 0) : Y ≅ 0

If an epimorphism in to Y is zero, then Y ≅ 0.

noncomputable def CategoryTheory.Limits.isoOfIsIsomorphicZero {C : Type u} [Category.{v, u} C] [HasZeroObject C] [HasZeroMorphisms C] {X : C} (P : IsIsomorphic X 0) : X ≅ 0

If an object X is isomorphic to 0, there's no need to use choice to construct an explicit isomorphism: the zero morphism suffices.

def CategoryTheory.Limits.isIsoZeroEquiv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) : IsIso 0 ≃ CategoryStruct.id X = 0 ∧ CategoryStruct.id Y = 0

A zero morphism 0 : X ⟶ Y is an isomorphism if and only if the identities on both X and Y are zero.

def CategoryTheory.Limits.isIsoZeroSelfEquiv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X : C) : IsIso 0 ≃ CategoryStruct.id X = 0

A zero morphism 0 : X ⟶ X is an isomorphism if and only if the identity on X is zero.

noncomputable def CategoryTheory.Limits.isIsoZeroEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)

A zero morphism 0 : X ⟶ Y is an isomorphism if and only if X and Y are isomorphic to the zero object.

theorem CategoryTheory.Limits.isIsoZero_iff_source_target_isZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : IsIso 0 ↔ IsZero X ∧ IsZero Y

A zero morphism 0 : X ⟶ Y is an isomorphism if and only if X and Y are zero objects.

theorem CategoryTheory.Limits.isIso_of_source_target_iso_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) : IsIso f

noncomputable def CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X : C) : IsIso 0 ≃ (X ≅ 0)

A zero morphism 0 : X ⟶ X is an isomorphism if and only if X is isomorphic to the zero object.

theorem CategoryTheory.Limits.hasZeroObject_of_hasInitial_object {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasInitial C] : HasZeroObject C

If there are zero morphisms, any initial object is a zero object.

theorem CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasTerminal C] : HasZeroObject C

If there are zero morphisms, any terminal object is a zero object.

theorem CategoryTheory.Limits.image_ι_comp_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f] [Epi (factorThruImage f)] (h : CategoryStruct.comp f g = 0) : CategoryStruct.comp (image.ι f) g = 0

theorem CategoryTheory.Limits.comp_factorThruImage_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage g] (h : CategoryStruct.comp f g = 0) : CategoryStruct.comp f (factorThruImage g) = 0

noncomputable def CategoryTheory.Limits.monoFactorisationZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : MonoFactorisation 0

The zero morphism has a MonoFactorisation through the zero object.

@[simp]

theorem CategoryTheory.Limits.monoFactorisationZero_m {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : (monoFactorisationZero X Y).m = 0

@[simp]

theorem CategoryTheory.Limits.monoFactorisationZero_e {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : (monoFactorisationZero X Y).e = 0

@[simp]

theorem CategoryTheory.Limits.monoFactorisationZero_I {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : (monoFactorisationZero X Y).I = 0

noncomputable def CategoryTheory.Limits.imageFactorisationZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] (X Y : C) : ImageFactorisation 0

The factorisation through the zero object is an image factorisation.

instance CategoryTheory.Limits.hasImage_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} : HasImage 0

noncomputable def CategoryTheory.Limits.imageZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} : image 0 ≅ 0

The image of a zero morphism is the zero object.

noncomputable def CategoryTheory.Limits.imageZero' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] : image f ≅ 0

The image of a morphism which is equal to zero is the zero object.

@[simp]

theorem CategoryTheory.Limits.image.ι_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} [HasImage 0] : ι 0 = 0

@[simp]

theorem CategoryTheory.Limits.image.ι_zero' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] [HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] : ι f = 0

If we know f = 0, it requires a little work to conclude image.ι f = 0, because f = g only implies image f ≅ image g.

instance CategoryTheory.Limits.isSplitMono_sigma_ι {C : Type u} [Category.{v, u} C] {β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasColimit (Discrete.functor f)] (b : β) : IsSplitMono (Sigma.ι f b)

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

instance CategoryTheory.Limits.isSplitEpi_pi_π {C : Type u} [Category.{v, u} C] {β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasLimit (Discrete.functor f)] (b : β) : IsSplitEpi (Pi.π f b)

In the presence of zero morphisms, projections into a product are (split) epimorphisms.

instance CategoryTheory.Limits.isSplitMono_coprod_inl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] : IsSplitMono coprod.inl

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

instance CategoryTheory.Limits.isSplitMono_coprod_inr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] : IsSplitMono coprod.inr

In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.

instance CategoryTheory.Limits.isSplitEpi_prod_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] : IsSplitEpi prod.fst

In the presence of zero morphisms, projections into a product are (split) epimorphisms.

instance CategoryTheory.Limits.isSplitEpi_prod_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] : IsSplitEpi prod.snd

In the presence of zero morphisms, projections into a product are (split) epimorphisms.

def CategoryTheory.Limits.IsLimit.ofIsZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} (c : Cone F) (hF : IsZero F) (hc : IsZero c.pt) : IsLimit c

If a functor F is zero, then any cone for F with a zero point is limit.

def CategoryTheory.Limits.IsColimit.ofIsZero {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} (c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) : IsColimit c

If a functor F is zero, then any cocone for F with a zero point is colimit.

theorem CategoryTheory.Limits.IsLimit.isZero_pt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} {c : Cone F} (hc : IsLimit c) (hF : IsZero F) : IsZero c.pt

theorem CategoryTheory.Limits.IsColimit.isZero_pt {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [HasZeroMorphisms C] [HasZeroObject C] {F : Functor D C} {c : Cocone F} (hc : IsColimit c) (hF : IsZero F) : IsZero c.pt

@[reducible]

def CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroMorphisms C] {F : Functor D C} (hF : F.FullyFaithful) : Limits.HasZeroMorphisms D

Given a functor F : D ⥤ C, zero morphisms on C induce zero morphisms on D by taking preimages.

theorem CategoryTheory.Functor.FullyFaithful.hasZeroMorphisms_def {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Limits.HasZeroMorphisms C] {F : Functor D C} (hF : F.FullyFaithful) (X Y : D) : 0 = hF.preimage 0

theorem CategoryTheory.Limits.IsTerminal.isZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X : C} (hX : IsTerminal X) : IsZero X

theorem CategoryTheory.Limits.IsInitial.isZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X : C} (hX : IsInitial X) : IsZero X

noncomputable def CategoryTheory.Limits.Pi.ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b : β) : f b ⟶ ∏ᶜ f

In the presence of 0-morphism we can define an inclusion morphism into any product.

@[simp]

theorem CategoryTheory.Limits.Pi.ι_π_eq_id {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b : β) : CategoryStruct.comp (ι f b) (π f b) = CategoryStruct.id (f b)

@[simp]

theorem CategoryTheory.Limits.Pi.ι_π_eq_id_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b : β) {Z : C} (h : f b ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f b) h) = h

theorem CategoryTheory.Limits.Pi.ι_π_of_ne {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] {b c : β} (h : b ≠ c) : CategoryStruct.comp (ι f b) (π f c) = 0

theorem CategoryTheory.Limits.Pi.ι_π_of_ne_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] {b c : β} (h : b ≠ c) {Z : C} (h✝ : f c ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f c) h✝) = CategoryStruct.comp 0 h✝

theorem CategoryTheory.Limits.Pi.ι_π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b c : β) : CategoryStruct.comp (ι f b) (π f c) = if h : b = c then eqToHom ⋯ else 0

theorem CategoryTheory.Limits.Pi.ι_π_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f c) h) = CategoryStruct.comp (if h : b = c then eqToHom ⋯ else 0) h

instance CategoryTheory.Limits.instMonoι_1 {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasProduct f] (b : β) : Mono (Pi.ι f b)

noncomputable def CategoryTheory.Limits.Sigma.π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b : β) : ∐ f ⟶ f b

In the presence of 0-morphisms we can define a projection morphism from any coproduct.

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_π_eq_id {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b : β) : CategoryStruct.comp (ι f b) (π f b) = CategoryStruct.id (f b)

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_π_eq_id_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b : β) {Z : C} (h : f b ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f b) h) = h

theorem CategoryTheory.Limits.Sigma.ι_π_of_ne {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] {b c : β} (h : b ≠ c) : CategoryStruct.comp (ι f b) (π f c) = 0

theorem CategoryTheory.Limits.Sigma.ι_π_of_ne_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] {b c : β} (h : b ≠ c) {Z : C} (h✝ : f c ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f c) h✝) = CategoryStruct.comp 0 h✝

theorem CategoryTheory.Limits.Sigma.ι_π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b c : β) : CategoryStruct.comp (ι f b) (π f c) = if h : b = c then eqToHom ⋯ else 0

theorem CategoryTheory.Limits.Sigma.ι_π_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b c : β) {Z : C} (h : f c ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (π f c) h) = CategoryStruct.comp (if h : b = c then eqToHom ⋯ else 0) h

instance CategoryTheory.Limits.instEpiπ {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {β : Type w} [DecidableEq β] (f : β → C) [HasCoproduct f] (b : β) : Epi (Sigma.π f b)

noncomputable def CategoryTheory.Limits.prod.inl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : X ⟶ X ⨯ Y

If a category C has 0-morphisms, there is a canonical inclusion from the first component X into any product of objects X ⨯ Y.

noncomputable def CategoryTheory.Limits.prod.inr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : Y ⟶ X ⨯ Y

If a category C has 0-morphisms, there is a canonical inclusion from the second component Y into any product of objects X ⨯ Y.

@[simp]

theorem CategoryTheory.Limits.prod.inl_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (inl X Y) fst = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.prod.inl_fst_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (inl X Y) (CategoryStruct.comp fst h) = h

@[simp]

theorem CategoryTheory.Limits.prod.inl_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (inl X Y) snd = 0

@[simp]

theorem CategoryTheory.Limits.prod.inl_snd_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (inl X Y) (CategoryStruct.comp snd h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Limits.prod.inr_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (inr X Y) fst = 0

@[simp]

theorem CategoryTheory.Limits.prod.inr_fst_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (inr X Y) (CategoryStruct.comp fst h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Limits.prod.inr_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : CategoryStruct.comp (inr X Y) snd = CategoryStruct.id Y

@[simp]

theorem CategoryTheory.Limits.prod.inr_snd_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (inr X Y) (CategoryStruct.comp snd h) = h

instance CategoryTheory.Limits.instMonoInl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : Mono (prod.inl X Y)

instance CategoryTheory.Limits.instMonoInr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryProduct X Y] : Mono (prod.inr X Y)

noncomputable def CategoryTheory.Limits.coprod.fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : X ⨿ Y ⟶ X

If a category C has 0-morphisms, there is a canonical projection from a coproduct X ⨿ Y to its first component X.

noncomputable def CategoryTheory.Limits.coprod.snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : X ⨿ Y ⟶ Y

If a category C has 0-morphisms, there is a canonical projection from a coproduct X ⨿ Y to its second component Y.

@[simp]

theorem CategoryTheory.Limits.coprod.inl_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp inl (fst X Y) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.coprod.inl_fst_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp (fst X Y) h) = h

@[simp]

theorem CategoryTheory.Limits.coprod.inr_fst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp inr (fst X Y) = 0

@[simp]

theorem CategoryTheory.Limits.coprod.inr_fst_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp (fst X Y) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Limits.coprod.inl_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp inl (snd X Y) = 0

@[simp]

theorem CategoryTheory.Limits.coprod.inl_snd_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp inl (CategoryStruct.comp (snd X Y) h) = CategoryStruct.comp 0 h

@[simp]

theorem CategoryTheory.Limits.coprod.inr_snd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : CategoryStruct.comp inr (snd X Y) = CategoryStruct.id Y

@[simp]

theorem CategoryTheory.Limits.coprod.inr_snd_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp inr (CategoryStruct.comp (snd X Y) h) = h

instance CategoryTheory.Limits.instEpiFst {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : Epi (coprod.fst X Y)

instance CategoryTheory.Limits.instEpiSnd {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) [HasBinaryCoproduct X Y] : Epi (coprod.snd X Y)

@[implicit_reducible]

instance CategoryTheory.ObjectProperty.instHasZeroMorphismsFullSubcategory {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [Limits.HasZeroMorphisms C] : Limits.HasZeroMorphisms P.FullSubcategory

@[simp]

theorem CategoryTheory.ObjectProperty.homMk_zero {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (X Y : P.FullSubcategory) : homMk 0 = 0

@[simp]

theorem CategoryTheory.ObjectProperty.zero_hom {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasZeroMorphisms C] (P : ObjectProperty C) (X Y : P.FullSubcategory) : InducedCategory.Hom.hom 0 = 0