mathlib documentation

category_theory.limits.shapes.zero

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

@[class]
structure category_theory.limits.has_zero_morphisms (C : Type u) [category_theory.category C] :
Type (max u v)
  • has_zero : Π (X Y : C), has_zero (X Y)
  • comp_zero' : (∀ {X Y : C} (f : X Y) (Z : C), f 0 = 0) . "obviously"
  • zero_comp' : (∀ (X : C) {Y Z : C} (f : Y Z), 0 f = 0) . "obviously"

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.

Instances
@[simp]
theorem category_theory.limits.comp_zero {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} {f : X Y} {Z : C} :
f 0 = 0

@[simp]

@[instance]

Equations
@[instance]

Equations

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 has_zero_morphisms to exist at all.

See, particularly, the note on zero_morphisms_of_zero_object below.

@[instance]

Equations

Construct a has_zero C for a category with a zero object. This can not be a global instance as it will trigger for every has_zero C typeclass search.

Equations

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 zero_morphisms_of_zero_object will then be incompatible with these categories because the has_zero_morphisms instances will not be definitionally equal. For this reason library code should generally ask for an instance of has_zero_morphisms separately, even if it already asks for an instance of has_zero_objects.

Equations

An arrow ending in the zero object is zero

An arrow starting at the zero object is zero

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 .

Equations

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

Equations

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

Equations

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

Equations
@[simp]

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]

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

Equations
@[instance]

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

Equations