mathlib documentation

category_theory.limits.shapes.zero_morphisms

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 of this typeclass
Instances of other typeclasses for category_theory.limits.has_zero_morphisms
@[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]
@[protected, instance]
Equations
@[protected, 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.

theorem category_theory.limits.zero_of_comp_mono {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z : C} {f : X Y} (g : Y Z) [category_theory.mono g] (h : f g = 0) :
f = 0
theorem category_theory.limits.zero_of_epi_comp {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z : C} (f : X Y) {g : Y Z} [category_theory.epi f] (h : f g = 0) :
g = 0
@[simp]

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

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

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

Equations

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

Equations

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

Equations

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

Equations

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

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

The zero morphism has a mono_factorisation through 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.

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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

@[protected, instance]

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