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]
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
- category_theory.preadditive.preadditive_has_zero_morphisms
- category_theory.non_preadditive_abelian.has_zero_morphisms
- category_theory.limits.has_zero_morphisms_pempty
- category_theory.limits.has_zero_morphisms_punit
- category_theory.graded_object.has_zero_morphisms
- category_theory.differential_object.has_zero_morphisms
@[instance]
Equations
- category_theory.limits.has_zero_morphisms_pempty = {has_zero := λ (X Y : category_theory.discrete pempty), pempty.cases_on (λ (Y : category_theory.discrete pempty), has_zero (X ⟶ Y)) Y, comp_zero' := category_theory.limits.has_zero_morphisms_pempty._proof_1, zero_comp' := category_theory.limits.has_zero_morphisms_pempty._proof_2}
@[instance]
Equations
- category_theory.limits.has_zero_morphisms_punit = {has_zero := λ (X Y : category_theory.discrete punit), punit.cases_on Y (punit.cases_on X {zero := {down := category_theory.limits.has_zero_morphisms_punit._proof_1.mpr {down := _}}}), comp_zero' := category_theory.limits.has_zero_morphisms_punit._proof_2, zero_comp' := category_theory.limits.has_zero_morphisms_punit._proof_3}
theorem
category_theory.limits.has_zero_morphisms.ext
{C : Type u}
[category_theory.category C]
(I J : category_theory.limits.has_zero_morphisms 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 has_zero_morphisms to exist at all.
See, particularly, the note on zero_morphisms_of_zero_object below.
@[instance]
def
category_theory.limits.has_zero_morphisms.subsingleton
{C : Type u}
[category_theory.category C] :
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] :
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] :
theorem
category_theory.limits.eq_zero_of_image_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_image f] :
category_theory.limits.image.ι f = 0 → f = 0
theorem
category_theory.limits.nonzero_image_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_image f] :
f ≠ 0 → category_theory.limits.image.ι f ≠ 0
theorem
category_theory.limits.equivalence_preserves_zero_morphisms
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ≌ D)
(X Y : C) :
@[simp]
theorem
category_theory.limits.is_equivalence_preserves_zero_morphisms
(C : Type u)
[category_theory.category C]
(D : Type u')
[category_theory.category D]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.is_equivalence F]
(X Y : C) :
@[class]
structure
category_theory.limits.has_zero_object
(C : Type u)
[category_theory.category C] :
Type (max u v)
- zero : C
- unique_to : Π (X : C), unique (category_theory.limits.has_zero_object.zero ⟶ X)
- unique_from : Π (X : C), unique (X ⟶ category_theory.limits.has_zero_object.zero)
A category "has a zero object" if it has an object which is both initial and terminal.
Instances
- category_theory.limits.has_zero_object_of_has_initial_object
- category_theory.limits.has_zero_object_of_has_terminal_object
- category_theory.non_preadditive_abelian.has_zero_object
- category_theory.limits.has_zero_object_punit
- Module.category_theory.limits.has_zero_object
- Group.category_theory.limits.has_zero_object
- AddGroup.has_zero_object
- CommGroup.category_theory.limits.has_zero_object
- AddCommGroup.has_zero_object
- category_theory.graded_object.has_zero_object
- category_theory.differential_object.has_zero_object
@[instance]
Equations
- category_theory.limits.has_zero_object_punit = {zero := punit.star, unique_to := λ (X : category_theory.discrete punit), punit.cases_on X {to_inhabited := category_theory.limits.has_zero_object_punit._aux_1, uniq := category_theory.limits.has_zero_object_punit._proof_1}, unique_from := λ (X : category_theory.discrete punit), punit.cases_on X {to_inhabited := category_theory.limits.has_zero_object_punit._aux_2, uniq := category_theory.limits.has_zero_object_punit._proof_2}}
def
category_theory.limits.has_zero_object.has_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C] :
has_zero C
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
@[ext]
theorem
category_theory.limits.has_zero_object.to_zero_ext
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{X : C}
(f g : X ⟶ 0) :
f = g
@[ext]
theorem
category_theory.limits.has_zero_object.from_zero_ext
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{X : C}
(f g : 0 ⟶ X) :
f = g
@[instance]
def
category_theory.limits.has_zero_object.subsingleton
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
(X : C) :
subsingleton (X ≅ 0)
Equations
- _ = _
@[instance]
def
category_theory.limits.has_zero_object.category_theory.mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{X : C}
(f : 0 ⟶ X) :
Equations
- _ = _
@[instance]
def
category_theory.limits.has_zero_object.category_theory.epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
{X : C}
(f : X ⟶ 0) :
Equations
- _ = _
def
category_theory.limits.has_zero_object.zero_morphisms_of_zero_object
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object 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
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
- category_theory.limits.has_zero_object.zero_morphisms_of_zero_object = {has_zero := λ (X Y : C), {zero := inhabited.default (X ⟶ 0) ≫ inhabited.default (0 ⟶ Y)}, comp_zero' := _, zero_comp' := _}
def
category_theory.limits.has_zero_object.has_initial
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C] :
A zero object is in particular initial.
def
category_theory.limits.has_zero_object.has_terminal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C] :
A zero object is in particular terminal.
@[simp]
theorem
category_theory.limits.id_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C] :
theorem
category_theory.limits.zero_of_to_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(f : X ⟶ 0) :
f = 0
An arrow ending in the zero object is zero
theorem
category_theory.limits.zero_of_target_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.limits.zero_of_from_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(f : 0 ⟶ X) :
f = 0
An arrow starting at the zero object is zero
theorem
category_theory.limits.zero_of_source_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y) :
theorem
category_theory.limits.mono_of_source_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y) :
(X ≅ 0) → category_theory.mono f
theorem
category_theory.limits.epi_of_target_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y) :
(Y ≅ 0) → category_theory.epi f
def
category_theory.limits.id_zero_equiv_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
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
- category_theory.limits.id_zero_equiv_iso_zero X = {to_fun := λ (h : 𝟙 X = 0), {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}, inv_fun := _, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.limits.id_zero_equiv_iso_zero_apply_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C)
(h : 𝟙 X = 0) :
@[simp]
theorem
category_theory.limits.id_zero_equiv_iso_zero_apply_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
(X : C)
(h : 𝟙 X = 0) :
def
category_theory.limits.is_iso_zero_equiv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C) :
A zero morphism 0 : X ⟶ Y is an isomorphism if and only if
the identities on both X and Y are zero.
@[simp]
theorem
category_theory.limits.is_iso_zero_equiv_inv_fun_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
(h : 𝟙 X = 0 ∧ 𝟙 Y = 0) :
def
category_theory.limits.is_iso_zero_self_equiv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.is_iso 0 ≃ 𝟙 X = 0
A zero morphism 0 : X ⟶ X is an isomorphism if and only if
the identity on X is zero.
Equations
def
category_theory.limits.is_iso_zero_equiv_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
category_theory.is_iso 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.
Equations
- category_theory.limits.is_iso_zero_equiv_iso_zero X Y = (category_theory.limits.is_iso_zero_equiv X Y).trans {to_fun := _, inv_fun := λ (a : 𝟙 X = 0 ∧ 𝟙 Y = 0), a.dcases_on (λ (hX : 𝟙 X = 0) (hY : 𝟙 Y = 0), (⇑(category_theory.limits.id_zero_equiv_iso_zero X) hX, ⇑(category_theory.limits.id_zero_equiv_iso_zero Y) hY)), left_inv := _, right_inv := _}.symm
def
category_theory.limits.is_iso_zero_self_equiv_iso_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X : C) :
category_theory.is_iso 0 ≃ (X ≅ 0)
A zero morphism 0 : X ⟶ X is an isomorphism if and only if
X is isomorphic to the zero object.
@[instance]
def
category_theory.limits.has_zero_object_of_has_initial_object
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_initial C] :
If there are zero morphisms, any initial object is a zero object.
Equations
- category_theory.limits.has_zero_object_of_has_initial_object = {zero := ⊥_C, unique_to := λ (X : C), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : C), {to_inhabited := {default := 0}, uniq := _}}
@[instance]
def
category_theory.limits.has_zero_object_of_has_terminal_object
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_terminal C] :
If there are zero morphisms, any terminal object is a zero object.
Equations
- category_theory.limits.has_zero_object_of_has_terminal_object = {zero := ⊤_C, unique_to := λ (X : C), {to_inhabited := {default := 0}, uniq := _}, unique_from := λ (X : C), {to_inhabited := {default := 0}, uniq := _}}
theorem
category_theory.limits.image_ι_comp_eq_zero
{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.limits.has_image f]
[category_theory.epi (category_theory.limits.factor_thru_image f)] :
f ≫ g = 0 → category_theory.limits.image.ι f ≫ g = 0
def
category_theory.limits.mono_factorisation_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
The zero morphism has a mono_factorisation through the zero object.
@[simp]
theorem
category_theory.limits.mono_factorisation_zero_e
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
@[simp]
theorem
category_theory.limits.mono_factorisation_zero_m
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
@[simp]
theorem
category_theory.limits.mono_factorisation_zero_I
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
def
category_theory.limits.has_image.zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
Any zero morphism has an image. We don't set this as an instance, as it is only intended for use inside the following proofs.
Equations
- category_theory.limits.has_image.zero X Y = {F := category_theory.limits.mono_factorisation_zero X Y, is_image := {lift := λ (F' : category_theory.limits.mono_factorisation 0), 0, lift_fac' := _}}
def
category_theory.limits.image_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
{X Y : C}
[category_theory.limits.has_image 0] :
The image of a zero morphism is the zero object.
def
category_theory.limits.image_zero'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
{X Y : C}
{f : X ⟶ Y}
(h : f = 0)
[category_theory.limits.has_image f] :
The image of a morphism which is equal to zero is the zero object.
@[simp]
theorem
category_theory.limits.image.ι_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
{X Y : C}
[category_theory.limits.has_image 0] :
@[simp]
theorem
category_theory.limits.image.ι_zero'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
{X Y : C}
{f : X ⟶ Y}
(h : f = 0)
[category_theory.limits.has_image f] :
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]
def
category_theory.limits.split_mono_sigma_ι
{C : Type u}
[category_theory.category C]
{β : Type v}
[decidable_eq β]
[category_theory.limits.has_zero_morphisms C]
(f : β → C)
[category_theory.limits.has_colimit (category_theory.discrete.functor f)]
(b : β) :
In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.
Equations
- category_theory.limits.split_mono_sigma_ι f b = {retraction := category_theory.limits.sigma.desc (λ (b' : β), dite (b' = b) (λ (h : b' = b), category_theory.eq_to_hom _) (λ (h : ¬b' = b), 0)), id' := _}
@[instance]
def
category_theory.limits.split_epi_pi_π
{C : Type u}
[category_theory.category C]
{β : Type v}
[decidable_eq β]
[category_theory.limits.has_zero_morphisms C]
(f : β → C)
[category_theory.limits.has_limit (category_theory.discrete.functor f)]
(b : β) :
In the presence of zero morphisms, projections into a product are (split) epimorphisms.
Equations
- category_theory.limits.split_epi_pi_π f b = {section_ := category_theory.limits.pi.lift (λ (b' : β), dite (b = b') (λ (h : b = b'), category_theory.eq_to_hom _) (λ (h : ¬b = b'), 0)), id' := _}
@[instance]
def
category_theory.limits.split_mono_coprod_inl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_colimit (category_theory.limits.pair X Y)] :
In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.
Equations
@[instance]
def
category_theory.limits.split_mono_coprod_inr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_colimit (category_theory.limits.pair X Y)] :
In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms.
Equations
@[instance]
def
category_theory.limits.split_epi_prod_fst
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_limit (category_theory.limits.pair X Y)] :
In the presence of zero morphisms, projections into a product are (split) epimorphisms.
Equations
@[instance]
def
category_theory.limits.split_epi_prod_snd
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
[category_theory.limits.has_limit (category_theory.limits.pair X Y)] :
In the presence of zero morphisms, projections into a product are (split) epimorphisms.