doc-next-gen

Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Module docstring

{"# 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] "}
CategoryTheory.Limits.HasZeroMorphisms structure
Full source 
/-- 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. -/
class HasZeroMorphisms where
  /-- Every morphism space has zero -/
  [zero : ∀ X Y : C, Zero (X ⟶ Y)]
  /-- `f` composed with `0` is `0` -/
  comp_zero : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) := by aesop_cat
  /-- `0` composed with `f` is `0` -/
  zero_comp : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) := by aesop_cat
Category with Zero Morphisms
Informal description
A category \( C \) is said to "have zero morphisms" if for every pair of objects \( X \) and \( Y \) in \( C \), there is a designated zero morphism \( 0 : X \to Y \), and for any morphisms \( f \) and \( g \) in \( C \), the compositions \( f \circ 0 \) and \( 0 \circ g \) are also zero morphisms. This structure ensures that zero morphisms behave consistently with respect to composition in the category.
CategoryTheory.Limits.comp_zero theorem
[HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} : f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z)
Full source 
@[simp]
theorem comp_zero [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} :
    f ≫ (0 : Y ⟶ Z) = (0 : X ⟶ Z) :=
  HasZeroMorphisms.comp_zero f Z
Right Composition with Zero Morphism Yields Zero Morphism
Informal description
In a category $C$ with zero morphisms, for any objects $X, Y, Z$ and any morphism $f : X \to Y$, the composition of $f$ with the zero morphism $0 : Y \to Z$ equals the zero morphism $0 : X \to Z$, i.e., $f \circ 0 = 0$.
CategoryTheory.Limits.zero_comp theorem
[HasZeroMorphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} : (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z)
Full source 
@[simp]
theorem zero_comp [HasZeroMorphisms C] {X : C} {Y Z : C} {f : Y ⟶ Z} :
    (0 : X ⟶ Y) ≫ f = (0 : X ⟶ Z) :=
  HasZeroMorphisms.zero_comp X f
Left Composition with Zero Morphism Yields Zero Morphism
Informal description
In a category $C$ with zero morphisms, for any objects $X, Y, Z$ and any morphism $f : Y \to Z$, the composition of the zero morphism $0 : X \to Y$ with $f$ equals the zero morphism $0 : X \to Z$, i.e., $0 \circ f = 0$.
CategoryTheory.Limits.HasZeroMorphisms.ext theorem
(I J : HasZeroMorphisms C) : I = J
Full source 
/-- 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.
-/
theorem ext (I J : HasZeroMorphisms C) : I = J := by
  apply ext_aux
  intro X Y
  have : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (I.zero X Y).zero := by
    apply I.zero_comp X (J.zero Y Y).zero
  have that : (I.zero X Y).zero ≫ (J.zero Y Y).zero = (J.zero X Y).zero := by
    apply J.comp_zero (I.zero X Y).zero Y
  rw [← this, ← that]
Uniqueness of Zero Morphism Structures on a Category
Informal description
For any category $C$, if $I$ and $J$ are two instances of the structure `HasZeroMorphisms` on $C$, then $I$ and $J$ are equal.
CategoryTheory.Limits.HasZeroMorphisms.instSubsingleton instance
: Subsingleton (HasZeroMorphisms C)
Full source 
instance : Subsingleton (HasZeroMorphisms C) :=
  ⟨ext⟩
Uniqueness of Zero Morphism Structures on a Category
Informal description
For any category $C$, there is at most one way to equip $C$ with zero morphisms.
CategoryTheory.Limits.hasZeroMorphismsOpposite instance
[HasZeroMorphisms C] : HasZeroMorphisms Cᵒᵖ
Full source 
instance hasZeroMorphismsOpposite [HasZeroMorphisms C] : HasZeroMorphisms Cᵒᵖ where
  zero X Y := ⟨(0 : unop Y ⟶ unop X).op⟩
  comp_zero f Z := congr_arg Quiver.Hom.op (HasZeroMorphisms.zero_comp (unop Z) f.unop)
  zero_comp X {Y Z} (f : Y ⟶ Z) :=
    congrArg Quiver.Hom.op (HasZeroMorphisms.comp_zero f.unop (unop X))
Opposite Category Inherits Zero Morphisms
Informal description
For any category $C$ with zero morphisms, its opposite category $C^{\mathrm{op}}$ also has zero morphisms.
CategoryTheory.Limits.op_zero theorem
(X Y : C) : (0 : X ⟶ Y).op = 0
Full source 
@[simp] lemma op_zero (X Y : C) : (0 : X ⟶ Y).op = 0 := rfl
Opposite of Zero Morphism is Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, the opposite of the zero morphism $0 : X \to Y$ in $C$ is equal to the zero morphism in the opposite category $C^{\mathrm{op}}$.
CategoryTheory.Limits.unop_zero theorem
(X Y : Cᵒᵖ) : (0 : X ⟶ Y).unop = 0
Full source 
@[simp] lemma unop_zero (X Y : Cᵒᵖ) : (0 : X ⟶ Y).unop = 0 := rfl
Unopposite of Zero Morphism is Zero
Informal description
For any objects $X$ and $Y$ in the opposite category $C^{\mathrm{op}}$, the unopposite of the zero morphism $0 : X \to Y$ in $C^{\mathrm{op}}$ is equal to the zero morphism in the original category $C$.
CategoryTheory.Limits.zero_of_comp_mono theorem
{X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : f ≫ g = 0) : f = 0
Full source 
theorem zero_of_comp_mono {X Y Z : C} {f : X ⟶ Y} (g : Y ⟶ Z) [Mono g] (h : f ≫ g = 0) : f = 0 := by
  rw [← zero_comp, cancel_mono] at h
  exact h
Zero Morphism from Composition with Monomorphism
Informal description
In a category $C$ with zero morphisms, given objects $X, Y, Z$, a morphism $f : X \to Y$, and a monomorphism $g : Y \to Z$, if the composition $f \circ g$ is the zero morphism, then $f$ must be the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.zero_of_epi_comp theorem
{X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : f ≫ g = 0) : g = 0
Full source 
theorem zero_of_epi_comp {X Y Z : C} (f : X ⟶ Y) {g : Y ⟶ Z} [Epi f] (h : f ≫ g = 0) : g = 0 := by
  rw [← comp_zero, cancel_epi] at h
  exact h
Zero Morphism from Epimorphism Composition
Informal description
In a category $C$ with zero morphisms, for any objects $X, Y, Z$, an epimorphism $f : X \to Y$, and a morphism $g : Y \to Z$, if the composition $f \circ g$ is the zero morphism, then $g$ must be the zero morphism, i.e., $g = 0$.
CategoryTheory.Limits.nonzero_image_of_nonzero theorem
{X Y : C} {f : X ⟶ Y} [HasImage f] (w : f ≠ 0) : image.ι f ≠ 0
Full source 
theorem nonzero_image_of_nonzero {X Y : C} {f : X ⟶ Y} [HasImage f] (w : f ≠ 0) : image.ιimage.ι f ≠ 0 :=
  fun h => w (eq_zero_of_image_eq_zero h)
Nonzero Image of Nonzero Morphism
Informal description
For any morphism $f \colon X \to Y$ in a category $C$ with zero morphisms, if $f$ is nonzero and $C$ has images, then the image inclusion morphism $\iota_f$ of $f$ is also nonzero.
CategoryTheory.Limits.instHasZeroMorphismsFunctor instance
: HasZeroMorphisms (C ⥤ D)
Full source 
instance : HasZeroMorphisms (C ⥤ D) where
  zero F G := ⟨{ app := fun _ => 0 }⟩
  comp_zero := fun η H => by
    ext X; dsimp; apply comp_zero
  zero_comp := fun F {G H} η => by
    ext X; dsimp; apply zero_comp
Functor Category Inherits Zero Morphisms
Informal description
For any categories $C$ and $D$ where $D$ has zero morphisms, the functor category $C \to D$ also has zero morphisms. Specifically, the zero morphism between two functors $F, G \colon C \to D$ is the natural transformation whose components are the zero morphisms in $D$ at each object in $C$.
CategoryTheory.Limits.zero_app theorem
(F G : C ⥤ D) (j : C) : (0 : F ⟶ G).app j = 0
Full source 
@[simp]
theorem zero_app (F G : C ⥤ D) (j : C) : (0 : F ⟶ G).app j = 0 := rfl
Component of Zero Natural Transformation is Zero Morphism
Informal description
For any functors $F, G \colon C \to D$ between categories $C$ and $D$ where $D$ has zero morphisms, and for any object $j$ in $C$, the component of the zero natural transformation $0 \colon F \to G$ at $j$ is equal to the zero morphism $0 \colon F(j) \to G(j)$ in $D$.
CategoryTheory.Limits.IsZero.iff_id_eq_zero theorem
(X : C) : IsZero X ↔ 𝟙 X = 0
Full source 
theorem iff_id_eq_zero (X : C) : IsZeroIsZero X ↔ 𝟙 X = 0 :=
  ⟨fun h => h.eq_of_src _ _, fun h =>
    ⟨fun Y => ⟨⟨⟨0⟩, fun f => by
        rw [← id_comp f, ← id_comp (0 : X ⟶ Y), h, zero_comp, zero_comp]; simp only⟩⟩,
    fun Y => ⟨⟨⟨0⟩, fun f => by
        rw [← comp_id f, ← comp_id (0 : Y ⟶ X), h, comp_zero, comp_zero]; simp only ⟩⟩⟩⟩
Characterization of Zero Objects via Identity Morphism
Informal description
An object $X$ in a category $C$ is a zero object if and only if its identity morphism $\mathrm{id}_X$ is equal to the zero morphism $0 : X \to X$.
CategoryTheory.Limits.IsZero.of_mono_zero theorem
(X Y : C) [Mono (0 : X ⟶ Y)] : IsZero X
Full source 
theorem of_mono_zero (X Y : C) [Mono (0 : X ⟶ Y)] : IsZero X :=
  (iff_id_eq_zero X).mpr ((cancel_mono (0 : X ⟶ Y)).1 (by simp))
Zero Object Characterization via Monic Zero Morphism
Informal description
In a category $C$, if the zero morphism $0 : X \to Y$ is a monomorphism, then the object $X$ is a zero object.
CategoryTheory.Limits.IsZero.of_epi_zero theorem
(X Y : C) [Epi (0 : X ⟶ Y)] : IsZero Y
Full source 
theorem of_epi_zero (X Y : C) [Epi (0 : X ⟶ Y)] : IsZero Y :=
  (iff_id_eq_zero Y).mpr ((cancel_epi (0 : X ⟶ Y)).1 (by simp))
Zero Object Characterization via Epimorphic Zero Morphism
Informal description
In a category $C$ with zero morphisms, if the zero morphism $0 : X \to Y$ is an epimorphism, then the object $Y$ is a zero object.
CategoryTheory.Limits.IsZero.of_mono_eq_zero theorem
{X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) : IsZero X
Full source 
theorem of_mono_eq_zero {X Y : C} (f : X ⟶ Y) [Mono f] (h : f = 0) : IsZero X := by
  subst h
  apply of_mono_zero X Y
Zero Object Characterization via Monomorphism Equal to Zero
Informal description
In a category $C$ with zero morphisms, if a monomorphism $f : X \to Y$ is equal to the zero morphism, then the object $X$ is a zero object.
CategoryTheory.Limits.IsZero.of_epi_eq_zero theorem
{X Y : C} (f : X ⟶ Y) [Epi f] (h : f = 0) : IsZero Y
Full source 
theorem of_epi_eq_zero {X Y : C} (f : X ⟶ Y) [Epi f] (h : f = 0) : IsZero Y := by
  subst h
  apply of_epi_zero X Y
Zero Object Characterization via Epimorphic Zero Morphism Equality
Informal description
In a category $C$ with zero morphisms, given an epimorphism $f : X \to Y$ that is equal to the zero morphism, the object $Y$ is a zero object.
CategoryTheory.Limits.IsZero.iff_isSplitMono_eq_zero theorem
{X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsZero X ↔ f = 0
Full source 
theorem iff_isSplitMono_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitMono f] : IsZeroIsZero X ↔ f = 0 := by
  rw [iff_id_eq_zero]
  constructor
  · intro h
    rw [← Category.id_comp f, h, zero_comp]
  · intro h
    rw [← IsSplitMono.id f]
    simp only [h, zero_comp]
Characterization of Zero Objects via Split Monomorphisms: $X$ is zero $\iff$ $f = 0$ for split mono $f$
Informal description
For any objects $X$ and $Y$ in a category $C$ and any split monomorphism $f : X \to Y$, the object $X$ is a zero object if and only if $f$ is the zero morphism.
CategoryTheory.Limits.IsZero.iff_isSplitEpi_eq_zero theorem
{X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZero Y ↔ f = 0
Full source 
theorem iff_isSplitEpi_eq_zero {X Y : C} (f : X ⟶ Y) [IsSplitEpi f] : IsZeroIsZero Y ↔ f = 0 := by
  rw [iff_id_eq_zero]
  constructor
  · intro h
    rw [← Category.comp_id f, h, comp_zero]
  · intro h
    rw [← IsSplitEpi.id f]
    simp [h]
Characterization of Zero Objects via Split Epimorphisms: $Y$ is zero $\iff$ $f = 0$
Informal description
Let $C$ be a category with zero morphisms, and let $f : X \to Y$ be a split epimorphism in $C$. Then the object $Y$ is a zero object if and only if $f$ is the zero morphism.
CategoryTheory.Limits.IsZero.of_mono theorem
{X Y : C} (f : X ⟶ Y) [Mono f] (i : IsZero Y) : IsZero X
Full source 
theorem of_mono {X Y : C} (f : X ⟶ Y) [Mono f] (i : IsZero Y) : IsZero X := by
  have hf := i.eq_zero_of_tgt f
  subst hf
  exact IsZero.of_mono_zero X Y
Zero Object Characterization via Monomorphism to Zero Object
Informal description
Let $C$ be a category with zero morphisms, and let $f : X \to Y$ be a monomorphism in $C$. If $Y$ is a zero object, then $X$ is also a zero object.
CategoryTheory.Limits.IsZero.of_epi theorem
{X Y : C} (f : X ⟶ Y) [Epi f] (i : IsZero X) : IsZero Y
Full source 
theorem of_epi {X Y : C} (f : X ⟶ Y) [Epi f] (i : IsZero X) : IsZero Y := by
  have hf := i.eq_zero_of_src f
  subst hf
  exact IsZero.of_epi_zero X Y
Epimorphism from Zero Object Implies Target is Zero Object
Informal description
Let $C$ be a category with zero morphisms, and let $f : X \to Y$ be an epimorphism in $C$. If $X$ is a zero object, then $Y$ is also a zero object.
CategoryTheory.Limits.IsZero.hasZeroMorphisms definition
{O : C} (hO : IsZero O) : HasZeroMorphisms C
Full source 
/-- 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 `HasZeroObjects`. -/
def IsZero.hasZeroMorphisms {O : C} (hO : IsZero O) : HasZeroMorphisms C where
  zero X Y := { zero := hO.from_ X ≫ hO.to_ Y }
  zero_comp X {Y Z} f := by
    change (hO.from_ X ≫ hO.to_ Y) ≫ f = hO.from_ X ≫ hO.to_ Z
    rw [Category.assoc]
    congr
    apply hO.eq_of_src
  comp_zero {X Y} f Z := by
    change f ≫ (hO.from_ Y ≫ hO.to_ Z) = hO.from_ X ≫ hO.to_ Z
    rw [← Category.assoc]
    congr
    apply hO.eq_of_tgt
Zero morphisms from a zero object
Informal description
Given an object \( O \) in a category \( C \) that is a zero object (i.e., \( O \) is both initial and terminal), the category \( C \) has zero morphisms. Specifically, for any objects \( X \) and \( Y \) in \( C \), the zero morphism \( 0 : X \to Y \) is defined as the composition of the unique morphism \( X \to O \) and the unique morphism \( O \to Y \). This definition ensures that compositions involving zero morphisms satisfy \( 0 \circ f = 0 \) and \( f \circ 0 = 0 \) for any morphism \( f \).
CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject definition
: HasZeroMorphisms C
Full source 
/-- 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 `has_zero_morphisms` 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 `HasZeroObjects`. -/
def zeroMorphismsOfZeroObject : HasZeroMorphisms C where
  zero X _ := { zero := (default : X ⟶ 0) ≫ default }
  zero_comp X {Y Z} f := by
    change ((default : X ⟶ 0) ≫ default) ≫ f = (default : X ⟶ 0) ≫ default
    rw [Category.assoc]
    congr
    simp only [eq_iff_true_of_subsingleton]
  comp_zero {X Y} f Z := by
    change f ≫ (default : Y ⟶ 0) ≫ default = (default : X ⟶ 0) ≫ default
    rw [← Category.assoc]
    congr
    simp only [eq_iff_true_of_subsingleton]
Zero Morphisms from Zero Object
Informal description
Given a category \( C \) with a zero object, the structure of zero morphisms is defined where for any objects \( X \) and \( Y \), the zero morphism \( 0 : X \to Y \) is given by the composition of the unique morphism \( X \to 0 \) and the unique morphism \( 0 \to Y \). This ensures that compositions involving zero morphisms behave as expected, i.e., \( 0 \circ f = 0 \) and \( f \circ 0 = 0 \) for any morphism \( f \).
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_hom theorem
{X : C} (t : IsInitial X) : (zeroIsoIsInitial t).hom = 0
Full source 
@[simp]
theorem zeroIsoIsInitial_hom {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).hom = 0 := by ext
Homomorphism of Zero-Initial Isomorphism is Zero Morphism
Informal description
For any object $X$ in a category $C$ with a zero object, if $X$ is initial, then the homomorphism part of the isomorphism between $X$ and the zero object is the zero morphism, i.e., $(zeroIsoIsInitial\ t).hom = 0$.
CategoryTheory.Limits.HasZeroObject.zeroIsoIsInitial_inv theorem
{X : C} (t : IsInitial X) : (zeroIsoIsInitial t).inv = 0
Full source 
@[simp]
theorem zeroIsoIsInitial_inv {X : C} (t : IsInitial X) : (zeroIsoIsInitial t).inv = 0 := by ext
Inverse of Zero-Initial Isomorphism is Zero Morphism
Informal description
For any object $X$ in a category $C$ with a zero object, if $X$ is initial, then the inverse of the isomorphism between $X$ and the zero object is the zero morphism, i.e., $(zeroIsoIsInitial\ t).inv = 0$.
CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_hom theorem
{X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).hom = 0
Full source 
@[simp]
theorem zeroIsoIsTerminal_hom {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).hom = 0 := by ext
Homomorphism of Zero-Terminal Isomorphism is Zero Morphism
Informal description
For any object $X$ in a category $C$ with a zero object, if $X$ is terminal, then the homomorphism part of the isomorphism between $X$ and the zero object is the zero morphism, i.e., $(zeroIsoIsTerminal\ t).hom = 0$.
CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal_inv theorem
{X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).inv = 0
Full source 
@[simp]
theorem zeroIsoIsTerminal_inv {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).inv = 0 := by ext
Inverse of Zero-Terminal Isomorphism is Zero Morphism
Informal description
For any object $X$ in a category $C$ with a zero object, if $X$ is terminal, then the inverse of the isomorphism between $X$ and the zero object is the zero morphism, i.e., $(zeroIsoIsTerminal\ t).inv = 0$.
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_hom theorem
[HasInitial C] : zeroIsoInitial.hom = (0 : 0 ⟶ ⊥_ C)
Full source 
@[simp]
theorem zeroIsoInitial_hom [HasInitial C] : zeroIsoInitial.hom = (0 : 0 ⟶ ⊥_ C) := by ext
Zero Morphism Property of Zero-Initial Isomorphism Homomorphism
Informal description
In a category $C$ with a zero object and an initial object, the homomorphism part of the isomorphism between the zero object $0$ and the initial object $\bot_C$ is the zero morphism, i.e., $\text{zeroIsoInitial.hom} = 0_{0 \to \bot_C}$.
CategoryTheory.Limits.HasZeroObject.zeroIsoInitial_inv theorem
[HasInitial C] : zeroIsoInitial.inv = (0 : ⊥_ C ⟶ 0)
Full source 
@[simp]
theorem zeroIsoInitial_inv [HasInitial C] : zeroIsoInitial.inv = (0 : ⊥_ C⊥_ C ⟶ 0) := by ext
Inverse of Zero-Initial Isomorphism is Zero Morphism
Informal description
In a category $C$ with a zero object and an initial object $\bot_C$, the inverse of the isomorphism between the zero object $0$ and the initial object is the zero morphism from $\bot_C$ to $0$, i.e., $\text{zeroIsoInitial.inv} = 0_{\bot_C \to 0}$.
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_hom theorem
[HasTerminal C] : zeroIsoTerminal.hom = (0 : 0 ⟶ ⊤_ C)
Full source 
@[simp]
theorem zeroIsoTerminal_hom [HasTerminal C] : zeroIsoTerminal.hom = (0 : 0 ⟶ ⊤_ C) := by ext
Zero-Terminal Isomorphism Homomorphism is Zero Morphism
Informal description
In a category $C$ with a terminal object $\top_C$ and a zero object $0$, the homomorphism part of the isomorphism between $0$ and $\top_C$ is equal to the zero morphism from $0$ to $\top_C$.
CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal_inv theorem
[HasTerminal C] : zeroIsoTerminal.inv = (0 : ⊤_ C ⟶ 0)
Full source 
@[simp]
theorem zeroIsoTerminal_inv [HasTerminal C] : zeroIsoTerminal.inv = (0 : ⊤_ C⊤_ C ⟶ 0) := by ext
Inverse of Zero-Terminal Isomorphism is Zero Morphism
Informal description
In a category $C$ with a terminal object and a zero object, the inverse of the isomorphism between the zero object and the terminal object is equal to the zero morphism from the terminal object to the zero object.
CategoryTheory.Limits.IsZero.map theorem
[HasZeroObject D] [HasZeroMorphisms D] {F : C ⥤ D} (hF : IsZero F) {X Y : C} (f : X ⟶ Y) : F.map f = 0
Full source 
@[simp]
theorem IsZero.map [HasZeroObject D] [HasZeroMorphisms D] {F : C ⥤ D} (hF : IsZero F) {X Y : C}
    (f : X ⟶ Y) : F.map f = 0 :=
  (hF.obj _).eq_of_src _ _
Zero Functor Maps All Morphisms to Zero Morphisms
Informal description
Let $C$ and $D$ be categories where $D$ has a zero object and zero morphisms. If $F : C \to D$ is a zero functor (i.e., $F$ is isomorphic to the zero object in the functor category $C \to D$), then for any morphism $f : X \to Y$ in $C$, the image of $f$ under $F$ is the zero morphism in $D$, i.e., $F(f) = 0$.
CategoryTheory.Functor.zero_obj theorem
[HasZeroObject D] (X : C) : IsZero ((0 : C ⥤ D).obj X)
Full source 
@[simp]
theorem _root_.CategoryTheory.Functor.zero_obj [HasZeroObject D] (X : C) :
    IsZero ((0 : C ⥤ D).obj X) :=
  (isZero_zero _).obj _
Zero Functor Maps Objects to Zero Objects
Informal description
For any category $C$ and any object $X$ in $C$, the image of $X$ under the zero functor $0 : C \to D$ is a zero object in $D$, provided $D$ has a zero object.
CategoryTheory.zero_map theorem
[HasZeroObject D] [HasZeroMorphisms D] {X Y : C} (f : X ⟶ Y) : (0 : C ⥤ D).map f = 0
Full source 
@[simp]
theorem _root_.CategoryTheory.zero_map [HasZeroObject D] [HasZeroMorphisms D] {X Y : C}
    (f : X ⟶ Y) : (0 : C ⥤ D).map f = 0 :=
  (isZero_zero _).map _
Zero Functor Maps Morphisms to Zero Morphisms
Informal description
Let $C$ and $D$ be categories where $D$ has a zero object and zero morphisms. For any morphism $f : X \to Y$ in $C$, the image of $f$ under the zero functor $0 : C \to D$ is the zero morphism in $D$, i.e., $0(f) = 0$.
CategoryTheory.Limits.id_zero theorem
: 𝟙 (0 : C) = (0 : (0 : C) ⟶ 0)
Full source 
@[simp]
theorem id_zero : 𝟙 (0 : C) = (0 : (0 : C) ⟶ 0) := by apply HasZeroObject.from_zero_ext
Identity on Zero Object is Zero Morphism
Informal description
In a category $C$ with a zero object, the identity morphism on the zero object is equal to the zero morphism from the zero object to itself, i.e., $\text{id}_0 = 0_{0 \to 0}$.
CategoryTheory.Limits.zero_of_to_zero theorem
{X : C} (f : X ⟶ 0) : f = 0
Full source 
/-- An arrow ending in the zero object is zero -/
theorem zero_of_to_zero {X : C} (f : X ⟶ 0) : f = 0 := by ext
Morphism to Zero Object is Zero
Informal description
For any object $X$ in a category $C$ with a zero object, any morphism $f : X \to 0$ is equal to the zero morphism.
CategoryTheory.Limits.zero_of_target_iso_zero theorem
{X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : f = 0
Full source 
theorem zero_of_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : f = 0 := by
  have h : f = f ≫ i.hom ≫ 𝟙 0 ≫ i.inv := by simp only [Iso.hom_inv_id, id_comp, comp_id]
  simpa using h
Morphism to Object Isomorphic to Zero is Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if there exists an isomorphism $i : Y \cong 0$ where $0$ is the zero object, then any morphism $f : X \to Y$ is equal to the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.zero_of_from_zero theorem
{X : C} (f : 0 ⟶ X) : f = 0
Full source 
/-- An arrow starting at the zero object is zero -/
theorem zero_of_from_zero {X : C} (f : 0 ⟶ X) : f = 0 := by ext
Morphism from Zero Object is Zero
Informal description
In a category $C$ with a zero object, any morphism $f$ from the zero object to an object $X$ is equal to the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.zero_of_source_iso_zero theorem
{X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0
Full source 
theorem zero_of_source_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : f = 0 := by
  have h : f = i.hom ≫ 𝟙 0 ≫ i.inv ≫ f := by simp only [Iso.hom_inv_id_assoc, id_comp, comp_id]
  simpa using h
Morphism from Object Isomorphic to Zero is Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if there exists an isomorphism $i : X \cong 0$ where $0$ is the zero object, then any morphism $f : X \to Y$ is equal to the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.zero_of_source_iso_zero' theorem
{X Y : C} (f : X ⟶ Y) (i : IsIsomorphic X 0) : f = 0
Full source 
theorem zero_of_source_iso_zero' {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic X 0) : f = 0 :=
  zero_of_source_iso_zero f (Nonempty.some i)
Morphism from Zero-Isomorphic Object is Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if $X$ is isomorphic to the zero object (i.e., $X \cong 0$), then any morphism $f : X \to Y$ is equal to the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.zero_of_target_iso_zero' theorem
{X Y : C} (f : X ⟶ Y) (i : IsIsomorphic Y 0) : f = 0
Full source 
theorem zero_of_target_iso_zero' {X Y : C} (f : X ⟶ Y) (i : IsIsomorphic Y 0) : f = 0 :=
  zero_of_target_iso_zero f (Nonempty.some i)
Morphism to Zero-Isomorphic Object is Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if $Y$ is isomorphic to the zero object $0$, then any morphism $f : X \to Y$ is equal to the zero morphism, i.e., $f = 0$.
CategoryTheory.Limits.mono_of_source_iso_zero theorem
{X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : Mono f
Full source 
theorem mono_of_source_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) : Mono f :=
  ⟨fun {Z} g h _ => by rw [zero_of_target_iso_zero g i, zero_of_target_iso_zero h i]⟩
Monomorphism from Object Isomorphic to Zero
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if there exists an isomorphism $i : X \cong 0$ where $0$ is the zero object, then any morphism $f : X \to Y$ is a monomorphism.
CategoryTheory.Limits.epi_of_target_iso_zero theorem
{X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : Epi f
Full source 
theorem epi_of_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : Y ≅ 0) : Epi f :=
  ⟨fun {Z} g h _ => by rw [zero_of_source_iso_zero g i, zero_of_source_iso_zero h i]⟩
Morphism to Zero Object is Epimorphism
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if $Y$ is isomorphic to the zero object (i.e., $Y \cong 0$), then any morphism $f : X \to Y$ is an epimorphism.
CategoryTheory.Limits.idZeroEquivIsoZero definition
(X : C) : 𝟙 X = 0 ≃ (X ≅ 0)
Full source 
/-- 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 `≃`.
-/
def idZeroEquivIsoZero (X : C) : 𝟙𝟙 X = 0 ≃ (X ≅ 0) where
  toFun h :=
    { hom := 0
      inv := 0 }
  invFun i := zero_of_target_iso_zero (𝟙 X) i
  left_inv := by aesop_cat
  right_inv := by aesop_cat
Equivalence between identity being zero and isomorphism to zero object
Informal description
For an object \( X \) in a category \( C \), the identity morphism \( \mathbf{1}_X \) being equal to the zero morphism is equivalent to \( X \) being isomorphic to the zero object. This equivalence is expressed as a bijection between the two conditions.
CategoryTheory.Limits.idZeroEquivIsoZero_apply_hom theorem
(X : C) (h : 𝟙 X = 0) : ((idZeroEquivIsoZero X) h).hom = 0
Full source 
@[simp]
theorem idZeroEquivIsoZero_apply_hom (X : C) (h : 𝟙 X = 0) : ((idZeroEquivIsoZero X) h).hom = 0 :=
  rfl
Homomorphism Component of Isomorphism from Identity Equals Zero is Zero
Informal description
For any object $X$ in a category $C$ with zero morphisms, if the identity morphism $1_X$ equals the zero morphism, then the homomorphism component of the isomorphism $(X \cong 0)$ obtained via the equivalence $1_X = 0 \leftrightarrow (X \cong 0)$ is the zero morphism.
CategoryTheory.Limits.idZeroEquivIsoZero_apply_inv theorem
(X : C) (h : 𝟙 X = 0) : ((idZeroEquivIsoZero X) h).inv = 0
Full source 
@[simp]
theorem idZeroEquivIsoZero_apply_inv (X : C) (h : 𝟙 X = 0) : ((idZeroEquivIsoZero X) h).inv = 0 :=
  rfl
Inverse of Isomorphism from Identity Equals Zero is Zero
Informal description
For any object $X$ in a category $C$ with zero morphisms, if the identity morphism $\mathbf{1}_X$ equals the zero morphism, then the inverse component of the isomorphism $(X \cong 0)$ obtained via the equivalence $\mathbf{1}_X = 0 \leftrightarrow (X \cong 0)$ is the zero morphism.
CategoryTheory.Limits.isoZeroOfMonoZero definition
{X Y : C} (_ : Mono (0 : X ⟶ Y)) : X ≅ 0
Full source 
/-- If `0 : X ⟶ Y` is a monomorphism, then `X ≅ 0`. -/
@[simps]
def isoZeroOfMonoZero {X Y : C} (_ : Mono (0 : X ⟶ Y)) : X ≅ 0 where
  hom := 0
  inv := 0
  hom_inv_id := (cancel_mono (0 : X ⟶ Y)).mp (by simp)
Isomorphism to zero object from mono zero morphism
Informal description
Given objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, if the zero morphism \( 0 : X \to Y \) is a monomorphism, then \( X \) is isomorphic to the zero object. The isomorphism is given by the zero morphisms in both directions, and the isomorphism condition follows from the monomorphism property of the zero morphism.
CategoryTheory.Limits.isoZeroOfEpiZero definition
{X Y : C} (_ : Epi (0 : X ⟶ Y)) : Y ≅ 0
Full source 
/-- If `0 : X ⟶ Y` is an epimorphism, then `Y ≅ 0`. -/
@[simps]
def isoZeroOfEpiZero {X Y : C} (_ : Epi (0 : X ⟶ Y)) : Y ≅ 0 where
  hom := 0
  inv := 0
  hom_inv_id := (cancel_epi (0 : X ⟶ Y)).mp (by simp)
Isomorphism to zero object from epi zero morphism
Informal description
Given objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, if the zero morphism \( 0 : X \to Y \) is an epimorphism, then \( Y \) is isomorphic to the zero object.
CategoryTheory.Limits.isoZeroOfMonoEqZero definition
{X Y : C} {f : X ⟶ Y} [Mono f] (h : f = 0) : X ≅ 0
Full source 
/-- If a monomorphism out of `X` is zero, then `X ≅ 0`. -/
def isoZeroOfMonoEqZero {X Y : C} {f : X ⟶ Y} [Mono f] (h : f = 0) : X ≅ 0 := by
  subst h
  apply isoZeroOfMonoZero ‹_›
Isomorphism to zero object from monomorphic zero morphism
Informal description
Given objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, if a monomorphism \( f : X \to Y \) is equal to the zero morphism, then \( X \) is isomorphic to the zero object.
CategoryTheory.Limits.isoZeroOfEpiEqZero definition
{X Y : C} {f : X ⟶ Y} [Epi f] (h : f = 0) : Y ≅ 0
Full source 
/-- If an epimorphism in to `Y` is zero, then `Y ≅ 0`. -/
def isoZeroOfEpiEqZero {X Y : C} {f : X ⟶ Y} [Epi f] (h : f = 0) : Y ≅ 0 := by
  subst h
  apply isoZeroOfEpiZero ‹_›
Isomorphism to zero object from epimorphic zero morphism
Informal description
Given objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, if a morphism \( f : X \to Y \) is an epimorphism and equals the zero morphism, then \( Y \) is isomorphic to the zero object.
CategoryTheory.Limits.isoOfIsIsomorphicZero definition
{X : C} (P : IsIsomorphic X 0) : X ≅ 0
Full source 
/-- 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 isoOfIsIsomorphicZero {X : C} (P : IsIsomorphic X 0) : X ≅ 0 where
  hom := 0
  inv := 0
  hom_inv_id := by
    have P := P.some
    rw [← P.hom_inv_id, ← Category.id_comp P.inv]
    apply Eq.symm
    simp only [id_comp, Iso.hom_inv_id, comp_zero]
    apply (idZeroEquivIsoZero X).invFun P
  inv_hom_id := by simp
Isomorphism from an object to zero via zero morphisms
Informal description
Given an object \( X \) in a category \( C \) that is isomorphic to the zero object, there exists an isomorphism \( X \cong 0 \) where both the forward and backward morphisms are the zero morphisms. This construction avoids the need for choice by utilizing the zero morphism directly.
CategoryTheory.Limits.isIsoZeroEquiv definition
(X Y : C) : IsIso (0 : X ⟶ Y) ≃ 𝟙 X = 0 ∧ 𝟙 Y = 0
Full source 
/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
the identities on both `X` and `Y` are zero.
-/
def isIsoZeroEquiv (X Y : C) : IsIsoIsIso (0 : X ⟶ Y) ≃ 𝟙 X = 0 ∧ 𝟙 Y = 0 where
  toFun := by
    intro i
    rw [← IsIso.hom_inv_id (0 : X ⟶ Y)]
    rw [← IsIso.inv_hom_id (0 : X ⟶ Y)]
    simp only [eq_self_iff_true,comp_zero,and_self,zero_comp]
  invFun h := ⟨⟨(0 : Y ⟶ X), by aesop_cat⟩⟩
  left_inv := by aesop_cat
  right_inv := by aesop_cat
Isomorphism condition for zero morphisms
Informal description
For any objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, the zero morphism \( 0 : X \to Y \) is an isomorphism if and only if the identity morphisms on \( X \) and \( Y \) are both equal to the zero morphism. In other words, \( \text{IsIso}(0) \iff (𝟙_X = 0) \land (𝟙_Y = 0) \).
CategoryTheory.Limits.isIsoZeroSelfEquiv definition
(X : C) : IsIso (0 : X ⟶ X) ≃ 𝟙 X = 0
Full source 
/-- A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
the identity on `X` is zero.
-/
def isIsoZeroSelfEquiv (X : C) : IsIsoIsIso (0 : X ⟶ X) ≃ 𝟙 X = 0 := by simpa using isIsoZeroEquiv X X
Isomorphism condition for zero endomorphism
Informal description
For any object \( X \) in a category \( C \) with zero morphisms, the zero morphism \( 0 : X \to X \) is an isomorphism if and only if the identity morphism on \( X \) is equal to the zero morphism. In other words, \( \text{IsIso}(0) \iff (𝟙_X = 0) \).
CategoryTheory.Limits.isIsoZeroEquivIsoZero definition
(X Y : C) : IsIso (0 : X ⟶ Y) ≃ (X ≅ 0) × (Y ≅ 0)
Full source 
/-- A zero morphism `0 : X ⟶ Y` is an isomorphism if and only if
`X` and `Y` are isomorphic to the zero object.
-/
def isIsoZeroEquivIsoZero (X Y : C) : IsIsoIsIso (0 : X ⟶ Y) ≃ (X ≅ 0) × (Y ≅ 0) := by
  -- This is lame, because `Prod` can't cope with `Prop`, so we can't use `Equiv.prodCongr`.
  refine (isIsoZeroEquiv X Y).trans ?_
  symm
  fconstructor
  · rintro ⟨eX, eY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X).symm eX
    · exact (idZeroEquivIsoZero Y).symm eY
  · rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY
  · aesop_cat
  · aesop_cat
Isomorphism condition for zero morphisms via zero object isomorphism
Informal description
For any objects \( X \) and \( Y \) in a category \( C \) with zero morphisms, the zero morphism \( 0 : X \to Y \) is an isomorphism if and only if both \( X \) and \( Y \) are isomorphic to the zero object. This equivalence is expressed as a bijection between the two conditions.
CategoryTheory.Limits.isIso_of_source_target_iso_zero theorem
{X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) : IsIso f
Full source 
theorem isIso_of_source_target_iso_zero {X Y : C} (f : X ⟶ Y) (i : X ≅ 0) (j : Y ≅ 0) :
    IsIso f := by
  rw [zero_of_source_iso_zero f i]
  exact (isIsoZeroEquivIsoZero _ _).invFun ⟨i, j⟩
Morphism between Zero-Isomorphic Objects is an Isomorphism
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if there exist isomorphisms $i : X \cong 0$ and $j : Y \cong 0$ where $0$ is the zero object, then any morphism $f : X \to Y$ is an isomorphism.
CategoryTheory.Limits.isIsoZeroSelfEquivIsoZero definition
(X : C) : IsIso (0 : X ⟶ X) ≃ (X ≅ 0)
Full source 
/-- A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
`X` is isomorphic to the zero object.
-/
def isIsoZeroSelfEquivIsoZero (X : C) : IsIsoIsIso (0 : X ⟶ X) ≃ (X ≅ 0) :=
  (isIsoZeroEquivIsoZero X X).trans subsingletonProdSelfEquiv
Isomorphism condition for zero endomorphism via zero object isomorphism
Informal description
For any object \( X \) in a category \( C \) with zero morphisms, the zero endomorphism \( 0 : X \to X \) is an isomorphism if and only if \( X \) is isomorphic to the zero object. This equivalence is expressed as a bijection between the two conditions.
CategoryTheory.Limits.hasZeroObject_of_hasInitial_object theorem
[HasZeroMorphisms C] [HasInitial C] : HasZeroObject C
Full source 
/-- If there are zero morphisms, any initial object is a zero object. -/
theorem hasZeroObject_of_hasInitial_object [HasZeroMorphisms C] [HasInitial C] :
    HasZeroObject C := by
  refine ⟨⟨⊥_ C, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩⟩⟩
  calc
    f = f ≫ 𝟙 _ := (Category.comp_id _).symm
    _ = f ≫ 0 := by congr!; subsingleton
    _ = 0 := HasZeroMorphisms.comp_zero _ _
Initial Object is Zero Object in Category with Zero Morphisms
Informal description
If a category $C$ has zero morphisms and an initial object, then $C$ has a zero object.
CategoryTheory.Limits.hasZeroObject_of_hasTerminal_object theorem
[HasZeroMorphisms C] [HasTerminal C] : HasZeroObject C
Full source 
/-- If there are zero morphisms, any terminal object is a zero object. -/
theorem hasZeroObject_of_hasTerminal_object [HasZeroMorphisms C] [HasTerminal C] :
    HasZeroObject C := by
  refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩⟩⟩
  calc
    f = 𝟙𝟙 _ ≫ f := (Category.id_comp _).symm
    _ = 0 ≫ f := by congr!; subsingleton
    _ = 0 := zero_comp
Terminal Object Implies Zero Object in Category with Zero Morphisms
Informal description
In a category $C$ with zero morphisms and a terminal object, $C$ has a zero object.
CategoryTheory.Limits.image_ι_comp_eq_zero theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f] [Epi (factorThruImage f)] (h : f ≫ g = 0) : image.ι f ≫ g = 0
Full source 
theorem image_ι_comp_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage f]
    [Epi (factorThruImage f)] (h : f ≫ g = 0) : image.ιimage.ι f ≫ g = 0 :=
  zero_of_epi_comp (factorThruImage f) <| by simp [h]
Image Inclusion Composed with Zero Yields Zero
Informal description
In a category $C$ with images and zero morphisms, for any objects $X, Y, Z$, morphisms $f : X \to Y$ and $g : Y \to Z$, if the composition $f \circ g$ is the zero morphism and the factorization through the image of $f$ is an epimorphism, then the composition of the image inclusion $\iota_f$ with $g$ is also the zero morphism, i.e., $\iota_f \circ g = 0$.
CategoryTheory.Limits.comp_factorThruImage_eq_zero theorem
{X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage g] (h : f ≫ g = 0) : f ≫ factorThruImage g = 0
Full source 
theorem comp_factorThruImage_eq_zero {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} [HasImage g]
    (h : f ≫ g = 0) : f ≫ factorThruImage g = 0 :=
  zero_of_comp_mono (image.ι g) <| by simp [h]
Factorization of Zero Composition Through Image Morphism
Informal description
In a category $C$ with zero morphisms, given objects $X, Y, Z$, a morphism $f : X \to Y$, and a morphism $g : Y \to Z$ that has an image factorization, if the composition $f \circ g$ is the zero morphism, then the composition $f \circ (\text{factorThruImage } g)$ is also the zero morphism.
CategoryTheory.Limits.monoFactorisationZero definition
(X Y : C) : MonoFactorisation (0 : X ⟶ Y)
Full source 
/-- The zero morphism has a `MonoFactorisation` through the zero object.
-/
@[simps]
def monoFactorisationZero (X Y : C) : MonoFactorisation (0 : X ⟶ Y) where
  I := 0
  m := 0
  e := 0
Mono-factorization of zero morphism through zero object
Informal description
For any objects \( X \) and \( Y \) in a category \( C \), the zero morphism \( 0 : X \to Y \) has a mono-factorization through the zero object, where the intermediate object \( I \) is the zero object, and both the morphism \( e : X \to I \) and the morphism \( m : I \to Y \) are zero morphisms.
CategoryTheory.Limits.imageFactorisationZero definition
(X Y : C) : ImageFactorisation (0 : X ⟶ Y)
Full source 
/-- The factorisation through the zero object is an image factorisation.
-/
def imageFactorisationZero (X Y : C) : ImageFactorisation (0 : X ⟶ Y) where
  F := monoFactorisationZero X Y
  isImage := { lift := fun _ => 0 }
Image factorization of zero morphism through zero object
Informal description
For any objects \( X \) and \( Y \) in a category \( C \), the zero morphism \( 0 : X \to Y \) has an image factorization through the zero object, where the intermediate object \( I \) is the zero object, and both the morphism \( e : X \to I \) and the morphism \( m : I \to Y \) are zero morphisms. The factorization is unique up to isomorphism, with the lifting morphism also being the zero morphism.
CategoryTheory.Limits.hasImage_zero instance
{X Y : C} : HasImage (0 : X ⟶ Y)
Full source 
instance hasImage_zero {X Y : C} : HasImage (0 : X ⟶ Y) :=
  HasImage.mk <| imageFactorisationZero _ _
Existence of Image for Zero Morphisms
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, the zero morphism $0 : X \to Y$ has an image.
CategoryTheory.Limits.imageZero' definition
{X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] : image f ≅ 0
Full source 
/-- The image of a morphism which is equal to zero is the zero object. -/
def imageZero' {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] : imageimage f ≅ 0 :=
  image.eqToIsoimage.eqToIso h ≪≫ imageZero
Image of zero morphism is zero object (variant)
Informal description
For any objects $X$ and $Y$ in a category $C$ with zero morphisms, if a morphism $f : X \to Y$ is equal to the zero morphism, then the image of $f$ is isomorphic to the zero object.
CategoryTheory.Limits.image.ι_zero theorem
{X Y : C} [HasImage (0 : X ⟶ Y)] : image.ι (0 : X ⟶ Y) = 0
Full source 
@[simp]
theorem image.ι_zero {X Y : C} [HasImage (0 : X ⟶ Y)] : image.ι (0 : X ⟶ Y) = 0 := by
  rw [← image.lift_fac (monoFactorisationZero X Y)]
  simp
Image Inclusion of Zero Morphism is Zero
Informal description
In a category $C$ with images, for any objects $X$ and $Y$, the image inclusion morphism $\iota$ of the zero morphism $0 : X \to Y$ is equal to the zero morphism, i.e., $\iota(0) = 0$.
CategoryTheory.Limits.image.ι_zero' theorem
[HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] : image.ι f = 0
Full source 
/-- If we know `f = 0`,
it requires a little work to conclude `image.ι f = 0`,
because `f = g` only implies `image f ≅ image g`.
-/
@[simp]
theorem image.ι_zero' [HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] :
    image.ι f = 0 := by
  rw [image.eq_fac h]
  simp
Image Inclusion of Zero Morphism is Zero (Equalizer Variant)
Informal description
In a category $C$ with equalizers, for any objects $X$ and $Y$ and morphism $f : X \to Y$ such that $f = 0$, the image inclusion morphism $\iota_f$ is equal to the zero morphism, i.e., $\iota_f = 0$.
CategoryTheory.Limits.isSplitMono_sigma_ι instance
{β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasColimit (Discrete.functor f)] (b : β) : IsSplitMono (Sigma.ι f b)
Full source 
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/
instance isSplitMono_sigma_ι {β : Type u'} [HasZeroMorphisms C] (f : β → C)
    [HasColimit (Discrete.functor f)] (b : β) : IsSplitMono (Sigma.ι f b) := by
  classical exact IsSplitMono.mk' { retraction := Sigma.desc <| Pi.single b (𝟙 _) }
Coprojections into Coproducts are Split Monomorphisms in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms, for any family of objects $(f_\beta)_{\beta \in \beta'}$ in $C$ that has a coproduct, the coprojection morphism $\iota_b : f_b \to \coprod_\beta f_\beta$ is a split monomorphism for each $b \in \beta'$.
CategoryTheory.Limits.isSplitEpi_pi_π instance
{β : Type u'} [HasZeroMorphisms C] (f : β → C) [HasLimit (Discrete.functor f)] (b : β) : IsSplitEpi (Pi.π f b)
Full source 
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/
instance isSplitEpi_pi_π {β : Type u'} [HasZeroMorphisms C] (f : β → C)
    [HasLimit (Discrete.functor f)] (b : β) : IsSplitEpi (Pi.π f b) := by
  classical exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }
Projections from Products are Split Epimorphisms in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms, for any family of objects $(f_\beta)_{\beta \in \beta'}$ in $C$ that has a product, the projection morphism $\pi_b : \prod_\beta f_\beta \to f_b$ is a split epimorphism for each $b \in \beta'$.
CategoryTheory.Limits.isSplitMono_coprod_inl instance
[HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] : IsSplitMono (coprod.inl : X ⟶ X ⨿ Y)
Full source 
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/
instance isSplitMono_coprod_inl [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] :
    IsSplitMono (coprod.inl : X ⟶ X ⨿ Y) :=
  IsSplitMono.mk' { retraction := coprod.desc (𝟙 X) 0 }
Coprojection as Split Monomorphism in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms and binary coproducts, the coprojection $\mathrm{coprod.inl} : X \to X \sqcup Y$ is a split monomorphism.
CategoryTheory.Limits.isSplitMono_coprod_inr instance
[HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] : IsSplitMono (coprod.inr : Y ⟶ X ⨿ Y)
Full source 
/-- In the presence of zero morphisms, coprojections into a coproduct are (split) monomorphisms. -/
instance isSplitMono_coprod_inr [HasZeroMorphisms C] {X Y : C} [HasColimit (pair X Y)] :
    IsSplitMono (coprod.inr : Y ⟶ X ⨿ Y) :=
  IsSplitMono.mk' { retraction := coprod.desc 0 (𝟙 Y) }
Coprojections are Split Monomorphisms in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms and binary coproducts, the coprojection $\mathrm{coprod.inr} : Y \to X \sqcup Y$ is a split monomorphism.
CategoryTheory.Limits.isSplitEpi_prod_fst instance
[HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] : IsSplitEpi (prod.fst : X ⨯ Y ⟶ X)
Full source 
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/
instance isSplitEpi_prod_fst [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] :
    IsSplitEpi (prod.fst : X ⨯ YX ⨯ Y ⟶ X) :=
  IsSplitEpi.mk' { section_ := prod.lift (𝟙 X) 0 }
First Projection is Split Epimorphism in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms and binary products, the first projection $\mathrm{fst} : X \times Y \to X$ is a split epimorphism.
CategoryTheory.Limits.isSplitEpi_prod_snd instance
[HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] : IsSplitEpi (prod.snd : X ⨯ Y ⟶ Y)
Full source 
/-- In the presence of zero morphisms, projections into a product are (split) epimorphisms. -/
instance isSplitEpi_prod_snd [HasZeroMorphisms C] {X Y : C} [HasLimit (pair X Y)] :
    IsSplitEpi (prod.snd : X ⨯ YX ⨯ Y ⟶ Y) :=
  IsSplitEpi.mk' { section_ := prod.lift 0 (𝟙 Y) }
Second Projection is Split Epimorphism in Categories with Zero Morphisms
Informal description
In a category $C$ with zero morphisms and binary products, the second projection $\mathrm{snd} : X \times Y \to Y$ is a split epimorphism.
CategoryTheory.Limits.IsLimit.ofIsZero definition
(c : Cone F) (hF : IsZero F) (hc : IsZero c.pt) : IsLimit c
Full source 
/-- If a functor `F` is zero, then any cone for `F` with a zero point is limit. -/
def IsLimit.ofIsZero (c : Cone F) (hF : IsZero F) (hc : IsZero c.pt) : IsLimit c where
  lift _ := 0
  fac _ j := (F.isZero_iff.1 hF j).eq_of_tgt _ _
  uniq _ _ _ := hc.eq_of_tgt _ _
Limit cone from zero objects
Informal description
Given a cone $c$ for a functor $F$ in a category, if both $F$ and the apex of $c$ are zero objects, then $c$ is a limit cone. Specifically, the unique morphism lifting any other cone to $c$ is the zero morphism, and the necessary commutativity and uniqueness conditions are satisfied by the properties of zero objects and zero morphisms.
CategoryTheory.Limits.IsColimit.ofIsZero definition
(c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) : IsColimit c
Full source 
/-- If a functor `F` is zero, then any cocone for `F` with a zero point is colimit. -/
def IsColimit.ofIsZero (c : Cocone F) (hF : IsZero F) (hc : IsZero c.pt) : IsColimit c where
  desc _ := 0
  fac _ j := (F.isZero_iff.1 hF j).eq_of_src _ _
  uniq _ _ _ := hc.eq_of_src _ _
Colimit cocone from zero objects
Informal description
Given a cocone \( c \) for a functor \( F \) in a category, if both \( F \) and the apex of \( c \) are zero objects, then \( c \) is a colimit cocone. Specifically, the unique morphism descending from any other cocone to \( c \) is the zero morphism, and the necessary commutativity and uniqueness conditions are satisfied by the properties of zero objects and zero morphisms.
CategoryTheory.Limits.IsLimit.isZero_pt theorem
{c : Cone F} (hc : IsLimit c) (hF : IsZero F) : IsZero c.pt
Full source 
lemma IsLimit.isZero_pt {c : Cone F} (hc : IsLimit c) (hF : IsZero F) : IsZero c.pt :=
  (isZero_zero C).of_iso (IsLimit.conePointUniqueUpToIso hc
    (IsLimit.ofIsZero (Cone.mk 0 0) hF (isZero_zero C)))
Apex of Limit Cone is Zero Object when Functor is Zero
Informal description
For any cone \( c \) of a functor \( F \) in a category, if \( F \) is a zero object and \( c \) is a limit cone, then the apex of \( c \) is also a zero object.
CategoryTheory.Limits.IsColimit.isZero_pt theorem
{c : Cocone F} (hc : IsColimit c) (hF : IsZero F) : IsZero c.pt
Full source 
lemma IsColimit.isZero_pt {c : Cocone F} (hc : IsColimit c) (hF : IsZero F) : IsZero c.pt :=
  (isZero_zero C).of_iso (IsColimit.coconePointUniqueUpToIso hc
    (IsColimit.ofIsZero (Cocone.mk 0 0) hF (isZero_zero C)))
Apex of Colimit Cocone is Zero Object when Functor is Zero
Informal description
For any cocone \( c \) of a functor \( F \) in a category, if \( F \) is a zero object and \( c \) is a colimit cocone, then the apex of \( c \) is also a zero object.
CategoryTheory.Limits.IsTerminal.isZero theorem
{X : C} (hX : IsTerminal X) : IsZero X
Full source 
lemma IsTerminal.isZero {X : C} (hX : IsTerminal X) : IsZero X := by
  rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext
Terminal Objects are Zero Objects
Informal description
If an object $X$ in a category $C$ is terminal, then $X$ is a zero object.
CategoryTheory.Limits.IsInitial.isZero theorem
{X : C} (hX : IsInitial X) : IsZero X
Full source 
lemma IsInitial.isZero {X : C} (hX : IsInitial X) : IsZero X := by
  rw [IsZero.iff_id_eq_zero]
  apply hX.hom_ext
Initial Objects are Zero Objects
Informal description
If an object $X$ in a category $C$ is initial, then $X$ is a zero object.
CategoryTheory.Limits.Pi.ι definition
(b : β) : f b ⟶ ∏ᶜ f
Full source 
/-- In the presence of 0-morphism we can define an inclusion morphism into any product. -/
def Pi.ι (b : β) : f b ⟶ ∏ᶜ f :=
  Pi.lift (Function.update (fun _ ↦ 0) b (𝟙 _))
Inclusion morphism into categorical product
Informal description
For each index $b$ in the indexing set $\beta$, the morphism $\iota_b : f(b) \to \prod^c f$ is defined as the inclusion of the $b$-th component into the categorical product $\prod^c f$ of the family of objects $f$. This is constructed using the universal property of the product, where $\iota_b$ is the unique morphism that is the identity on the $b$-th component and the zero morphism on all other components.
CategoryTheory.Limits.Pi.ι_π_eq_id theorem
(b : β) : Pi.ι f b ≫ Pi.π f b = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma Pi.ι_π_eq_id (b : β) : Pi.ιPi.ι f b ≫ Pi.π f b = 𝟙 _ := by
  simp [Pi.ι]
Identity Property of Product Inclusion and Projection Morphisms
Informal description
For any index $b$ in the indexing set $\beta$, the composition of the inclusion morphism $\iota_b : f(b) \to \prod^c f$ with the projection morphism $\pi_b : \prod^c f \to f(b)$ equals the identity morphism on $f(b)$, i.e., $\iota_b \circ \pi_b = \text{id}_{f(b)}$.
CategoryTheory.Limits.Pi.ι_π_of_ne theorem
{b c : β} (h : b ≠ c) : Pi.ι f b ≫ Pi.π f c = 0
Full source 
@[reassoc]
lemma Pi.ι_π_of_ne {b c : β} (h : b ≠ c) : Pi.ιPi.ι f b ≫ Pi.π f c = 0 := by
  simp [Pi.ι, Function.update_of_ne h.symm]
Composition of Product Inclusion and Projection Morphisms for Distinct Indices is Zero
Informal description
For any distinct indices $b$ and $c$ in the indexing set $\beta$, the composition of the inclusion morphism $\iota_b \colon f(b) \to \prod^c f$ with the projection morphism $\pi_c \colon \prod^c f \to f(c)$ is the zero morphism, i.e., $\iota_b \circ \pi_c = 0$.
CategoryTheory.Limits.Pi.ι_π theorem
(b c : β) : Pi.ι f b ≫ Pi.π f c = if h : b = c then eqToHom (congrArg f h) else 0
Full source 
@[reassoc]
lemma Pi.ι_π (b c : β) :
    Pi.ιPi.ι f b ≫ Pi.π f c = if h : b = c then eqToHom (congrArg f h) else 0 := by
  split_ifs with h
  · subst h; simp
  · simp [Pi.ι_π_of_ne f h]
Composition of Product Inclusion and Projection Morphisms: $\iota_b \circ \pi_c = \text{id}$ if $b = c$, $0$ otherwise
Informal description
For any indices $b$ and $c$ in the indexing set $\beta$, the composition of the inclusion morphism $\iota_b \colon f(b) \to \prod^c f$ with the projection morphism $\pi_c \colon \prod^c f \to f(c)$ is equal to the identity morphism $\text{id}_{f(b)}$ when $b = c$, and is the zero morphism otherwise. More precisely: \[ \iota_b \circ \pi_c = \begin{cases} \text{id}_{f(b)} & \text{if } b = c, \\ 0 & \text{if } b \neq c. \end{cases} \]
CategoryTheory.Limits.instMonoι_1 instance
(b : β) : Mono (Pi.ι f b)
Full source 
instance (b : β) : Mono (Pi.ι f b) where
  right_cancellation _ _ e := by simpa using congrArg (· ≫ Pi.π f b) e
Inclusion Morphisms into Products are Monomorphisms
Informal description
For each index $b$ in the indexing set $\beta$, the inclusion morphism $\iota_b \colon f(b) \to \prod^c f$ is a monomorphism. This means that $\iota_b$ is left-cancellative: for any two morphisms $g, h \colon X \to f(b)$, if $\iota_b \circ g = \iota_b \circ h$, then $g = h$.
CategoryTheory.Limits.Sigma.π definition
(b : β) : ∐ f ⟶ f b
Full source 
/-- In the presence of 0-morphisms we can define a projection morphism from any coproduct. -/
def Sigma.π (b : β) : ∐ f∐ f ⟶ f b :=
  Limits.Sigma.desc (Function.update (fun _ ↦ 0) b (𝟙 _))
Projection morphism from coproduct
Informal description
For each object \( b \) in the index type \( \beta \), the morphism \( \pi_b : \coprod f \to f(b) \) is defined as the projection from the coproduct \( \coprod f \) to the component \( f(b) \), where it acts as the identity on \( f(b) \) and as the zero morphism on all other components.
CategoryTheory.Limits.Sigma.ι_π_eq_id theorem
(b : β) : Sigma.ι f b ≫ Sigma.π f b = 𝟙 _
Full source 
@[reassoc (attr := simp)]
lemma Sigma.ι_π_eq_id (b : β) : Sigma.ιSigma.ι f b ≫ Sigma.π f b = 𝟙 _ := by
  simp [Sigma.π]
Identity Property of Inclusion and Projection Morphisms for Coproducts
Informal description
For any object $b$ in the index type $\beta$, the composition of the inclusion morphism $\iota_b \colon f(b) \to \coprod f$ with the projection morphism $\pi_b \colon \coprod f \to f(b)$ is equal to the identity morphism on $f(b)$, i.e., $\iota_b \circ \pi_b = \mathrm{id}_{f(b)}$.
CategoryTheory.Limits.Sigma.ι_π_of_ne theorem
{b c : β} (h : b ≠ c) : Sigma.ι f b ≫ Sigma.π f c = 0
Full source 
@[reassoc]
lemma Sigma.ι_π_of_ne {b c : β} (h : b ≠ c) : Sigma.ιSigma.ι f b ≫ Sigma.π f c = 0 := by
  simp [Sigma.π, Function.update_of_ne h]
Composition of Inclusion and Projection Morphisms for Distinct Indices is Zero
Informal description
For any distinct indices $b$ and $c$ in the index type $\beta$, the composition of the inclusion morphism $\iota_b : f(b) \to \coprod f$ with the projection morphism $\pi_c : \coprod f \to f(c)$ is the zero morphism, i.e., $\iota_b \circ \pi_c = 0$.
CategoryTheory.Limits.Sigma.ι_π theorem
(b c : β) : Sigma.ι f b ≫ Sigma.π f c = if h : b = c then eqToHom (congrArg f h) else 0
Full source 
@[reassoc]
theorem Sigma.ι_π (b c : β) :
    Sigma.ιSigma.ι f b ≫ Sigma.π f c = if h : b = c then eqToHom (congrArg f h) else 0 := by
  split_ifs with h
  · subst h; simp
  · simp [Sigma.ι_π_of_ne f h]
Composition of Inclusion and Projection Morphisms for Coproducts: $\iota_b \circ \pi_c = \mathrm{id}$ if $b = c$, $0$ otherwise
Informal description
For any objects $b$ and $c$ in the index type $\beta$, the composition of the inclusion morphism $\iota_b \colon f(b) \to \coprod f$ with the projection morphism $\pi_c \colon \coprod f \to f(c)$ is equal to the identity morphism $\mathrm{id}_{f(b)}$ if $b = c$, and the zero morphism otherwise. That is, \[ \iota_b \circ \pi_c = \begin{cases} \mathrm{id}_{f(b)} & \text{if } b = c, \\ 0 & \text{otherwise.} \end{cases} \]
CategoryTheory.Limits.instEpiπ instance
(b : β) : Epi (Sigma.π f b)
Full source 
instance (b : β) : Epi (Sigma.π f b) where
  left_cancellation _ _ e := by simpa using congrArg (Sigma.ιSigma.ι f b ≫ ·) e
Projection Morphisms from Coproducts are Epimorphisms
Informal description
For each object $b$ in the index type $\beta$, the projection morphism $\pi_b \colon \coprod f \to f(b)$ is an epimorphism.
CategoryTheory.Limits.prod.inl definition
: X ⟶ X ⨯ Y
Full source 
/-- If a category `C` has 0-morphisms, there is a canonical inclusion from the first component `X`
into any product of objects `X ⨯ Y`. -/
def prod.inl : X ⟶ X ⨯ Y :=
  prod.lift (𝟙 _) 0
Inclusion into product (left component)
Informal description
The morphism \( \text{inl} : X \to X \times Y \) is the canonical inclusion of the first component \( X \) into the product \( X \times Y \), defined as the lift of the identity morphism on \( X \) and the zero morphism from \( X \) to \( Y \).
CategoryTheory.Limits.prod.inr definition
: Y ⟶ X ⨯ Y
Full source 
/-- If a category `C` has 0-morphisms, there is a canonical inclusion from the second component `Y`
into any product of objects `X ⨯ Y`. -/
def prod.inr : Y ⟶ X ⨯ Y :=
  prod.lift 0 (𝟙 _)
Inclusion into product (right component)
Informal description
The morphism \( \text{inr} : Y \to X \times Y \) is the canonical inclusion of the second component \( Y \) into the product \( X \times Y \), defined as the lift of the zero morphism from \( Y \) to \( X \) and the identity morphism on \( Y \).
CategoryTheory.Limits.prod.inl_fst theorem
: prod.inl X Y ≫ prod.fst = 𝟙 X
Full source 
@[reassoc (attr := simp)]
lemma prod.inl_fst : prod.inlprod.inl X Y ≫ prod.fst = 𝟙 X := by
  simp [prod.inl]
Composition of Left Inclusion with First Projection Yields Identity
Informal description
In a category with zero morphisms, the composition of the left inclusion morphism $\text{inl} : X \to X \times Y$ with the first projection morphism $\text{fst} : X \times Y \to X$ equals the identity morphism on $X$, i.e., $\text{inl} \circ \text{fst} = \text{id}_X$.
CategoryTheory.Limits.prod.inl_snd theorem
: prod.inl X Y ≫ prod.snd = 0
Full source 
@[reassoc (attr := simp)]
lemma prod.inl_snd : prod.inlprod.inl X Y ≫ prod.snd = 0 := by
  simp [prod.inl]
Composition of Left Inclusion with Second Projection Yields Zero Morphism
Informal description
In a category with zero morphisms, the composition of the left inclusion morphism $\text{inl} : X \to X \times Y$ with the second projection morphism $\text{snd} : X \times Y \to Y$ equals the zero morphism from $X$ to $Y$, i.e., $\text{inl} \circ \text{snd} = 0_{X,Y}$.
CategoryTheory.Limits.prod.inr_fst theorem
: prod.inr X Y ≫ prod.fst = 0
Full source 
@[reassoc (attr := simp)]
lemma prod.inr_fst : prod.inrprod.inr X Y ≫ prod.fst = 0 := by
  simp [prod.inr]
Composition of Right Inclusion with First Projection Yields Zero Morphism
Informal description
In a category with zero morphisms, the composition of the right inclusion morphism $\text{inr} : Y \to X \times Y$ with the first projection morphism $\text{fst} : X \times Y \to X$ equals the zero morphism from $Y$ to $X$, i.e., $\text{inr} \circ \text{fst} = 0_{Y,X}$.
CategoryTheory.Limits.prod.inr_snd theorem
: prod.inr X Y ≫ prod.snd = 𝟙 Y
Full source 
@[reassoc (attr := simp)]
lemma prod.inr_snd : prod.inrprod.inr X Y ≫ prod.snd = 𝟙 Y := by
  simp [prod.inr]
Right inclusion composed with second projection yields identity
Informal description
In a category with zero morphisms, the composition of the right inclusion morphism $\text{inr} : Y \to X \times Y$ with the second projection morphism $\text{snd} : X \times Y \to Y$ equals the identity morphism on $Y$, i.e., $\text{inr} \circ \text{snd} = \text{id}_Y$.
CategoryTheory.Limits.instMonoInl instance
: Mono (prod.inl X Y)
Full source 
instance : Mono (prod.inl X Y) where
  right_cancellation _ _ e := by simpa using congrArg (· ≫ prod.fst) e
Left Inclusion into Product is Mono
Informal description
The left inclusion morphism $\text{inl} : X \to X \times Y$ in a category with zero morphisms is a monomorphism.
CategoryTheory.Limits.instMonoInr instance
: Mono (prod.inr X Y)
Full source 
instance : Mono (prod.inr X Y) where
  right_cancellation _ _ e := by simpa using congrArg (· ≫ prod.snd) e
Right Inclusion into Product is a Monomorphism
Informal description
In a category with zero morphisms, the right inclusion morphism $\text{inr} : Y \to X \times Y$ is a monomorphism.
CategoryTheory.Limits.coprod.fst definition
: X ⨿ Y ⟶ X
Full source 
/-- If a category `C` has 0-morphisms, there is a canonical projection from a coproduct `X ⨿ Y` to
its first component `X`. -/
def coprod.fst : X ⨿ YX ⨿ Y ⟶ X :=
  coprod.desc (𝟙 _) 0
First projection from coproduct
Informal description
The morphism $\text{coprod.fst} : X \amalg Y \to X$ is the canonical projection from the coproduct $X \amalg Y$ to its first component $X$, defined as the coproduct universal property applied to the identity morphism $\text{id}_X : X \to X$ and the zero morphism $0 : Y \to X$.
CategoryTheory.Limits.coprod.snd definition
: X ⨿ Y ⟶ Y
Full source 
/-- If a category `C` has 0-morphisms, there is a canonical projection from a coproduct `X ⨿ Y` to
its second component `Y`. -/
def coprod.snd : X ⨿ YX ⨿ Y ⟶ Y :=
  coprod.desc 0 (𝟙 _)
Second projection from coproduct
Informal description
The morphism $\text{coprod.snd} : X \amalg Y \to Y$ is the canonical projection from the coproduct $X \amalg Y$ to its second component $Y$, defined as the coproduct universal property applied to the zero morphism $0 : X \to Y$ and the identity morphism $\text{id}_Y : Y \to Y$.
CategoryTheory.Limits.coprod.inl_fst theorem
: coprod.inl ≫ coprod.fst X Y = 𝟙 X
Full source 
@[reassoc (attr := simp)]
lemma coprod.inl_fst : coprod.inlcoprod.inl ≫ coprod.fst X Y = 𝟙 X := by
  simp [coprod.fst]
Composition of coproduct inclusion and first projection equals identity
Informal description
In a category with zero morphisms, the composition of the coproduct inclusion $\text{coprod.inl} : X \to X \amalg Y$ with the first projection $\text{coprod.fst} : X \amalg Y \to X$ equals the identity morphism $\text{id}_X$ on $X$, i.e., $\text{coprod.inl} \circ \text{coprod.fst} = \text{id}_X$.
CategoryTheory.Limits.coprod.inr_fst theorem
: coprod.inr ≫ coprod.fst X Y = 0
Full source 
@[reassoc (attr := simp)]
lemma coprod.inr_fst : coprod.inrcoprod.inr ≫ coprod.fst X Y = 0 := by
  simp [coprod.fst]
Composition of Coproduct Inclusion and First Projection Yields Zero Morphism
Informal description
In a category with zero morphisms, the composition of the coproduct inclusion $\text{coprod.inr} : Y \to X \amalg Y$ with the first projection $\text{coprod.fst} : X \amalg Y \to X$ equals the zero morphism $0 : Y \to X$, i.e., $\text{coprod.inr} \circ \text{coprod.fst} = 0$.
CategoryTheory.Limits.coprod.inl_snd theorem
: coprod.inl ≫ coprod.snd X Y = 0
Full source 
@[reassoc (attr := simp)]
lemma coprod.inl_snd : coprod.inlcoprod.inl ≫ coprod.snd X Y = 0 := by
  simp [coprod.snd]
Composition of Coproduct Inclusion and Second Projection Yields Zero Morphism
Informal description
In a category with zero morphisms, the composition of the coproduct inclusion $\text{coprod.inl} : X \to X \amalg Y$ with the second projection $\text{coprod.snd} : X \amalg Y \to Y$ equals the zero morphism $0 : X \to Y$, i.e., $\text{coprod.inl} \circ \text{coprod.snd} = 0$.
CategoryTheory.Limits.coprod.inr_snd theorem
: coprod.inr ≫ coprod.snd X Y = 𝟙 Y
Full source 
@[reassoc (attr := simp)]
lemma coprod.inr_snd : coprod.inrcoprod.inr ≫ coprod.snd X Y = 𝟙 Y := by
  simp [coprod.snd]
Identity via Coproduct Inclusion and Second Projection
Informal description
In a category with zero morphisms, the composition of the coproduct inclusion $\text{coprod.inr} : Y \to X \amalg Y$ with the second projection $\text{coprod.snd} : X \amalg Y \to Y$ equals the identity morphism $\text{id}_Y : Y \to Y$, i.e., $\text{coprod.inr} \circ \text{coprod.snd} = \text{id}_Y$.
CategoryTheory.Limits.instEpiFst instance
: Epi (coprod.fst X Y)
Full source 
instance : Epi (coprod.fst X Y) where
  left_cancellation _ _ e := by simpa using congrArg (coprod.inlcoprod.inl ≫ ·) e
First Coproduct Projection is Epimorphic
Informal description
The first projection morphism $\text{coprod.fst} : X \amalg Y \to X$ from the coproduct is an epimorphism.
CategoryTheory.Limits.instEpiSnd instance
: Epi (coprod.snd X Y)
Full source 
instance : Epi (coprod.snd X Y) where
  left_cancellation _ _ e := by simpa using congrArg (coprod.inrcoprod.inr ≫ ·) e
Second Coproduct Projection is Epimorphic
Informal description
The second projection morphism $\text{coprod.snd} : X \amalg Y \to Y$ from the coproduct is an epimorphism.