Zero morphisms and zero objects #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
- category_theory.preadditive.preadditive_has_zero_morphisms
- category_theory.non_preadditive_abelian.to_has_zero_morphisms
- category_theory.limits.has_zero_morphisms_pempty
- category_theory.limits.has_zero_morphisms_punit
- category_theory.limits.has_zero_morphisms_opposite
- category_theory.limits.category_theory.functor.has_zero_morphisms
- Action.category_theory.limits.has_zero_morphisms
- category_theory.graded_object.has_zero_morphisms
- homological_complex.category_theory.limits.has_zero_morphisms
- category_theory.differential_object.has_zero_morphisms
- SemiNormedGroup.category_theory.limits.has_zero_morphisms
- SemiNormedGroup₁.category_theory.limits.has_zero_morphisms
Instances of other typeclasses for category_theory.limits.has_zero_morphisms
- category_theory.limits.has_zero_morphisms.has_sizeof_inst
- category_theory.limits.has_zero_morphisms.subsingleton
theorem
category_theory.limits.has_zero_morphisms.comp_zero
{C : Type u}
[category_theory.category C]
[self : category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
(Z : C) :
theorem
category_theory.limits.has_zero_morphisms.zero_comp
{C : Type u}
[category_theory.category C]
[self : category_theory.limits.has_zero_morphisms C]
(X : C)
{Y Z : C}
(f : Y ⟶ Z) :
@[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} :
@[simp]
theorem
category_theory.limits.zero_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
{f : Y ⟶ Z} :
@[protected, instance]
Equations
- category_theory.limits.has_zero_morphisms_pempty = {has_zero := λ (X Y : category_theory.discrete pempty), {zero := {down := _.mpr {down := _}}}, comp_zero' := category_theory.limits.has_zero_morphisms_pempty._proof_2, zero_comp' := category_theory.limits.has_zero_morphisms_pempty._proof_3}
@[protected, instance]
Equations
- category_theory.limits.has_zero_morphisms_punit = {has_zero := λ (X Y : category_theory.discrete punit), {zero := {down := _.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.
@[protected, instance]
@[protected, instance]
def
category_theory.limits.has_zero_morphisms_opposite
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Equations
- category_theory.limits.has_zero_morphisms_opposite = {has_zero := λ (X Y : Cᵒᵖ), {zero := 0.op}, comp_zero' := _, zero_comp' := _}
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
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]
(w : 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]
(w : f ≠ 0) :
@[protected, instance]
def
category_theory.limits.category_theory.functor.has_zero_morphisms
{C : Type u}
[category_theory.category C]
(D : Type u')
[category_theory.category D]
[category_theory.limits.has_zero_morphisms D] :
Equations
- category_theory.limits.category_theory.functor.has_zero_morphisms D = {has_zero := λ (F G : C ⥤ D), {zero := {app := λ (X : C), 0, naturality' := _}}, comp_zero' := _, zero_comp' := _}
@[simp]
theorem
category_theory.limits.zero_app
{C : Type u}
[category_theory.category C]
(D : Type u')
[category_theory.category D]
[category_theory.limits.has_zero_morphisms D]
(F G : C ⥤ D)
(j : C) :
theorem
category_theory.limits.is_zero.eq_zero_of_src
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(o : category_theory.limits.is_zero X)
(f : X ⟶ Y) :
f = 0
theorem
category_theory.limits.is_zero.eq_zero_of_tgt
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(o : category_theory.limits.is_zero Y)
(f : X ⟶ Y) :
f = 0
theorem
category_theory.limits.is_zero.iff_id_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X : C) :
category_theory.limits.is_zero X ↔ 𝟙 X = 0
theorem
category_theory.limits.is_zero.of_mono_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.mono 0] :
theorem
category_theory.limits.is_zero.of_epi_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
[category_theory.epi 0] :
theorem
category_theory.limits.is_zero.of_mono_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
(h : f = 0) :
theorem
category_theory.limits.is_zero.of_epi_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f]
(h : f = 0) :
theorem
category_theory.limits.is_zero.iff_is_split_mono_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_split_mono f] :
category_theory.limits.is_zero X ↔ f = 0
theorem
category_theory.limits.is_zero.iff_is_split_epi_eq_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.is_split_epi f] :
category_theory.limits.is_zero Y ↔ f = 0
theorem
category_theory.limits.is_zero.of_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f]
(i : category_theory.limits.is_zero Y) :
theorem
category_theory.limits.is_zero.of_epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f]
(i : category_theory.limits.is_zero X) :
noncomputable
def
category_theory.limits.is_zero.has_zero_morphisms
{C : Type u}
[category_theory.category C]
{O : C}
(hO : category_theory.limits.is_zero O) :
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
- hO.has_zero_morphisms = {has_zero := λ (X Y : C), {zero := hO.from X ≫ hO.to Y}, comp_zero' := _, zero_comp' := _}
noncomputable
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 ≫ inhabited.default}, comp_zero' := _, zero_comp' := _}
@[simp]
theorem
category_theory.limits.has_zero_object.zero_iso_is_initial_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(t : category_theory.limits.is_initial X) :
@[simp]
theorem
category_theory.limits.has_zero_object.zero_iso_is_initial_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(t : category_theory.limits.is_initial X) :
@[simp]
theorem
category_theory.limits.has_zero_object.zero_iso_is_terminal_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(t : category_theory.limits.is_terminal X) :
@[simp]
theorem
category_theory.limits.has_zero_object.zero_iso_is_terminal_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(t : category_theory.limits.is_terminal X) :
@[protected, instance]
@[simp]
theorem
category_theory.limits.is_zero.map
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms D]
{F : C ⥤ D}
(hF : category_theory.limits.is_zero F)
{X Y : C}
(f : X ⟶ Y) :
@[simp]
theorem
category_theory.functor.zero_obj
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_zero_object D]
(X : C) :
@[simp]
theorem
category_theory.zero_map
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_zero_object D]
[category_theory.limits.has_zero_morphisms D]
{X Y : C}
(f : X ⟶ Y) :
@[simp]
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)
(i : Y ≅ 0) :
f = 0
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)
(i : X ≅ 0) :
f = 0
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)
(i : category_theory.is_isomorphic X 0) :
f = 0
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)
(i : category_theory.is_isomorphic Y 0) :
f = 0
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)
(i : X ≅ 0) :
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)
(i : Y ≅ 0) :
noncomputable
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) :
noncomputable
def
category_theory.limits.iso_zero_of_mono_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}
(h : category_theory.mono 0) :
X ≅ 0
If 0 : X ⟶ Y is an monomorphism, then X ≅ 0.
Equations
- category_theory.limits.iso_zero_of_mono_zero h = {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.iso_zero_of_mono_zero_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(h : category_theory.mono 0) :
@[simp]
theorem
category_theory.limits.iso_zero_of_mono_zero_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(h : category_theory.mono 0) :
@[simp]
theorem
category_theory.limits.iso_zero_of_epi_zero_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(h : category_theory.epi 0) :
@[simp]
theorem
category_theory.limits.iso_zero_of_epi_zero_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(h : category_theory.epi 0) :
noncomputable
def
category_theory.limits.iso_zero_of_epi_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}
(h : category_theory.epi 0) :
Y ≅ 0
If 0 : X ⟶ Y is an epimorphism, then Y ≅ 0.
Equations
- category_theory.limits.iso_zero_of_epi_zero h = {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
category_theory.limits.iso_zero_of_mono_eq_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}
[category_theory.mono f]
(h : f = 0) :
X ≅ 0
If a monomorphism out of X is zero, then X ≅ 0.
Equations
- category_theory.limits.iso_zero_of_mono_eq_zero h = eq.rec (λ [_inst_5 : category_theory.mono 0], category_theory.limits.iso_zero_of_mono_zero _inst_5) _
noncomputable
def
category_theory.limits.iso_zero_of_epi_eq_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}
[category_theory.epi f]
(h : f = 0) :
Y ≅ 0
If an epimorphism in to Y is zero, then Y ≅ 0.
Equations
- category_theory.limits.iso_zero_of_epi_eq_zero h = eq.rec (λ [_inst_5 : category_theory.epi 0], category_theory.limits.iso_zero_of_epi_zero _inst_5) _
noncomputable
def
category_theory.limits.iso_of_is_isomorphic_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_zero_morphisms C]
{X : C}
(P : category_theory.is_isomorphic 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.
Equations
- category_theory.limits.iso_of_is_isomorphic_zero P = {hom := 0, inv := 0, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.is_iso_zero_equiv_symm_apply
{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_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_apply
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C)
(i : category_theory.is_iso 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
noncomputable
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 := λ (ᾰ : 𝟙 X = 0 ∧ 𝟙 Y = 0), ᾰ.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
theorem
category_theory.limits.is_iso_of_source_target_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}
(f : X ⟶ Y)
(i : X ≅ 0)
(j : Y ≅ 0) :
noncomputable
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.
theorem
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.
theorem
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.
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)]
(h : f ≫ g = 0) :
category_theory.limits.image.ι f ≫ g = 0
theorem
category_theory.limits.comp_factor_thru_image_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 g]
(h : f ≫ g = 0) :
@[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) :
noncomputable
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) :
noncomputable
def
category_theory.limits.image_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 factorisation through the zero object is an image factorisation.
Equations
- category_theory.limits.image_factorisation_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' := _}}
@[protected, instance]
noncomputable
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} :
The image of a zero morphism is the zero object.
noncomputable
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.
@[protected, instance]
def
category_theory.limits.is_split_mono_sigma_ι
{C : Type u}
[category_theory.category C]
{β : Type u'}
[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.
@[protected, instance]
def
category_theory.limits.is_split_epi_pi_π
{C : Type u}
[category_theory.category C]
{β : Type u'}
[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.
@[protected, instance]
def
category_theory.limits.is_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.
@[protected, instance]
def
category_theory.limits.is_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.
@[protected, instance]
def
category_theory.limits.is_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.
@[protected, instance]
def
category_theory.limits.is_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.