Mathlib.CategoryTheory.Limits.Shapes.Kernels

CategoryTheory.Limits.HasKernel abbrev

{X Y : C} (f : X ⟶ Y) : Prop

Full source

/-- A morphism `f` has a kernel if the functor `ParallelPair f 0` has a limit. -/
abbrev HasKernel {X Y : C} (f : X ⟶ Y) : Prop :=
  HasLimit (parallelPair f 0)

Existence of Kernel for a Morphism in a Category with Zero Morphisms

Informal description

A morphism $f : X \to Y$ in a category $\mathcal{C}$ with zero morphisms is said to *have a kernel* if the equalizer of $f$ and the zero morphism $0 : X \to Y$ exists. This means there exists an object $\text{kernel}(f)$ and a morphism $\iota : \text{kernel}(f) \to X$ such that $\iota \circ f = 0$, and $\text{kernel}(f)$ is universal with this property.

CategoryTheory.Limits.HasCokernel abbrev

{X Y : C} (f : X ⟶ Y) : Prop

Full source

/-- A morphism `f` has a cokernel if the functor `ParallelPair f 0` has a colimit. -/
abbrev HasCokernel {X Y : C} (f : X ⟶ Y) : Prop :=
  HasColimit (parallelPair f 0)

Existence of Cokernel for a Morphism in a Category with Zero Morphisms

Informal description

A morphism $f : X \to Y$ in a category with zero morphisms has a cokernel if the functor $\text{parallelPair}(f, 0)$ has a colimit. This means there exists a coequalizer of $f$ and the zero morphism $0 : X \to Y$.

CategoryTheory.Limits.KernelFork abbrev

Full source

/-- A kernel fork is just a fork where the second morphism is a zero morphism. -/
abbrev KernelFork :=
  Fork f 0

Kernel Fork as Equalizer of Morphism and Zero Morphism

Informal description

A *kernel fork* for a morphism $f : X \to Y$ in a category with zero morphisms is a fork where the second morphism is the zero morphism $0 : X \to Y$. That is, it consists of an object $K$ and a morphism $\iota : K \to X$ such that $\iota \circ f = 0$.

CategoryTheory.Limits.KernelFork.condition theorem

(s : KernelFork f) : Fork.ι s ≫ f = 0

Full source

@[reassoc (attr := simp)]
theorem KernelFork.condition (s : KernelFork f) : Fork.ιFork.ι s ≫ f = 0 := by
  rw [Fork.condition, HasZeroMorphisms.comp_zero]

Kernel Fork Condition: $\iota \circ f = 0$

Informal description

For any kernel fork $s$ of a morphism $f : X \to Y$ in a category with zero morphisms, the composition of the inclusion morphism $\iota_s$ with $f$ is the zero morphism, i.e., $\iota_s \circ f = 0$.

CategoryTheory.Limits.KernelFork.app_one theorem

(s : KernelFork f) : s.π.app one = 0

Full source

theorem KernelFork.app_one (s : KernelFork f) : s.π.app one = 0 := by
  simp [Fork.app_one_eq_ι_comp_right]

Kernel Fork Component at Terminal Object is Zero Morphism

Informal description

For any kernel fork $s$ of a morphism $f : X \to Y$ in a category with zero morphisms, the component of the cone $s.\pi$ at the terminal object of the walking parallel pair category is the zero morphism, i.e., $s.\pi(\text{one}) = 0$.

CategoryTheory.Limits.KernelFork.ofι abbrev

{Z : C} (ι : Z ⟶ X) (w : ι ≫ f = 0) : KernelFork f

Full source

/-- A morphism `ι` satisfying `ι ≫ f = 0` determines a kernel fork over `f`. -/
abbrev KernelFork.ofι {Z : C} (ι : Z ⟶ X) (w : ι ≫ f = 0) : KernelFork f :=
  Fork.ofι ι <| by rw [w, HasZeroMorphisms.comp_zero]

Construction of Kernel Fork from Morphism Satisfying Kernel Condition

Informal description

Given an object $Z$ in a category $\mathcal{C}$ with zero morphisms, and a morphism $\iota : Z \to X$ such that $\iota \circ f = 0$, the construction `KernelFork.ofι` produces a kernel fork for the morphism $f : X \to Y$. This fork has $Z$ as its vertex and $\iota$ as the morphism from $Z$ to $X$, satisfying the kernel condition $\iota \circ f = 0$.

CategoryTheory.Limits.KernelFork.ι_ofι theorem

{X Y P : C} (f : X ⟶ Y) (ι : P ⟶ X) (w : ι ≫ f = 0) : Fork.ι (KernelFork.ofι ι w) = ι

Full source

@[simp]
theorem KernelFork.ι_ofι {X Y P : C} (f : X ⟶ Y) (ι : P ⟶ X) (w : ι ≫ f = 0) :
    Fork.ι (KernelFork.ofι ι w) = ι := rfl

Inclusion Morphism of Kernel Fork Construction

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f : X \to Y$ be a morphism in $\mathcal{C}$. Given an object $P$ in $\mathcal{C}$ and a morphism $\iota : P \to X$ such that $\iota \circ f = 0$, the inclusion morphism $\iota$ of the kernel fork constructed via `KernelFork.ofι` is equal to $\iota$ itself. In other words, $\text{Fork.ι}(\text{KernelFork.ofι}\, \iota\, w) = \iota$.

CategoryTheory.Limits.isoOfι definition

(s : Fork f 0) : s ≅ Fork.ofι (Fork.ι s) (Fork.condition s)

Full source

/-- Every kernel fork `s` is isomorphic (actually, equal) to `fork.ofι (fork.ι s) _`. -/
def isoOfι (s : Fork f 0) : s ≅ Fork.ofι (Fork.ι s) (Fork.condition s) :=
  Cones.ext (Iso.refl _) <| by rintro ⟨j⟩ <;> simp

Isomorphism between a kernel fork and its canonical construction

Informal description

For any kernel fork $s$ of a morphism $f : X \to Y$ (i.e., a fork where $s.\iota \circ f = 0$), the fork $s$ is isomorphic to the fork constructed via `Fork.ofι` using the inclusion morphism $s.\iota$ and the kernel condition $s.\text{condition}$. More precisely, the isomorphism is given by the identity isomorphism on the vertex of the fork, and it commutes with the inclusion morphisms in the natural way.

CategoryTheory.Limits.ofιCongr definition

 {P : C} {ι ι' : P ⟶ X} {w : ι ≫ f = 0} (h : ι = ι') : KernelFork.ofι ι w ≅ KernelFork.ofι ι' (by rw [← h, w])

Full source

/-- If `ι = ι'`, then `fork.ofι ι _` and `fork.ofι ι' _` are isomorphic. -/
def ofιCongr {P : C} {ι ι' : P ⟶ X} {w : ι ≫ f = 0} (h : ι = ι') :
    KernelFork.ofιKernelFork.ofι ι w ≅ KernelFork.ofι ι' (by rw [← h, w]) :=
  Cones.ext (Iso.refl _)

Isomorphism of kernel forks from equal morphisms

Informal description

Given two morphisms $\iota, \iota' : P \to X$ in a category $\mathcal{C}$ with zero morphisms, both satisfying the kernel condition $\iota \circ f = 0$ (and $\iota' \circ f = 0$), if $\iota = \iota'$, then the kernel forks constructed from $\iota$ and $\iota'$ are isomorphic. More precisely, for any object $P$ and morphisms $\iota, \iota' : P \to X$ such that $\iota \circ f = 0$, if $\iota = \iota'$, then the kernel forks $\text{KernelFork.ofι} \, \iota \, w$ and $\text{KernelFork.ofι} \, \iota' \, w'$ (where $w'$ is derived from $w$ via the equality $\iota = \iota'$) are isomorphic via the identity isomorphism on $P$.

CategoryTheory.Limits.compNatIso definition

 {D : Type u'} [Category.{v} D] [HasZeroMorphisms D] (F : C ⥤ D) [F.IsEquivalence] :
  parallelPair f 0 ⋙ F ≅ parallelPair (F.map f) 0

Full source

/-- If `F` is an equivalence, then applying `F` to a diagram indexing a (co)kernel of `f` yields
    the diagram indexing the (co)kernel of `F.map f`. -/
def compNatIso {D : Type u'} [Category.{v} D] [HasZeroMorphisms D] (F : C ⥤ D) [F.IsEquivalence] :
    parallelPairparallelPair f 0 ⋙ FparallelPair f 0 ⋙ F ≅ parallelPair (F.map f) 0 :=
  let app (j : WalkingParallelPair) :
      (parallelPair f 0 ⋙ F).obj j ≅ (parallelPair (F.map f) 0).obj j :=
    match j with
    | zero => Iso.refl _
    | one => Iso.refl _
  NatIso.ofComponents app <| by rintro ⟨i⟩ ⟨j⟩ <;> intro g <;> cases g <;> simp [app]

Natural isomorphism between composed parallel pair functors under equivalence

Informal description

Given a category $\mathcal{D}$ with zero morphisms and an equivalence of categories $F \colon \mathcal{C} \to \mathcal{D}$, the composition of the parallel pair functor $(f, 0)$ with $F$ is naturally isomorphic to the parallel pair functor $(F(f), 0)$. More precisely, for any morphism $f \colon X \to Y$ in $\mathcal{C}$, there is a natural isomorphism between the functors: 1. $\text{parallelPair}(f, 0) \circ F \colon \text{WalkingParallelPair} \to \mathcal{D}$, and 2. $\text{parallelPair}(F(f), 0) \colon \text{WalkingParallelPair} \to \mathcal{D}$. This isomorphism is given componentwise by identity isomorphisms on the objects corresponding to the two objects of the walking parallel pair category.

CategoryTheory.Limits.KernelFork.IsLimit.lift' definition

{s : KernelFork f} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : { l : W ⟶ s.pt // l ≫ Fork.ι s = k }

Full source

/-- If `s` is a limit kernel fork and `k : W ⟶ X` satisfies `k ≫ f = 0`, then there is some
    `l : W ⟶ s.X` such that `l ≫ fork.ι s = k`. -/
def KernelFork.IsLimit.lift' {s : KernelFork f} (hs : IsLimit s) {W : C} (k : W ⟶ X)
    (h : k ≫ f = 0) : { l : W ⟶ s.pt // l ≫ Fork.ι s = k } :=
  ⟨hs.lift <| KernelFork.ofι _ h, hs.fac _ _⟩

Lift of a morphism to a limit kernel fork

Informal description

Given a limit kernel fork $ s $ for a morphism $ f : X \to Y $ in a category with zero morphisms, and a morphism $ k : W \to X $ such that $ k \circ f = 0 $, there exists a unique morphism $ l : W \to s.\text{pt} $ such that $ l \circ \iota_s = k $, where $ \iota_s $ is the inclusion morphism of the fork $ s $.

CategoryTheory.Limits.isLimitAux definition

 (t : KernelFork f) (lift : ∀ s : KernelFork f, s.pt ⟶ t.pt) (fac : ∀ s : KernelFork f, lift s ≫ t.ι = s.ι)
  (uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t

Full source

/-- This is a slightly more convenient method to verify that a kernel fork is a limit cone. It
    only asks for a proof of facts that carry any mathematical content -/
def isLimitAux (t : KernelFork f) (lift : ∀ s : KernelFork f, s.pt ⟶ t.pt)
    (fac : ∀ s : KernelFork f, lift s ≫ t.ι = s.ι)
    (uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt) (_ : m ≫ t.ι = s.ι), m = lift s) : IsLimit t :=
  { lift
    fac := fun s j => by
      cases j
      · exact fac s
      · simp
    uniq := fun s m w => uniq s m (w Limits.WalkingParallelPair.zero) }

Auxiliary construction for kernel limit cone

Informal description

Given a kernel fork $ t $ for a morphism $ f : X \to Y $ in a category with zero morphisms, a lifting function `lift` that constructs a morphism from any other kernel fork $ s $ to $ t $, a proof `fac` that these lifts commute with the fork morphisms, and a uniqueness condition `uniq` ensuring the lifts are unique, the function `isLimitAux` constructs a proof that $ t $ is a limit cone for the kernel diagram. More precisely, for any kernel fork $ t $, if: 1. For every kernel fork $ s $, there exists a morphism $ \text{lift}(s) : s.\text{pt} \to t.\text{pt} $ such that $ \text{lift}(s) \circ t.\iota = s.\iota $, and 2. For any morphism $ m : s.\text{pt} \to t.\text{pt} $ satisfying $ m \circ t.\iota = s.\iota $, we have $ m = \text{lift}(s) $, then $ t $ is a limit cone for the kernel diagram of $ f $.

CategoryTheory.Limits.KernelFork.IsLimit.ofι definition

 {W : C} (g : W ⟶ X) (eq : g ≫ f = 0) (lift : ∀ {W' : C} (g' : W' ⟶ X) (_ : g' ≫ f = 0), W' ⟶ W)
  (fac : ∀ {W' : C} (g' : W' ⟶ X) (eq' : g' ≫ f = 0), lift g' eq' ≫ g = g')
  (uniq : ∀ {W' : C} (g' : W' ⟶ X) (eq' : g' ≫ f = 0) (m : W' ⟶ W) (_ : m ≫ g = g'), m = lift g' eq') :
  IsLimit (KernelFork.ofι g eq)

Full source

/-- This is a more convenient formulation to show that a `KernelFork` constructed using
`KernelFork.ofι` is a limit cone.
-/
def KernelFork.IsLimit.ofι {W : C} (g : W ⟶ X) (eq : g ≫ f = 0)
    (lift : ∀ {W' : C} (g' : W' ⟶ X) (_ : g' ≫ f = 0), W' ⟶ W)
    (fac : ∀ {W' : C} (g' : W' ⟶ X) (eq' : g' ≫ f = 0), lift g' eq' ≫ g = g')
    (uniq :
      ∀ {W' : C} (g' : W' ⟶ X) (eq' : g' ≫ f = 0) (m : W' ⟶ W) (_ : m ≫ g = g'), m = lift g' eq') :
    IsLimit (KernelFork.ofι g eq) :=
  isLimitAux _ (fun s => lift s.ι s.condition) (fun s => fac s.ι s.condition) fun s =>
    uniq s.ι s.condition

Limit condition for kernel fork constructed from a morphism

Informal description

Given a morphism $ g : W \to X $ in a category $ C $ with zero morphisms, such that $ g \circ f = 0 $, and functions: 1. `lift`: For any morphism $ g' : W' \to X $ satisfying $ g' \circ f = 0 $, produces a morphism $ W' \to W $, 2. `fac`: Ensuring that for any such $ g' $, the composition $ \text{lift}(g') \circ g = g' $, 3. `uniq`: Guaranteeing uniqueness of the lift when $ m \circ g = g' $, then the kernel fork constructed from $ g $ and the equation $ g \circ f = 0 $ is a limit cone for the kernel diagram of $ f $.

CategoryTheory.Limits.KernelFork.IsLimit.ofι' definition

 {X Y K : C} {f : X ⟶ Y} (i : K ⟶ X) (w : i ≫ f = 0)
  (h : ∀ {A : C} (k : A ⟶ X) (_ : k ≫ f = 0), { l : A ⟶ K // l ≫ i = k }) [hi : Mono i] : IsLimit (KernelFork.ofι i w)

Full source

/-- This is a more convenient formulation to show that a `KernelFork` of the form
`KernelFork.ofι i _` is a limit cone when we know that `i` is a monomorphism. -/
def KernelFork.IsLimit.ofι' {X Y K : C} {f : X ⟶ Y} (i : K ⟶ X) (w : i ≫ f = 0)
    (h : ∀ {A : C} (k : A ⟶ X) (_ : k ≫ f = 0), { l : A ⟶ K // l ≫ i = k}) [hi : Mono i] :
    IsLimit (KernelFork.ofι i w) :=
  ofι _ _ (fun {_} k hk => (h k hk).1) (fun {_} k hk => (h k hk).2) (fun {A} k hk m hm => by
    rw [← cancel_mono i, (h k hk).2, hm])

Limit condition for kernel fork with monomorphic inclusion

Informal description

Given a morphism $ i : K \to X $ in a category $ C $ with zero morphisms, such that $ i \circ f = 0 $, and a function $ h $ that for any morphism $ k : A \to X $ satisfying $ k \circ f = 0 $ produces a morphism $ l : A \to K $ with $ l \circ i = k $, if $ i $ is a monomorphism, then the kernel fork constructed from $ i $ and the equation $ i \circ f = 0 $ is a limit cone for the kernel diagram of $ f $.

CategoryTheory.Limits.isKernelCompMono definition

 {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z} (hh : h = f ≫ g) :
  IsLimit (KernelFork.ofι c.ι (by simp [hh]) : KernelFork h)

Full source

/-- Every kernel of `f` induces a kernel of `f ≫ g` if `g` is mono. -/
def isKernelCompMono {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z}
    (hh : h = f ≫ g) : IsLimit (KernelFork.ofι c.ι (by simp [hh]) : KernelFork h) :=
  Fork.IsLimit.mk' _ fun s =>
    let s' : KernelFork f := Fork.ofι s.ι (by rw [← cancel_mono g]; simp [← hh, s.condition])
    let l := KernelFork.IsLimit.lift' i s'.ι s'.condition
    ⟨l.1, l.2, fun hm => by
      apply Fork.IsLimit.hom_ext i; rw [Fork.ι_ofι] at hm; rw [hm]; exact l.2.symm⟩

Limit kernel fork of a composition with a monomorphism

Informal description

Given a limit kernel fork $ c $ for a morphism $ f : X \to Y $ in a category with zero morphisms, and a monomorphism $ g : Y \to Z $, the kernel fork of the composition $ h = f \circ g $ is also a limit cone, with the same inclusion morphism $ \iota : c.\text{pt} \to X $ as $ c $. Specifically, the fork $ \text{KernelFork.ofι} \, c.\iota \, \text{(by simp [hh])} $ is a limit cone for $ h $, where $ hh $ is the equality $ h = f \circ g $.

CategoryTheory.Limits.isKernelCompMono_lift theorem

 {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z} (hh : h = f ≫ g) (s : KernelFork h) :
  (isKernelCompMono i g hh).lift s =
    i.lift
      (Fork.ofι s.ι
        (by
          rw [← cancel_mono g, Category.assoc, ← hh]
          simp))

Full source

theorem isKernelCompMono_lift {c : KernelFork f} (i : IsLimit c) {Z} (g : Y ⟶ Z) [hg : Mono g]
    {h : X ⟶ Z} (hh : h = f ≫ g) (s : KernelFork h) :
    (isKernelCompMono i g hh).lift s = i.lift (Fork.ofι s.ι (by
      rw [← cancel_mono g, Category.assoc, ← hh]
      simp)) := rfl

Lift Formula for Kernel of Composition with Monomorphism

Informal description

Let $f \colon X \to Y$ be a morphism in a category with zero morphisms, and let $c$ be a kernel fork of $f$ that is a limit cone. Given a monomorphism $g \colon Y \to Z$ and defining $h = f \circ g \colon X \to Z$, for any kernel fork $s$ of $h$, the lift of $s$ to the limit cone of the kernel of $h$ (constructed via `isKernelCompMono`) equals the lift of the fork $\text{Fork.ofι } s.\iota \text{ (by ...)}$ to the original limit cone $c$. More precisely, the following equality holds: $$(\text{isKernelCompMono } i \, g \, hh).\text{lift } s = i.\text{lift } (\text{Fork.ofι } s.\iota \text{ (by ...)})$$ where the proof term inside the fork construction verifies that $s.\iota \circ f = 0$ using the monomorphism property of $g$ and the equality $h = f \circ g$.

CategoryTheory.Limits.isKernelOfComp definition

 {W : C} (g : Y ⟶ W) (h : X ⟶ W) {c : KernelFork h} (i : IsLimit c) (hf : c.ι ≫ f = 0) (hfg : f ≫ g = h) :
  IsLimit (KernelFork.ofι c.ι hf)

Full source

/-- Every kernel of `f ≫ g` is also a kernel of `f`, as long as `c.ι ≫ f` vanishes. -/
def isKernelOfComp {W : C} (g : Y ⟶ W) (h : X ⟶ W) {c : KernelFork h} (i : IsLimit c)
    (hf : c.ι ≫ f = 0) (hfg : f ≫ g = h) : IsLimit (KernelFork.ofι c.ι hf) :=
  Fork.IsLimit.mk _ (fun s => i.lift (KernelFork.ofι s.ι (by simp [← hfg])))
    (fun s => by simp only [KernelFork.ι_ofι, Fork.IsLimit.lift_ι]) fun s m h => by
    apply Fork.IsLimit.hom_ext i; simpa using h

Kernel of a composition is a kernel of the first map under annihilation condition

Informal description

Given a morphism $ f : X \to Y $ and a morphism $ g : Y \to W $ in a category $ C $ with zero morphisms, suppose $ h = f \circ g : X \to W $. Let $ c $ be a kernel fork of $ h $ that is a limit cone, and suppose the inclusion morphism $ \iota : c.\text{pt} \to X $ satisfies $ \iota \circ f = 0 $. Then $ c $ is also a limit cone for the kernel fork of $ f $. In other words, if $ c $ is a kernel of $ h = f \circ g $ and $ \iota $ annihilates $ f $, then $ c $ is a kernel of $ f $.

CategoryTheory.Limits.KernelFork.IsLimit.ofId definition

{X Y : C} (f : X ⟶ Y) (hf : f = 0) : IsLimit (KernelFork.ofι (𝟙 X) (show 𝟙 X ≫ f = 0 by rw [hf, comp_zero]))

Full source

/-- `X` identifies to the kernel of a zero map `X ⟶ Y`. -/
def KernelFork.IsLimit.ofId {X Y : C} (f : X ⟶ Y) (hf : f = 0) :
    IsLimit (KernelFork.ofι (𝟙 X) (show 𝟙𝟙 X ≫ f = 0 by rw [hf, comp_zero])) :=
  KernelFork.IsLimit.ofι _ _ (fun x _ => x) (fun _ _ => Category.comp_id _)
    (fun _ _ _ hb => by simp only [← hb, Category.comp_id])

Limit cone for kernel of zero morphism via identity

Informal description

Given a zero morphism $ f = 0 \colon X \to Y $ in a category with zero morphisms, the identity morphism $ \mathrm{id}_X \colon X \to X $ makes $ X $ a limit cone for the kernel of $ f $. Specifically, the kernel fork constructed with $ \mathrm{id}_X $ satisfies the universal property of the kernel of $ f $.

CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero definition

{X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hf : Mono f) (h : IsZero c.pt) : IsLimit c

Full source

/-- Any zero object identifies to the kernel of a given monomorphisms. -/
def KernelFork.IsLimit.ofMonoOfIsZero {X Y : C} {f : X ⟶ Y} (c : KernelFork f)
    (hf : Mono f) (h : IsZero c.pt) : IsLimit c :=
  isLimitAux _ (fun _ => 0) (fun s => by rw [zero_comp, ← cancel_mono f, zero_comp, s.condition])
    (fun _ _ _ => h.eq_of_tgt _ _)

Limit cone for kernel of monomorphism with zero domain

Informal description

Given a kernel fork $ c $ for a monomorphism $ f : X \to Y $ in a category with zero morphisms, if the object $ c.\text{pt} $ is a zero object, then $ c $ is a limit cone for the kernel diagram of $ f $. In other words, if $ f $ is a monomorphism and the domain of the kernel morphism $ c.\iota $ is a zero object, then $ c $ is a universal cone for the kernel of $ f $.

CategoryTheory.Limits.KernelFork.IsLimit.isIso_ι theorem

{X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) (hf : f = 0) : IsIso c.ι

Full source

lemma KernelFork.IsLimit.isIso_ι {X Y : C} {f : X ⟶ Y} (c : KernelFork f)
    (hc : IsLimit c) (hf : f = 0) : IsIso c.ι := by
  let e : c.pt ≅ X := IsLimit.conePointUniqueUpToIso hc
    (KernelFork.IsLimit.ofId (f : X ⟶ Y) hf)
  have eq : e.inv ≫ c.ι = 𝟙 X := Fork.IsLimit.lift_ι hc
  haveI : IsIso (e.inv ≫ c.ι) := by
    rw [eq]
    infer_instance
  exact IsIso.of_isIso_comp_left e.inv c.ι

Isomorphism Property of Kernel Inclusion for Zero Morphism

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f : X \to Y$ be a morphism in $\mathcal{C}$ such that $f = 0$. If $c$ is a kernel fork for $f$ and $c$ is a limit cone, then the inclusion morphism $\iota : c.\mathrm{pt} \to X$ is an isomorphism.

CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff definition

 {X Y : C} {g : X ⟶ Y} {c : KernelFork g} (hc : IsLimit c) {X' Y' : C} (g' : X' ⟶ Y') (e : X ≅ X')
  (iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0) :
  IsLimit (KernelFork.ofι (f := g') (c.ι ≫ e.hom) (by simp [← iff]))

Full source

/-- If `c` is a limit kernel fork for `g : X ⟶ Y`, `e : X ≅ X'` and `g' : X' ⟶ Y` is a morphism,
then there is a limit kernel fork for `g'` with the same point as `c` if for any
morphism `φ : W ⟶ X`, there is an equivalence `φ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0`. -/
def KernelFork.isLimitOfIsLimitOfIff {X Y : C} {g : X ⟶ Y} {c : KernelFork g} (hc : IsLimit c)
    {X' Y' : C} (g' : X' ⟶ Y') (e : X ≅ X')
    (iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ gφ ≫ g = 0 ↔ φ ≫ e.hom ≫ g' = 0) :
    IsLimit (KernelFork.ofι (f := g') (c.ι ≫ e.hom) (by simp [← iff])) :=
  KernelFork.IsLimit.ofι _ _
    (fun s hs ↦ hc.lift (KernelFork.ofι (ι := s ≫ e.inv)
      (by rw [iff, Category.assoc, Iso.inv_hom_id_assoc, hs])))
    (fun s hs ↦ by simp [← cancel_mono e.inv])
    (fun s hs m hm ↦ Fork.IsLimit.hom_ext hc (by simpa [← cancel_mono e.hom] using hm))

Limit kernel fork under isomorphism and equivalent vanishing conditions

Informal description

Given a limit kernel fork $ c $ for a morphism $ g : X \to Y $ in a category $ C $ with zero morphisms, an isomorphism $ e : X \cong X' $, and a morphism $ g' : X' \to Y' $, if for any morphism $ \varphi : W \to X $ the condition $ \varphi \circ g = 0 $ is equivalent to $ \varphi \circ e \circ g' = 0 $, then the kernel fork constructed from $ c.\iota \circ e $ is also a limit cone for $ g' $.

CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff' definition

 {X Y : C} {g : X ⟶ Y} {c : KernelFork g} (hc : IsLimit c) {Y' : C} (g' : X ⟶ Y')
  (iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ g = 0 ↔ φ ≫ g' = 0) : IsLimit (KernelFork.ofι (f := g') c.ι (by simp [← iff]))

Full source

/-- If `c` is a limit kernel fork for `g : X ⟶ Y`, and `g' : X ⟶ Y'` is a another morphism,
then there is a limit kernel fork for `g'` with the same point as `c` if for any
morphism `φ : W ⟶ X`, there is an equivalence `φ ≫ g = 0 ↔ φ ≫ g' = 0`. -/
def KernelFork.isLimitOfIsLimitOfIff' {X Y : C} {g : X ⟶ Y} {c : KernelFork g} (hc : IsLimit c)
    {Y' : C} (g' : X ⟶ Y')
    (iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), φ ≫ gφ ≫ g = 0 ↔ φ ≫ g' = 0) :
    IsLimit (KernelFork.ofι (f := g') c.ι (by simp [← iff])) :=
  IsLimit.ofIsoLimit (isLimitOfIsLimitOfIff hc g' (Iso.refl _) (by simpa using iff))
    (Fork.ext (Iso.refl _))

Limit kernel fork under equivalent vanishing conditions

Informal description

Given a limit kernel fork $ c $ for a morphism $ g : X \to Y $ in a category $ C $ with zero morphisms, and another morphism $ g' : X \to Y' $, if for any morphism $ \varphi : W \to X $ the condition $ \varphi \circ g = 0 $ is equivalent to $ \varphi \circ g' = 0 $, then the kernel fork constructed from $ c.\iota $ is also a limit cone for $ g' $.

CategoryTheory.Limits.KernelFork.mapOfIsLimit definition

(kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') : kf.pt ⟶ kf'.pt

Full source

/-- The morphism between points of kernel forks induced by a morphism
in the category of arrows. -/
def mapOfIsLimit (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf')
    (φ : Arrow.mkArrow.mk f ⟶ Arrow.mk f') : kf.pt ⟶ kf'.pt :=
  hf'.lift (KernelFork.ofι (kf.ι ≫ φ.left) (by simp))

Morphism between kernel forks induced by a morphism of arrows

Informal description

Given a kernel fork $ kf $ for a morphism $ f $ and another kernel fork $ kf' $ for a morphism $ f' $ that is a limit cone, the function `KernelFork.mapOfIsLimit` constructs a morphism from the vertex of $ kf $ to the vertex of $ kf' $ induced by a morphism $ \varphi $ between the arrows $ f $ and $ f' $. This morphism satisfies the condition that its composition with the inclusion morphism of $ kf' $ equals the composition of the inclusion morphism of $ kf $ with the left component of $ \varphi $.

CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι theorem

 (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') :
  kf.mapOfIsLimit hf' φ ≫ kf'.ι = kf.ι ≫ φ.left

Full source

@[reassoc (attr := simp)]
lemma mapOfIsLimit_ι (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf')
    (φ : Arrow.mkArrow.mk f ⟶ Arrow.mk f') :
    kf.mapOfIsLimit hf' φ ≫ kf'.ι = kf.ι ≫ φ.left :=
  hf'.fac _ _

Commutativity of Kernel Fork Morphism Induced by Arrow Map

Informal description

Given a kernel fork $kf$ for a morphism $f : X \to Y$ and another kernel fork $kf'$ for $f' : X' \to Y'$ that is a limit cone, the morphism $\text{mapOfIsLimit}(kf, hf', \varphi)$ induced by a morphism of arrows $\varphi : (f) \to (f')$ satisfies the commutativity condition: \[ \text{mapOfIsLimit}(kf, hf', \varphi) \circ \iota_{kf'} = \iota_{kf} \circ \varphi_{\text{left}} \] where $\iota_{kf}$ and $\iota_{kf'}$ are the inclusion morphisms of the respective forks, and $\varphi_{\text{left}}$ is the left component of $\varphi$.

CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit definition

 {kf : KernelFork f} {kf' : KernelFork f'} (hf : IsLimit kf) (hf' : IsLimit kf') (φ : Arrow.mk f ≅ Arrow.mk f') :
  kf.pt ≅ kf'.pt

Full source

/-- The isomorphism between points of limit kernel forks induced by an isomorphism
in the category of arrows. -/
@[simps]
def mapIsoOfIsLimit {kf : KernelFork f} {kf' : KernelFork f'}
    (hf : IsLimit kf) (hf' : IsLimit kf')
    (φ : Arrow.mkArrow.mk f ≅ Arrow.mk f') : kf.pt ≅ kf'.pt where
  hom := kf.mapOfIsLimit hf' φ.hom
  inv := kf'.mapOfIsLimit hf φ.inv
  hom_inv_id := Fork.IsLimit.hom_ext hf (by simp)
  inv_hom_id := Fork.IsLimit.hom_ext hf' (by simp)

Isomorphism between kernel vertices induced by an isomorphism of arrows

Informal description

Given two kernel forks $ kf $ and $ kf' $ for morphisms $ f $ and $ f' $ respectively, both of which are limit cones, and an isomorphism $ \varphi $ between the arrows $ f $ and $ f' $ in the arrow category, the function `KernelFork.mapIsoOfIsLimit` constructs an isomorphism between the vertices of $ kf $ and $ kf' $. This isomorphism is induced by the isomorphism $ \varphi $ and satisfies the naturality conditions with respect to the inclusion morphisms of the kernel forks.

CategoryTheory.Limits.kernel abbrev

(f : X ⟶ Y) [HasKernel f] : C

Full source

/-- The kernel of a morphism, expressed as the equalizer with the 0 morphism. -/
abbrev kernel (f : X ⟶ Y) [HasKernel f] : C :=
  equalizer f 0

Kernel of a Morphism in a Category with Zero Morphisms

Informal description

In a category $\mathcal{C}$ with zero morphisms, the kernel of a morphism $f : X \to Y$ is the equalizer of $f$ and the zero morphism $0 : X \to Y$. It consists of an object $\text{kernel}(f)$ equipped with a morphism $\iota : \text{kernel}(f) \to X$ satisfying $\iota \circ f = 0$, and is universal with this property.

CategoryTheory.Limits.kernel.ι abbrev

: kernel f ⟶ X

Full source

/-- The map from `kernel f` into the source of `f`. -/
abbrev kernel.ι : kernelkernel f ⟶ X :=
  equalizer.ι f 0

Inclusion Morphism from Kernel to Source Object

Informal description

In a category $\mathcal{C}$ with zero morphisms, given a morphism $f : X \to Y$ that has a kernel, the morphism $\iota : \text{kernel}(f) \to X$ is the canonical inclusion from the kernel object to the source object $X$, satisfying $\iota \circ f = 0$.

CategoryTheory.Limits.equalizer_as_kernel theorem

: equalizer.ι f 0 = kernel.ι f

Full source

@[simp]
theorem equalizer_as_kernel : equalizer.ι f 0 = kernel.ι f := rfl

Equalizer Inclusion as Kernel Inclusion

Informal description

In a category $\mathcal{C}$ with zero morphisms, the inclusion morphism $\iota$ of the equalizer of a morphism $f : X \to Y$ and the zero morphism $0 : X \to Y$ is equal to the kernel inclusion morphism of $f$, i.e., $\mathrm{equalizer}(f, 0).\iota = \mathrm{kernel}(f).\iota$.

CategoryTheory.Limits.kernel.condition theorem

: kernel.ι f ≫ f = 0

Full source

@[reassoc (attr := simp)]
theorem kernel.condition : kernel.ιkernel.ι f ≫ f = 0 :=
  KernelFork.condition _

Kernel Condition: $\iota \circ f = 0$

Informal description

For a morphism $f : X \to Y$ in a category with zero morphisms, the composition of the kernel inclusion $\iota : \mathrm{kernel}(f) \to X$ with $f$ is the zero morphism, i.e., $\iota \circ f = 0$.

CategoryTheory.Limits.kernelIsKernel definition

: IsLimit (Fork.ofι (kernel.ι f) ((kernel.condition f).trans comp_zero.symm))

Full source

/-- The kernel built from `kernel.ι f` is limiting. -/
def kernelIsKernel : IsLimit (Fork.ofι (kernel.ι f) ((kernel.condition f).trans comp_zero.symm)) :=
  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by simp))

Universal property of the kernel fork

Informal description

The fork constructed from the kernel inclusion morphism $\iota : \mathrm{kernel}(f) \to X$ and the condition $\iota \circ f = 0$ is a limit cone, meaning it satisfies the universal property of the kernel of $f$.

CategoryTheory.Limits.kernel.lift abbrev

{W : C} (k : W ⟶ X) (h : k ≫ f = 0) : W ⟶ kernel f

Full source

/-- Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through `kernel.ι f`
    via `kernel.lift : W ⟶ kernel f`. -/
abbrev kernel.lift {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : W ⟶ kernel f :=
  (kernelIsKernel f).lift (KernelFork.ofι k h)

Universal Property of Kernel: Factorization of Morphisms through Kernel

Informal description

Given a morphism $f : X \to Y$ in a category $\mathcal{C}$ with zero morphisms and a kernel of $f$, for any object $W$ and morphism $k : W \to X$ such that $k \circ f = 0$, there exists a unique morphism $\text{kernel.lift}(f, k, h) : W \to \text{kernel}(f)$ factoring $k$ through the kernel inclusion $\iota : \text{kernel}(f) \to X$.

CategoryTheory.Limits.kernel.lift_ι theorem

{W : C} (k : W ⟶ X) (h : k ≫ f = 0) : kernel.lift f k h ≫ kernel.ι f = k

Full source

@[reassoc (attr := simp)]
theorem kernel.lift_ι {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : kernel.liftkernel.lift f k h ≫ kernel.ι f = k :=
  (kernelIsKernel f).fac (KernelFork.ofι k h) WalkingParallelPair.zero

Factorization Property of Kernel Lift: $\text{kernel.lift}(f, k, h) \circ \iota = k$

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f : X \to Y$ be a morphism in $\mathcal{C}$ that has a kernel. For any object $W$ and morphism $k : W \to X$ such that $k \circ f = 0$, the composition of the kernel lift $\text{kernel.lift}(f, k, h) : W \to \text{kernel}(f)$ with the kernel inclusion $\iota : \text{kernel}(f) \to X$ equals $k$, i.e., $\text{kernel.lift}(f, k, h) \circ \iota = k$.

CategoryTheory.Limits.kernel.lift_zero theorem

{W : C} {h} : kernel.lift f (0 : W ⟶ X) h = 0

Full source

@[simp]
theorem kernel.lift_zero {W : C} {h} : kernel.lift f (0 : W ⟶ X) h = 0 := by
  ext; simp

Kernel Lift of Zero Morphism is Zero

Informal description

In a category $\mathcal{C}$ with zero morphisms, for any morphism $f : X \to Y$ that has a kernel and any object $W$, the kernel lift of the zero morphism $0 : W \to X$ is the zero morphism $0 : W \to \text{kernel}(f)$.

CategoryTheory.Limits.kernel.lift_mono instance

{W : C} (k : W ⟶ X) (h : k ≫ f = 0) [Mono k] : Mono (kernel.lift f k h)

Full source

instance kernel.lift_mono {W : C} (k : W ⟶ X) (h : k ≫ f = 0) [Mono k] : Mono (kernel.lift f k h) :=
  ⟨fun {Z} g g' w => by
    replace w := w =≫ kernel.ι f
    simp only [Category.assoc, kernel.lift_ι] at w
    exact (cancel_mono k).1 w⟩

Lifting a Monomorphism through a Kernel Preserves Monomorphisms

Informal description

In a category with zero morphisms, given a morphism $f \colon X \to Y$ with a kernel, and a monomorphism $k \colon W \to X$ such that $k \circ f = 0$, the induced morphism $\text{kernel.lift}(f, k, h) \colon W \to \text{kernel}(f)$ is also a monomorphism.

CategoryTheory.Limits.kernel.lift' definition

{W : C} (k : W ⟶ X) (h : k ≫ f = 0) : { l : W ⟶ kernel f // l ≫ kernel.ι f = k }

Full source

/-- Any morphism `k : W ⟶ X` satisfying `k ≫ f = 0` induces a morphism `l : W ⟶ kernel f` such that
    `l ≫ kernel.ι f = k`. -/
def kernel.lift' {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : { l : W ⟶ kernel f // l ≫ kernel.ι f = k } :=
  ⟨kernel.lift f k h, kernel.lift_ι _ _ _⟩

Factorization through kernel with proof

Informal description

Given a morphism $f : X \to Y$ in a category $\mathcal{C}$ with zero morphisms and a kernel of $f$, for any object $W$ and morphism $k : W \to X$ such that $k \circ f = 0$, there exists a morphism $l : W \to \text{kernel}(f)$ such that $l \circ \iota = k$, where $\iota : \text{kernel}(f) \to X$ is the kernel inclusion. This morphism $l$ is given by $\text{kernel.lift}(f, k, h)$ and satisfies the factorization property $\text{kernel.lift}(f, k, h) \circ \iota = k$.

CategoryTheory.Limits.kernel.map abbrev

 {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : f ≫ q = p ≫ f') : kernel f ⟶ kernel f'

Full source

/-- A commuting square induces a morphism of kernels. -/
abbrev kernel.map {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
    (w : f ≫ q = p ≫ f') : kernelkernel f ⟶ kernel f' :=
  kernel.lift f' (kernel.ιkernel.ι f ≫ p) (by simp [← w])

Induced Morphism on Kernels from a Commutative Square

Informal description

Given a commutative square in a category $\mathcal{C}$ with zero morphisms, where $f : X \to Y$ and $f' : X' \to Y'$ are morphisms with kernels, and $p : X \to X'$, $q : Y \to Y'$ are morphisms satisfying $f \circ q = p \circ f'$, there exists an induced morphism $\text{kernel}(f) \to \text{kernel}(f')$ between the kernels of $f$ and $f'$.

CategoryTheory.Limits.kernel.lift_map theorem

 {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel g] (w : f ≫ g = 0) (f' : X' ⟶ Y') (g' : Y' ⟶ Z') [HasKernel g']
  (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
  kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w'

Full source

/-- Given a commutative diagram
    X --f--> Y --g--> Z
    |        |        |
    |        |        |
    v        v        v
    X' -f'-> Y' -g'-> Z'
with horizontal arrows composing to zero,
then we obtain a commutative square
   X ---> kernel g
   |         |
   |         | kernel.map
   |         |
   v         v
   X' --> kernel g'
-/
theorem kernel.lift_map {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel g] (w : f ≫ g = 0)
    (f' : X' ⟶ Y') (g' : Y' ⟶ Z') [HasKernel g'] (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y')
    (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
    kernel.liftkernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w' := by
  ext; simp [h₁]

Commutativity of Kernel Lifts and Maps in a Double Commutative Diagram

Informal description

Consider a commutative diagram in a category $\mathcal{C}$ with zero morphisms: \[ \begin{CD} X @>{f}>> Y @>{g}>> Z \\ @V{p}VV @V{q}VV @V{r}VV \\ X' @>{f'}>> Y' @>{g'}>> Z' \end{CD} \] where the horizontal compositions satisfy $f \circ g = 0$ and $f' \circ g' = 0$, and the squares commute via $f \circ q = p \circ f'$ and $g \circ r = q \circ g'$. Then the following diagram commutes: \[ \mathrm{kernel}(g) \xrightarrow{\mathrm{kernel.map}(g, g', q, r, h_2)} \mathrm{kernel}(g') \] \[ \uparrow\mathrm{kernel.lift}(g, f, w) \quad \quad \uparrow\mathrm{kernel.lift}(g', f', w') \] \[ X \xrightarrow{p} X' \] That is, the composition $\mathrm{kernel.lift}(g, f, w) \circ \mathrm{kernel.map}(g, g', q, r, h_2)$ equals $p \circ \mathrm{kernel.lift}(g', f', w')$.

CategoryTheory.Limits.kernel.mapIso definition

 {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') : kernel f ≅ kernel f'

Full source

/-- A commuting square of isomorphisms induces an isomorphism of kernels. -/
@[simps]
def kernel.mapIso {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q : Y ≅ Y')
    (w : f ≫ q.hom = p.hom ≫ f') : kernelkernel f ≅ kernel f' where
  hom := kernel.map f f' p.hom q.hom w
  inv :=
    kernel.map f' f p.inv q.inv
      (by
        refine (cancel_mono q.hom).1 ?_
        simp [w])

Isomorphism of kernels induced by a commutative square of isomorphisms

Informal description

Given a commutative square of isomorphisms in a category $\mathcal{C}$ with zero morphisms, where $f : X \to Y$ and $f' : X' \to Y'$ are morphisms with kernels, and $p : X \cong X'$, $q : Y \cong Y'$ are isomorphisms satisfying $f \circ q = p \circ f'$, there exists an induced isomorphism $\text{kernel}(f) \cong \text{kernel}(f')$ between the kernels of $f$ and $f'$.

CategoryTheory.Limits.kernel.ι_zero_isIso instance

: IsIso (kernel.ι (0 : X ⟶ Y))

Full source

/-- Every kernel of the zero morphism is an isomorphism -/
instance kernel.ι_zero_isIso : IsIso (kernel.ι (0 : X ⟶ Y)) :=
  equalizer.ι_of_self _

Kernel Inclusion of Zero Morphism is an Isomorphism

Informal description

In a category with zero morphisms, the kernel inclusion morphism $\iota : \mathrm{kernel}(0) \to X$ of the zero morphism $0 : X \to Y$ is an isomorphism.

CategoryTheory.Limits.kernelZeroIsoSource definition

: kernel (0 : X ⟶ Y) ≅ X

Full source

/-- The kernel of a zero morphism is isomorphic to the source. -/
def kernelZeroIsoSource : kernelkernel (0 : X ⟶ Y) ≅ X :=
  equalizer.isoSourceOfSelf 0

Kernel of zero morphism is isomorphic to source

Informal description

In a category with zero morphisms, the kernel of the zero morphism $ 0 : X \to Y $ is isomorphic to the source object $ X $.

CategoryTheory.Limits.kernelZeroIsoSource_hom theorem

: kernelZeroIsoSource.hom = kernel.ι (0 : X ⟶ Y)

Full source

@[simp]
theorem kernelZeroIsoSource_hom : kernelZeroIsoSource.hom = kernel.ι (0 : X ⟶ Y) := rfl

Homomorphism of Kernel-Zero Isomorphism Equals Kernel Inclusion

Informal description

In a category with zero morphisms, the homomorphism component of the isomorphism `kernelZeroIsoSource` from the kernel of the zero morphism $0 : X \to Y$ to the source object $X$ is equal to the kernel inclusion morphism $\iota : \text{kernel}(0) \to X$.

CategoryTheory.Limits.kernelZeroIsoSource_inv theorem

: kernelZeroIsoSource.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp)

Full source

@[simp]
theorem kernelZeroIsoSource_inv :
    kernelZeroIsoSource.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) := by
  ext
  simp [kernelZeroIsoSource]

Inverse of Kernel-Zero Isomorphism via Identity Lift

Informal description

The inverse morphism of the isomorphism $\text{kernel}(0 : X \to Y) \cong X$ is given by the kernel lift of the identity morphism $\text{id}_X : X \to X$ (which trivially satisfies $\text{id}_X \circ 0 = 0$).

CategoryTheory.Limits.kernelIsoOfEq definition

{f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : kernel f ≅ kernel g

Full source

/-- If two morphisms are known to be equal, then their kernels are isomorphic. -/
def kernelIsoOfEq {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : kernelkernel f ≅ kernel g :=
  HasLimit.isoOfNatIso (by rw [h])

Isomorphism between kernels of equal morphisms

Informal description

Given two equal morphisms $ f, g : X \to Y $ in a category with zero morphisms, where both $ f $ and $ g $ have kernels, there is a canonical isomorphism between their kernel objects $ \text{kernel}(f) $ and $ \text{kernel}(g) $.

CategoryTheory.Limits.kernelIsoOfEq_refl theorem

{h : f = f} : kernelIsoOfEq h = Iso.refl (kernel f)

Full source

@[simp]
theorem kernelIsoOfEq_refl {h : f = f} : kernelIsoOfEq h = Iso.refl (kernel f) := by
  ext
  simp [kernelIsoOfEq]

Kernel Isomorphism Identity: $\text{kernelIsoOfEq}(h) = \text{id}_{\text{kernel}(f)}$ for $h : f = f$

Informal description

For any morphism $f : X \to Y$ in a category with zero morphisms, the isomorphism between the kernel of $f$ and itself, induced by the equality $f = f$, is equal to the identity isomorphism on $\text{kernel}(f)$.

CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι theorem

{f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f

Full source

@[reassoc (attr := simp)]
theorem kernelIsoOfEq_hom_comp_ι {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) :
    (kernelIsoOfEq h).hom ≫ kernel.ι g = kernel.ι f := by
  cases h; simp

Compatibility of Kernel Isomorphism with Kernel Inclusions: $(\text{kernelIsoOfEq}(h))_{\text{hom}} \circ \iota_g = \iota_f$

Informal description

Given two equal morphisms $f, g : X \to Y$ in a category with zero morphisms, where both $f$ and $g$ have kernels, the composition of the forward morphism of the kernel isomorphism $\text{kernelIsoOfEq}(h)$ with the kernel inclusion $\iota_g$ of $g$ equals the kernel inclusion $\iota_f$ of $f$. That is, $(\text{kernelIsoOfEq}(h))_{\text{hom}} \circ \iota_g = \iota_f$.

CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι theorem

{f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : (kernelIsoOfEq h).inv ≫ kernel.ι _ = kernel.ι _

Full source

@[reassoc (attr := simp)]
theorem kernelIsoOfEq_inv_comp_ι {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) :
    (kernelIsoOfEq h).inv ≫ kernel.ι _ = kernel.ι _ := by
  cases h; simp

Inverse Kernel Isomorphism Commutes with Kernel Inclusion: $(\text{kernelIsoOfEq}(h))^{-1} \circ \iota_g = \iota_f$

Informal description

Given two equal morphisms $f, g : X \to Y$ in a category with zero morphisms, where both $f$ and $g$ have kernels, the inverse of the canonical isomorphism $\text{kernelIsoOfEq}(h) : \text{kernel}(f) \cong \text{kernel}(g)$ satisfies the commutative diagram where post-composing with the kernel inclusion $\iota$ of $g$ equals the kernel inclusion $\iota$ of $f$.

CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom theorem

 {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he) :
  kernel.lift _ e he ≫ (kernelIsoOfEq h).hom = kernel.lift _ e (by simp [← h, he])

Full source

@[reassoc (attr := simp)]
theorem lift_comp_kernelIsoOfEq_hom {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g)
    (e : Z ⟶ X) (he) :
    kernel.liftkernel.lift _ e he ≫ (kernelIsoOfEq h).hom = kernel.lift _ e (by simp [← h, he]) := by
  cases h; simp

Compatibility of Kernel Lift with Kernel Isomorphism: $\text{kernel.lift}(f, e, he) \circ (\text{kernelIsoOfEq}(h))_{\text{hom}} = \text{kernel.lift}(g, e, he')$

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f, g : X \to Y$ be morphisms in $\mathcal{C}$ such that $f = g$. Suppose both $f$ and $g$ have kernels. For any object $Z$ and morphism $e : Z \to X$ satisfying $e \circ f = 0$, the composition of the kernel lift $\text{kernel.lift}(f, e, he)$ with the forward morphism of the kernel isomorphism $\text{kernelIsoOfEq}(h)$ equals the kernel lift $\text{kernel.lift}(g, e, he')$, where $he'$ is the condition $e \circ g = 0$ (which follows from $f = g$ and $he$).

CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv theorem

 {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he) :
  kernel.lift _ e he ≫ (kernelIsoOfEq h).inv = kernel.lift _ e (by simp [h, he])

Full source

@[reassoc (attr := simp)]
theorem lift_comp_kernelIsoOfEq_inv {Z} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g)
    (e : Z ⟶ X) (he) :
    kernel.liftkernel.lift _ e he ≫ (kernelIsoOfEq h).inv = kernel.lift _ e (by simp [h, he]) := by
  cases h; simp

Kernel Lift Commutes with Inverse Kernel Isomorphism for Equal Morphisms

Informal description

Let $f, g : X \to Y$ be morphisms in a category with zero morphisms, where both $f$ and $g$ have kernels. Given an equality $h : f = g$, an object $Z$, and a morphism $e : Z \to X$ such that $e \circ f = 0$, the composition of the kernel lift $\text{kernel.lift}(f, e, he)$ with the inverse of the kernel isomorphism $\text{kernelIsoOfEq}(h)$ equals the kernel lift $\text{kernel.lift}(g, e, he')$, where $he'$ is the proof that $e \circ g = 0$ obtained by rewriting $he$ using $h$.

CategoryTheory.Limits.kernelIsoOfEq_trans theorem

 {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g) (w₂ : g = h) :
  kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (w₁.trans w₂)

Full source

@[simp]
theorem kernelIsoOfEq_trans {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g)
    (w₂ : g = h) : kernelIsoOfEqkernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq (w₁.trans w₂) := by
  cases w₁; cases w₂; ext; simp [kernelIsoOfEq]

Composition of Kernel Isomorphisms for Equal Morphisms

Informal description

Given three morphisms $f, g, h \colon X \to Y$ in a category with zero morphisms, where $f$, $g$, and $h$ all have kernels, and given equalities $w_1 \colon f = g$ and $w_2 \colon g = h$, the composition of the isomorphisms $\text{kernelIsoOfEq}(w_1)$ and $\text{kernelIsoOfEq}(w_2)$ is equal to the isomorphism $\text{kernelIsoOfEq}(w_1 \circ w_2)$ between the kernel objects of $f$ and $h$.

CategoryTheory.Limits.kernel_not_epi_of_nonzero theorem

(w : f ≠ 0) : ¬Epi (kernel.ι f)

Full source

theorem kernel_not_epi_of_nonzero (w : f ≠ 0) : ¬Epi (kernel.ι f) := fun _ =>
  w (eq_zero_of_epi_kernel f)

Kernel inclusion is not epi for nonzero morphisms

Informal description

For any nonzero morphism $f : X \to Y$ in a category with zero morphisms, the kernel inclusion morphism $\iota : \text{kernel}(f) \to X$ is not an epimorphism.

CategoryTheory.Limits.kernel_not_iso_of_nonzero theorem

(w : f ≠ 0) : IsIso (kernel.ι f) → False

Full source

theorem kernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (kernel.ι f) → False := fun _ =>
  kernel_not_epi_of_nonzero w inferInstance

Nonzero morphisms have non-isomorphic kernel inclusions

Informal description

For any nonzero morphism $f \colon X \to Y$ in a category with zero morphisms, the kernel inclusion morphism $\iota \colon \ker(f) \to X$ cannot be an isomorphism.

CategoryTheory.Limits.hasKernel_comp_mono instance

{X Y Z : C} (f : X ⟶ Y) [HasKernel f] (g : Y ⟶ Z) [Mono g] : HasKernel (f ≫ g)

Full source

instance hasKernel_comp_mono {X Y Z : C} (f : X ⟶ Y) [HasKernel f] (g : Y ⟶ Z) [Mono g] :
    HasKernel (f ≫ g) :=
  ⟨⟨{   cone := _
        isLimit := isKernelCompMono (limit.isLimit _) g rfl }⟩⟩

Existence of Kernel for Composition with Monomorphism

Informal description

For any morphism $f : X \to Y$ in a category with zero morphisms that has a kernel, and any monomorphism $g : Y \to Z$, the composition $f \circ g$ also has a kernel.

CategoryTheory.Limits.kernelCompMono definition

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g] : kernel (f ≫ g) ≅ kernel f

Full source

/-- When `g` is a monomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.
-/
@[simps]
def kernelCompMono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g] :
    kernelkernel (f ≫ g) ≅ kernel f where
  hom :=
    kernel.lift _ (kernel.ι _)
      (by
        rw [← cancel_mono g]
        simp)
  inv := kernel.lift _ (kernel.ι _) (by simp)

Kernel of composition with monomorphism is isomorphic to kernel

Informal description

Given a morphism $ f : X \to Y $ in a category with zero morphisms that has a kernel, and a monomorphism $ g : Y \to Z $, the kernel of the composition $ f \circ g $ is isomorphic to the kernel of $ f $. More precisely, there exists an isomorphism $ \text{kernel}(f \circ g) \cong \text{kernel}(f) $ that commutes with the kernel inclusion morphisms.

CategoryTheory.Limits.hasKernel_iso_comp instance

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : HasKernel (f ≫ g)

Full source

instance hasKernel_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] :
    HasKernel (f ≫ g) where
  exists_limit :=
    ⟨{  cone := KernelFork.ofι (kernel.ι g ≫ inv f) (by simp)
        isLimit := isLimitAux _ (fun s => kernel.lift _ (s.ι ≫ f) (by simp))
            (by simp) fun s m w => by
          simp_rw [← w]
          symm
          apply equalizer.hom_ext
          simp }⟩

Existence of Kernel for Composition with Isomorphism

Informal description

For any morphism $f : X \to Y$ that is an isomorphism and any morphism $g : Y \to Z$ that has a kernel, the composition $f \circ g$ also has a kernel.

CategoryTheory.Limits.kernelIsIsoComp definition

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : kernel (f ≫ g) ≅ kernel g

Full source

/-- When `f` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `g`.
-/
@[simps]
def kernelIsIsoComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] :
    kernelkernel (f ≫ g) ≅ kernel g where
  hom := kernel.lift _ (kernel.ι _ ≫ f) (by simp)
  inv := kernel.lift _ (kernel.ι _ ≫ inv f) (by simp)

Kernel isomorphism for composition with isomorphism

Informal description

For any morphism $ f : X \to Y $ that is an isomorphism and any morphism $ g : Y \to Z $ that has a kernel, the kernel of the composition $ f \circ g $ is isomorphic to the kernel of $ g $. More precisely, there exists an isomorphism $ \text{kernel}(f \circ g) \cong \text{kernel}(g) $ where: - The forward morphism is given by the universal property of the kernel of $ f \circ g $, factoring $ \iota_g \circ f $ (where $ \iota_g $ is the kernel inclusion of $ g $) - The inverse morphism is given by factoring $ \iota_g \circ f^{-1} $ through the kernel of $ g $

CategoryTheory.Limits.kernel.congr definition

{X Y : C} (f g : X ⟶ Y) [HasKernel f] [HasKernel g] (h : f = g) : kernel f ≅ kernel g

Full source

/-- Equal maps have isomorphic kernels. -/
@[simps] def kernel.congr {X Y : C} (f g : X ⟶ Y) [HasKernel f] [HasKernel g]
    (h : f = g) : kernelkernel f ≅ kernel g where
  hom := kernel.lift _ (kernel.ι f) (by simp [← h])
  inv := kernel.lift _ (kernel.ι g) (by simp [h])

Isomorphism of kernels for equal morphisms

Informal description

Given two equal morphisms $ f, g : X \to Y $ in a category with zero morphisms, their kernels are isomorphic. Specifically, if $ f = g $, then there exists an isomorphism between $\text{kernel}(f)$ and $\text{kernel}(g)$.

CategoryTheory.Limits.kernel.zeroKernelFork definition

: KernelFork f

Full source

/-- The morphism from the zero object determines a cone on a kernel diagram -/
def kernel.zeroKernelFork : KernelFork f where
  pt := 0
  π := { app := fun _ => 0 }

Zero kernel fork

Informal description

The *zero kernel fork* for a morphism $ f : X \to Y $ in a category with zero morphisms is the kernel fork where the object is the zero object and the morphism $ \iota : 0 \to X $ is the zero morphism. This satisfies the kernel condition $ \iota \circ f = 0 $.

CategoryTheory.Limits.kernel.isLimitConeZeroCone definition

[Mono f] : IsLimit (kernel.zeroKernelFork f)

Full source

/-- The map from the zero object is a kernel of a monomorphism -/
def kernel.isLimitConeZeroCone [Mono f] : IsLimit (kernel.zeroKernelFork f) :=
  Fork.IsLimit.mk _ (fun _ => 0)
    (fun s => by
      rw [zero_comp]
      refine (zero_of_comp_mono f ?_).symm
      exact KernelFork.condition _)
    fun _ _ _ => zero_of_to_zero _

Zero kernel fork is limit for monomorphism

Informal description

In a category with zero morphisms and a zero object, if a morphism $ f : X \to Y $ is a monomorphism, then the zero kernel fork (where the object is the zero object and the morphism is the zero morphism) is a limit cone for the kernel of $ f $. This means that the kernel of a monomorphism is the zero object, and the unique morphism from any other kernel fork to this zero kernel fork is the zero morphism.

CategoryTheory.Limits.kernel.ofMono definition

[HasKernel f] [Mono f] : kernel f ≅ 0

Full source

/-- The kernel of a monomorphism is isomorphic to the zero object -/
def kernel.ofMono [HasKernel f] [Mono f] : kernelkernel f ≅ 0 :=
  Functor.mapIso (Cones.forget _) <|
    IsLimit.uniqueUpToIso (limit.isLimit (parallelPair f 0)) (kernel.isLimitConeZeroCone f)

Kernel of a monomorphism is zero object

Informal description

In a category with zero morphisms and a zero object, the kernel of a monomorphism $ f : X \to Y $ is isomorphic to the zero object. This isomorphism is constructed using the universal property of the kernel and the fact that the zero kernel fork is a limit cone for monomorphisms.

CategoryTheory.Limits.kernel.ι_of_mono theorem

[HasKernel f] [Mono f] : kernel.ι f = 0

Full source

/-- The kernel morphism of a monomorphism is a zero morphism -/
theorem kernel.ι_of_mono [HasKernel f] [Mono f] : kernel.ι f = 0 :=
  zero_of_source_iso_zero _ (kernel.ofMono f)

Kernel Inclusion of Monomorphism is Zero Morphism

Informal description

In a category with zero morphisms and a zero object, if a morphism $f : X \to Y$ is a monomorphism, then the kernel inclusion morphism $\iota : \text{kernel}(f) \to X$ is equal to the zero morphism, i.e., $\iota = 0$.

CategoryTheory.Limits.zeroKernelOfCancelZero definition

 {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X) (_ : g ≫ f = 0), g = 0) :
  IsLimit (KernelFork.ofι (0 : 0 ⟶ X) (show 0 ≫ f = 0 by simp))

Full source

/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `0 : 0 ⟶ X` is a kernel of `f`. -/
def zeroKernelOfCancelZero {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (Z : C) (g : Z ⟶ X) (_ : g ≫ f = 0), g = 0) :
    IsLimit (KernelFork.ofι (0 : 0 ⟶ X) (show 0 ≫ f = 0 by simp)) :=
  Fork.IsLimit.mk _ (fun _ => 0) (fun s => by rw [hf _ _ (KernelFork.condition s), zero_comp])
    fun s m _ => by dsimp; apply HasZeroObject.to_zero_ext

Zero morphism as kernel under cancellation condition

Informal description

Given a morphism $ f : X \to Y $ in a category $ C $ with zero morphisms and a zero object, if for every object $ Z $ and morphism $ g : Z \to X $ the condition $ g \circ f = 0 $ implies $ g = 0 $, then the zero morphism $ 0 : 0 \to X $ is a kernel of $ f $. Here, $ 0 $ denotes the zero object in $ C $.

CategoryTheory.Limits.IsKernel.ofCompIso definition

 {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : l ≫ i.hom = f) {s : KernelFork f} (hs : IsLimit s) :
  IsLimit (KernelFork.ofι (Fork.ι s) <| show Fork.ι s ≫ l = 0 by simp [← i.comp_inv_eq.2 h.symm])

Full source

/-- If `i` is an isomorphism such that `l ≫ i.hom = f`, any kernel of `f` is a kernel of `l`. -/
def IsKernel.ofCompIso {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : l ≫ i.hom = f) {s : KernelFork f}
    (hs : IsLimit s) :
    IsLimit
      (KernelFork.ofι (Fork.ι s) <| show Fork.ιFork.ι s ≫ l = 0 by simp [← i.comp_inv_eq.2 h.symm]) :=
  Fork.IsLimit.mk _ (fun s => hs.lift <| KernelFork.ofι (Fork.ι s) <| by simp [← h])
    (fun s => by simp) fun s m h => by
      apply Fork.IsLimit.hom_ext hs
      simpa using h

Kernel preservation under composition with isomorphism

Informal description

Given a morphism $f : X \to Y$ in a category $\mathcal{C}$ with zero morphisms, an isomorphism $i : Z \cong Y$, and a morphism $l : X \to Z$ such that $l \circ i = f$, if $s$ is a kernel fork of $f$ that is a limit cone, then the fork obtained by replacing $f$ with $l$ (using the same morphism $\iota_s$ from the vertex of $s$ to $X$) is also a limit cone. In other words, any kernel of $f$ is also a kernel of $l$ under these conditions.

CategoryTheory.Limits.kernel.ofCompIso definition

 [HasKernel f] {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : l ≫ i.hom = f) :
  IsLimit (KernelFork.ofι (kernel.ι f) <| show kernel.ι f ≫ l = 0 by simp [← i.comp_inv_eq.2 h.symm])

Full source

/-- If `i` is an isomorphism such that `l ≫ i.hom = f`, the kernel of `f` is a kernel of `l`. -/
def kernel.ofCompIso [HasKernel f] {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : l ≫ i.hom = f) :
    IsLimit
      (KernelFork.ofι (kernel.ι f) <| show kernel.ιkernel.ι f ≫ l = 0 by simp [← i.comp_inv_eq.2 h.symm]) :=
  IsKernel.ofCompIso f l i h <| limit.isLimit _

Kernel preservation under composition with isomorphism

Informal description

Given a morphism $f \colon X \to Y$ in a category $\mathcal{C}$ with zero morphisms, an isomorphism $i \colon Z \cong Y$, and a morphism $l \colon X \to Z$ such that $l \circ i = f$, if $f$ has a kernel, then the kernel of $f$ is also a kernel of $l$. Specifically, the kernel inclusion $\iota_f \colon \text{kernel}(f) \to X$ satisfies $\iota_f \circ l = 0$, and the fork formed by $\iota_f$ is a limit cone for $l$.

CategoryTheory.Limits.IsKernel.isoKernel definition

 {Z : C} (l : Z ⟶ X) {s : KernelFork f} (hs : IsLimit s) (i : Z ≅ s.pt) (h : i.hom ≫ Fork.ι s = l) :
  IsLimit (KernelFork.ofι l <| show l ≫ f = 0 by simp [← h])

Full source

/-- If `s` is any limit kernel cone over `f` and if `i` is an isomorphism such that
    `i.hom ≫ s.ι = l`, then `l` is a kernel of `f`. -/
def IsKernel.isoKernel {Z : C} (l : Z ⟶ X) {s : KernelFork f} (hs : IsLimit s) (i : Z ≅ s.pt)
    (h : i.hom ≫ Fork.ι s = l) : IsLimit (KernelFork.ofι l <| show l ≫ f = 0 by simp [← h]) :=
  IsLimit.ofIsoLimit hs <|
    Cones.ext i.symm fun j => by
      cases j
      · exact (Iso.eq_inv_comp i).2 h
      · dsimp; rw [← h]; simp

Limit cone transport for kernel along isomorphism

Informal description

Given an isomorphism $i \colon Z \cong s.\text{pt}$ between an object $Z$ and the vertex of a kernel fork $s$ for a morphism $f \colon X \to Y$, if the composition $i.\text{hom} \circ \iota_s = l$ holds, then the fork constructed from $l \colon Z \to X$ (satisfying $l \circ f = 0$) is also a limit cone. Here, $\iota_s \colon s.\text{pt} \to X$ is the inclusion morphism of the kernel fork $s$.

CategoryTheory.Limits.kernel.isoKernel definition

 [HasKernel f] {Z : C} (l : Z ⟶ X) (i : Z ≅ kernel f) (h : i.hom ≫ kernel.ι f = l) :
  IsLimit (@KernelFork.ofι _ _ _ _ _ f _ l <| by simp [← h])

Full source

/-- If `i` is an isomorphism such that `i.hom ≫ kernel.ι f = l`, then `l` is a kernel of `f`. -/
def kernel.isoKernel [HasKernel f] {Z : C} (l : Z ⟶ X) (i : Z ≅ kernel f)
    (h : i.hom ≫ kernel.ι f = l) :
    IsLimit (@KernelFork.ofι _ _ _ _ _ f _ l <| by simp [← h]) :=
  IsKernel.isoKernel f l (limit.isLimit _) i h

Limit cone transport for kernel along isomorphism

Informal description

Given a morphism $f : X \to Y$ in a category $\mathcal{C}$ with zero morphisms and a kernel for $f$, if there exists an isomorphism $i : Z \cong \text{kernel}(f)$ such that $i.\text{hom} \circ \iota = l$, where $\iota : \text{kernel}(f) \to X$ is the kernel inclusion, then the fork constructed from $l : Z \to X$ (satisfying $l \circ f = 0$) is also a limit cone for the kernel of $f$.

CategoryTheory.Limits.kernel.ι_of_zero theorem

: IsIso (kernel.ι (0 : X ⟶ Y))

Full source

/-- The kernel morphism of a zero morphism is an isomorphism -/
theorem kernel.ι_of_zero : IsIso (kernel.ι (0 : X ⟶ Y)) :=
  equalizer.ι_of_self _

Kernel inclusion of zero morphism is an isomorphism

Informal description

In a category with zero morphisms, the kernel inclusion morphism $\iota : \mathrm{kernel}(0) \to X$ of the zero morphism $0 : X \to Y$ is an isomorphism.

CategoryTheory.Limits.CokernelCofork abbrev

Full source

/-- A cokernel cofork is just a cofork where the second morphism is a zero morphism. -/
abbrev CokernelCofork :=
  Cofork f 0

Cokernel Cofork Construction via Zero Morphism

Informal description

A cokernel cofork for a morphism $f : X \to Y$ in a category with zero morphisms is a cofork where the second morphism is the zero morphism $0 : X \to Y$. Specifically, it consists of an object $Q$ and a morphism $\pi : Y \to Q$ such that $f \circ \pi = 0$.

CategoryTheory.Limits.CokernelCofork.condition theorem

(s : CokernelCofork f) : f ≫ s.π = 0

Full source

@[reassoc (attr := simp)]
theorem CokernelCofork.condition (s : CokernelCofork f) : f ≫ s.π = 0 := by
  rw [Cofork.condition, zero_comp]

Cokernel Cofork Condition: $f \circ \pi = 0$

Informal description

For any cokernel cofork $s$ of a morphism $f \colon X \to Y$ in a category with zero morphisms, the composition $f \circ s.\pi$ equals the zero morphism, i.e., $f \circ s.\pi = 0$.

CategoryTheory.Limits.CokernelCofork.π_eq_zero theorem

(s : CokernelCofork f) : s.ι.app zero = 0

Full source

theorem CokernelCofork.π_eq_zero (s : CokernelCofork f) : s.ι.app zero = 0 := by
  simp [Cofork.app_zero_eq_comp_π_right]

Cokernel Cofork Initial Component is Zero

Informal description

For any cokernel cofork $s$ of a morphism $f \colon X \to Y$ in a category with zero morphisms, the cocone's component at the initial object of the walking parallel pair category is the zero morphism, i.e., $s.\iota(\text{zero}) = 0$.

CategoryTheory.Limits.CokernelCofork.ofπ abbrev

{Z : C} (π : Y ⟶ Z) (w : f ≫ π = 0) : CokernelCofork f

Full source

/-- A morphism `π` satisfying `f ≫ π = 0` determines a cokernel cofork on `f`. -/
abbrev CokernelCofork.ofπ {Z : C} (π : Y ⟶ Z) (w : f ≫ π = 0) : CokernelCofork f :=
  Cofork.ofπ π <| by rw [w, zero_comp]

Construction of Cokernel Cofork from a Zero-Composing Morphism

Informal description

Given a morphism $f \colon X \to Y$ in a category with zero morphisms, and a morphism $\pi \colon Y \to Z$ such that $f \circ \pi = 0$, the construction `CokernelCofork.ofπ` produces a cokernel cofork for $f$ with object $Z$ and morphism $\pi$.

CategoryTheory.Limits.CokernelCofork.π_ofπ theorem

{X Y P : C} (f : X ⟶ Y) (π : Y ⟶ P) (w : f ≫ π = 0) : Cofork.π (CokernelCofork.ofπ π w) = π

Full source

@[simp]
theorem CokernelCofork.π_ofπ {X Y P : C} (f : X ⟶ Y) (π : Y ⟶ P) (w : f ≫ π = 0) :
    Cofork.π (CokernelCofork.ofπ π w) = π :=
  rfl

Projection of Cokernel Cofork Construction Equals Input Morphism

Informal description

Given a morphism $f \colon X \to Y$ and a morphism $\pi \colon Y \to P$ in a category with zero morphisms such that $f \circ \pi = 0$, the projection morphism of the cokernel cofork constructed via `CokernelCofork.ofπ` equals $\pi$. That is, $\text{Cofork.π}(\text{CokernelCofork.ofπ} \pi w) = \pi$.

CategoryTheory.Limits.isoOfπ definition

(s : Cofork f 0) : s ≅ Cofork.ofπ (Cofork.π s) (Cofork.condition s)

Full source

/-- Every cokernel cofork `s` is isomorphic (actually, equal) to `cofork.ofπ (cofork.π s) _`. -/
def isoOfπ (s : Cofork f 0) : s ≅ Cofork.ofπ (Cofork.π s) (Cofork.condition s) :=
  Cocones.ext (Iso.refl _) fun j => by cases j <;> aesop_cat

Isomorphism between a cofork and its canonical construction from projection

Informal description

For any cofork $s$ of a morphism $f \colon X \to Y$ and the zero morphism $0 \colon X \to Y$ in a category with zero morphisms, the cofork $s$ is isomorphic to the cofork constructed from its projection morphism $\pi_s \colon Y \to s.pt$ and the condition $f \circ \pi_s = 0$.

CategoryTheory.Limits.ofπCongr definition

 {P : C} {π π' : Y ⟶ P} {w : f ≫ π = 0} (h : π = π') : CokernelCofork.ofπ π w ≅ CokernelCofork.ofπ π' (by rw [← h, w])

Full source

/-- If `π = π'`, then `CokernelCofork.of_π π _` and `CokernelCofork.of_π π' _` are isomorphic. -/
def ofπCongr {P : C} {π π' : Y ⟶ P} {w : f ≫ π = 0} (h : π = π') :
    CokernelCofork.ofπCokernelCofork.ofπ π w ≅ CokernelCofork.ofπ π' (by rw [← h, w]) :=
  Cocones.ext (Iso.refl _) fun j => by cases j <;> aesop_cat

Isomorphism of cokernel coforks from equal morphisms

Informal description

Given a morphism $f \colon X \to Y$ in a category with zero morphisms, and two equal morphisms $\pi, \pi' \colon Y \to P$ such that $f \circ \pi = 0$ and $f \circ \pi' = 0$, the cokernel coforks constructed from $\pi$ and $\pi'$ are isomorphic. Specifically, if $\pi = \pi'$, then `CokernelCofork.ofπ π w` and `CokernelCofork.ofπ π' (by rw [← h, w])` are isomorphic via the identity isomorphism.

CategoryTheory.Limits.CokernelCofork.IsColimit.desc' definition

 {s : CokernelCofork f} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : { l : s.pt ⟶ W // Cofork.π s ≫ l = k }

Full source

/-- If `s` is a colimit cokernel cofork, then every `k : Y ⟶ W` satisfying `f ≫ k = 0` induces
    `l : s.X ⟶ W` such that `cofork.π s ≫ l = k`. -/
def CokernelCofork.IsColimit.desc' {s : CokernelCofork f} (hs : IsColimit s) {W : C} (k : Y ⟶ W)
    (h : f ≫ k = 0) : { l : s.pt ⟶ W // Cofork.π s ≫ l = k } :=
  ⟨hs.desc <| CokernelCofork.ofπ _ h, hs.fac _ _⟩

Universal property of cokernel cofork

Informal description

Given a cokernel cofork $ s $ for a morphism $ f : X \to Y $ in a category with zero morphisms, if $ s $ is a colimit, then for any morphism $ k : Y \to W $ satisfying $ f \circ k = 0 $, there exists a unique morphism $ l : s.pt \to W $ such that $ \pi_s \circ l = k $, where $ \pi_s $ is the projection morphism of the cofork $ s $.

CategoryTheory.Limits.isColimitAux definition

 (t : CokernelCofork f) (desc : ∀ s : CokernelCofork f, t.pt ⟶ s.pt) (fac : ∀ s : CokernelCofork f, t.π ≫ desc s = s.π)
  (uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt) (_ : t.π ≫ m = s.π), m = desc s) : IsColimit t

Full source

/-- This is a slightly more convenient method to verify that a cokernel cofork is a colimit cocone.
It only asks for a proof of facts that carry any mathematical content -/
def isColimitAux (t : CokernelCofork f) (desc : ∀ s : CokernelCofork f, t.pt ⟶ s.pt)
    (fac : ∀ s : CokernelCofork f, t.π ≫ desc s = s.π)
    (uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt) (_ : t.π ≫ m = s.π), m = desc s) :
    IsColimit t :=
  { desc
    fac := fun s j => by
      cases j
      · simp
      · exact fac s
    uniq := fun s m w => uniq s m (w Limits.WalkingParallelPair.one) }

Verification of cokernel cofork as colimit via universal property

Informal description

Given a cokernel cofork $ t $ for a morphism $ f : X \to Y $ in a category with zero morphisms, along with: - A function `desc` that for any other cokernel cofork $ s $ provides a morphism $ t.pt \to s.pt $, - A proof `fac` that for any $ s $, the composition $ t.\pi \circ \text{desc}(s) = s.\pi $, - A proof `uniq` that any morphism $ m : t.pt \to s.pt $ satisfying $ t.\pi \circ m = s.\pi $ must equal $ \text{desc}(s) $, then $ t $ is a colimit cokernel cofork for $ f $. This construction verifies the universal property of the cokernel.

CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ definition

 {Z : C} (g : Y ⟶ Z) (eq : f ≫ g = 0) (desc : ∀ {Z' : C} (g' : Y ⟶ Z') (_ : f ≫ g' = 0), Z ⟶ Z')
  (fac : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0), g ≫ desc g' eq' = g')
  (uniq : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0) (m : Z ⟶ Z') (_ : g ≫ m = g'), m = desc g' eq') :
  IsColimit (CokernelCofork.ofπ g eq)

Full source

/-- This is a more convenient formulation to show that a `CokernelCofork` constructed using
`CokernelCofork.ofπ` is a limit cone.
-/
def CokernelCofork.IsColimit.ofπ {Z : C} (g : Y ⟶ Z) (eq : f ≫ g = 0)
    (desc : ∀ {Z' : C} (g' : Y ⟶ Z') (_ : f ≫ g' = 0), Z ⟶ Z')
    (fac : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0), g ≫ desc g' eq' = g')
    (uniq :
      ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : f ≫ g' = 0) (m : Z ⟶ Z') (_ : g ≫ m = g'), m = desc g' eq') :
    IsColimit (CokernelCofork.ofπ g eq) :=
  isColimitAux _ (fun s => desc s.π s.condition) (fun s => fac s.π s.condition) fun s =>
    uniq s.π s.condition

Universal property verification for cokernel cofork

Informal description

Given a morphism $f \colon X \to Y$ in a category with zero morphisms, a morphism $g \colon Y \to Z$ satisfying $f \circ g = 0$, and functions: - `desc` that for any morphism $g' \colon Y \to Z'$ with $f \circ g' = 0$ provides a morphism $Z \to Z'$, - `fac` ensuring $g \circ \text{desc}(g') = g'$ for all such $g'$, - `uniq` guaranteeing any $m \colon Z \to Z'$ satisfying $g \circ m = g'$ must equal $\text{desc}(g')$, then the cokernel cofork constructed from $g$ (via `CokernelCofork.ofπ`) is a colimit. This verifies the universal property of the cokernel of $f$.

CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ' definition

 {X Y Q : C} {f : X ⟶ Y} (p : Y ⟶ Q) (w : f ≫ p = 0)
  (h : ∀ {A : C} (k : Y ⟶ A) (_ : f ≫ k = 0), { l : Q ⟶ A // p ≫ l = k }) [hp : Epi p] :
  IsColimit (CokernelCofork.ofπ p w)

Full source

/-- This is a more convenient formulation to show that a `CokernelCofork` of the form
`CokernelCofork.ofπ p _` is a colimit cocone when we know that `p` is an epimorphism. -/
def CokernelCofork.IsColimit.ofπ' {X Y Q : C} {f : X ⟶ Y} (p : Y ⟶ Q) (w : f ≫ p = 0)
    (h : ∀ {A : C} (k : Y ⟶ A) (_ : f ≫ k = 0), { l : Q ⟶ A // p ≫ l = k}) [hp : Epi p] :
    IsColimit (CokernelCofork.ofπ p w) :=
  ofπ _ _ (fun {_} k hk => (h k hk).1) (fun {_} k hk => (h k hk).2) (fun {A} k hk m hm => by
    rw [← cancel_epi p, (h k hk).2, hm])

Colimit cokernel cofork from an epimorphism

Informal description

Given a morphism $ f : X \to Y $ in a category with zero morphisms, a morphism $ p : Y \to Q $ satisfying $ f \circ p = 0 $, and a function $ h $ that for any morphism $ k : Y \to A $ with $ f \circ k = 0 $ provides a morphism $ l : Q \to A $ such that $ p \circ l = k $, if $ p $ is an epimorphism, then the cokernel cofork constructed from $ p $ is a colimit. This provides a convenient criterion to verify that a cokernel cofork is a colimit when the morphism $ p $ is epic.

CategoryTheory.Limits.isCokernelEpiComp definition

 {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g] {h : W ⟶ Y} (hh : h = g ≫ f) :
  IsColimit (CokernelCofork.ofπ c.π (by rw [hh]; simp) : CokernelCofork h)

Full source

/-- Every cokernel of `f` induces a cokernel of `g ≫ f` if `g` is epi. -/
def isCokernelEpiComp {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g]
    {h : W ⟶ Y} (hh : h = g ≫ f) :
    IsColimit (CokernelCofork.ofπ c.π (by rw [hh]; simp) : CokernelCofork h) :=
  Cofork.IsColimit.mk' _ fun s =>
    let s' : CokernelCofork f :=
      Cofork.ofπ s.π
        (by
          apply hg.left_cancellation
          rw [← Category.assoc, ← hh, s.condition]
          simp)
    let l := CokernelCofork.IsColimit.desc' i s'.π s'.condition
    ⟨l.1, l.2, fun hm => by
      apply Cofork.IsColimit.hom_ext i; rw [Cofork.π_ofπ] at hm; rw [hm]; exact l.2.symm⟩

Colimit property of cokernel under epimorphism composition

Informal description

Given a cokernel cofork $ c $ for a morphism $ f : X \to Y $ in a category with zero morphisms, if $ c $ is a colimit, then for any epimorphism $ g : W \to X $ and morphism $ h : W \to Y $ such that $ h = g \circ f $, the cokernel cofork formed by $ c.\pi $ is also a colimit for $ h $.

CategoryTheory.Limits.isCokernelEpiComp_desc theorem

 {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g] {h : W ⟶ Y} (hh : h = g ≫ f)
  (s : CokernelCofork h) :
  (isCokernelEpiComp i g hh).desc s =
    i.desc
      (Cofork.ofπ s.π
        (by
          rw [← cancel_epi g, ← Category.assoc, ← hh]
          simp))

Full source

@[simp]
theorem isCokernelEpiComp_desc {c : CokernelCofork f} (i : IsColimit c) {W} (g : W ⟶ X) [hg : Epi g]
    {h : W ⟶ Y} (hh : h = g ≫ f) (s : CokernelCofork h) :
    (isCokernelEpiComp i g hh).desc s =
      i.desc
        (Cofork.ofπ s.π
          (by
            rw [← cancel_epi g, ← Category.assoc, ← hh]
            simp)) :=
  rfl

Descending Morphism Equality for Cokernel under Epimorphism Composition

Informal description

Let $f \colon X \to Y$ be a morphism in a category with zero morphisms, and let $c$ be a cokernel cofork for $f$ that is a colimit. Given an epimorphism $g \colon W \to X$ and a morphism $h \colon W \to Y$ such that $h = g \circ f$, the descending morphism from the colimit of the cokernel cofork constructed via $c.\pi$ for $h$ is equal to the descending morphism from $c$ applied to the cofork formed by $s.\pi$, where $s$ is any cokernel cofork for $h$.

CategoryTheory.Limits.isCokernelOfComp definition

 {W : C} (g : W ⟶ X) (h : W ⟶ Y) {c : CokernelCofork h} (i : IsColimit c) (hf : f ≫ c.π = 0) (hfg : g ≫ f = h) :
  IsColimit (CokernelCofork.ofπ c.π hf)

Full source

/-- Every cokernel of `g ≫ f` is also a cokernel of `f`, as long as `f ≫ c.π` vanishes. -/
def isCokernelOfComp {W : C} (g : W ⟶ X) (h : W ⟶ Y) {c : CokernelCofork h} (i : IsColimit c)
    (hf : f ≫ c.π = 0) (hfg : g ≫ f = h) : IsColimit (CokernelCofork.ofπ c.π hf) :=
  Cofork.IsColimit.mk _ (fun s => i.desc (CokernelCofork.ofπ s.π (by simp [← hfg])))
    (fun s => by simp only [CokernelCofork.π_ofπ, Cofork.IsColimit.π_desc]) fun s m h => by
      apply Cofork.IsColimit.hom_ext i
      simpa using h

Colimit property of cokernel cofork under composition

Informal description

Given morphisms $ g : W \to X $ and $ h : W \to Y $ in a category with zero morphisms, if $ c $ is a cokernel cofork for $ h $ and $ i $ is a proof that $ c $ is a colimit, then under the conditions that $ f \circ c.\pi = 0 $ and $ g \circ f = h $, the cokernel cofork formed by $ c.\pi $ is also a colimit.

CategoryTheory.Limits.CokernelCofork.IsColimit.ofId definition

 {X Y : C} (f : X ⟶ Y) (hf : f = 0) : IsColimit (CokernelCofork.ofπ (𝟙 Y) (show f ≫ 𝟙 Y = 0 by rw [hf, zero_comp]))

Full source

/-- `Y` identifies to the cokernel of a zero map `X ⟶ Y`. -/
def CokernelCofork.IsColimit.ofId {X Y : C} (f : X ⟶ Y) (hf : f = 0) :
    IsColimit (CokernelCofork.ofπ (𝟙 Y) (show f ≫ 𝟙 Y = 0 by rw [hf, zero_comp])) :=
  CokernelCofork.IsColimit.ofπ _ _ (fun x _ => x) (fun _ _ => Category.id_comp _)
    (fun _ _ _ hb => by simp only [← hb, Category.id_comp])

Identity morphism as cokernel of zero morphism

Informal description

Given a zero morphism $ f : X \to Y $ in a category with zero morphisms, the identity morphism $ \text{id}_Y $ on $ Y $ satisfies the universal property of the cokernel of $ f $. Specifically, the cokernel cofork formed by $ \text{id}_Y $ is a colimit, meaning that for any morphism $ g : Y \to Z $ such that $ f \circ g = 0 $, there exists a unique morphism $ Y \to Z $ factoring $ g $ through $ \text{id}_Y $.

CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero definition

{X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hf : Epi f) (h : IsZero c.pt) : IsColimit c

Full source

/-- Any zero object identifies to the cokernel of a given epimorphisms. -/
def CokernelCofork.IsColimit.ofEpiOfIsZero {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f)
    (hf : Epi f) (h : IsZero c.pt) : IsColimit c :=
  isColimitAux _ (fun _ => 0) (fun s => by rw [comp_zero, ← cancel_epi f, comp_zero, s.condition])
    (fun _ _ _ => h.eq_of_src _ _)

Cokernel cofork is colimit for epimorphism with zero target

Informal description

Given a cokernel cofork $ c $ for an epimorphism $ f : X \to Y $ in a category with zero morphisms, if the object $ c.pt $ is a zero object, then $ c $ is a colimit cokernel cofork for $ f $. This means that the zero morphism from $ Y $ to $ c.pt $ satisfies the universal property of the cokernel of $ f $.

CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π theorem

{X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c) (hf : f = 0) : IsIso c.π

Full source

lemma CokernelCofork.IsColimit.isIso_π {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f)
    (hc : IsColimit c) (hf : f = 0) : IsIso c.π := by
  let e : c.pt ≅ Y := IsColimit.coconePointUniqueUpToIso hc
    (CokernelCofork.IsColimit.ofId (f : X ⟶ Y) hf)
  have eq : c.π ≫ e.hom = 𝟙 Y := Cofork.IsColimit.π_desc hc
  haveI : IsIso (c.π ≫ e.hom) := by
    rw [eq]
    dsimp
    infer_instance
  exact IsIso.of_isIso_comp_right c.π e.hom

Cokernel Projection Isomorphism for Zero Morphism

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f : X \to Y$ be a morphism in $\mathcal{C}$ such that $f = 0$. If $c$ is a cokernel cofork for $f$ and $hc$ is a proof that $c$ is a colimit cokernel cofork, then the projection morphism $\pi_c : Y \to c.pt$ is an isomorphism.

CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff definition

 {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (hc : IsColimit c) {X' Y' : C} (f' : X' ⟶ Y') (e : Y' ≅ Y)
  (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0) :
  IsColimit (CokernelCofork.ofπ (f := f') (e.hom ≫ c.π) (by simp [← iff]))

Full source

/-- If `c` is a colimit cokernel cofork for `f : X ⟶ Y`, `e : Y ≅ Y'` and `f' : X' ⟶ Y` is a
morphism, then there is a colimit cokernel cofork for `f'` with the same point as `c` if for any
morphism `φ : Y ⟶ W`, there is an equivalence `f ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0`. -/
def CokernelCofork.isColimitOfIsColimitOfIff {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f}
    (hc : IsColimit c) {X' Y' : C} (f' : X' ⟶ Y') (e : Y' ≅ Y)
    (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φf ≫ φ = 0 ↔ f' ≫ e.hom ≫ φ = 0) :
    IsColimit (CokernelCofork.ofπ (f := f') (e.hom ≫ c.π) (by simp [← iff])) :=
  CokernelCofork.IsColimit.ofπ _ _
    (fun s hs ↦ hc.desc (CokernelCofork.ofπ (π := e.inv ≫ s)
      (by rw [iff, e.hom_inv_id_assoc, hs])))
    (fun s hs ↦ by simp [← cancel_epi e.inv])
    (fun s hs m hm ↦ Cofork.IsColimit.hom_ext hc (by simpa [← cancel_epi e.hom] using hm))

Colimit cokernel cofork equivalence under isomorphism and zero condition

Informal description

Given a colimit cokernel cofork $ c $ for a morphism $ f : X \to Y $ in a category with zero morphisms, an isomorphism $ e : Y' \to Y $, and a morphism $ f' : X' \to Y' $, if for any morphism $ \varphi : Y \to W $ the condition $ f \circ \varphi = 0 $ is equivalent to $ f' \circ e \circ \varphi = 0 $, then the cokernel cofork for $ f' $ constructed by composing $ e $ with $ c.\pi $ is also a colimit.

CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff' definition

 {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (hc : IsColimit c) {X' : C} (f' : X' ⟶ Y)
  (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φ = 0 ↔ f' ≫ φ = 0) : IsColimit (CokernelCofork.ofπ (f := f') c.π (by simp [← iff]))

Full source

/-- If `c` is a colimit cokernel cofork for `f : X ⟶ Y`, and `f' : X' ⟶ Y is another
morphism, then there is a colimit cokernel cofork for `f'` with the same point as `c` if for any
morphism `φ : Y ⟶ W`, there is an equivalence `f ≫ φ = 0 ↔ f' ≫ φ = 0`. -/
def CokernelCofork.isColimitOfIsColimitOfIff' {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f}
    (hc : IsColimit c) {X' : C} (f' : X' ⟶ Y)
    (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), f ≫ φf ≫ φ = 0 ↔ f' ≫ φ = 0) :
    IsColimit (CokernelCofork.ofπ (f := f') c.π (by simp [← iff])) :=
  IsColimit.ofIsoColimit (isColimitOfIsColimitOfIff hc f' (Iso.refl _) (by simpa using iff))
    (Cofork.ext (Iso.refl _))

Colimit cokernel cofork equivalence under zero condition

Informal description

Given a colimit cokernel cofork $ c $ for a morphism $ f : X \to Y $ in a category with zero morphisms, and another morphism $ f' : X' \to Y $, if for any morphism $ \varphi : Y \to W $ the condition $ f \circ \varphi = 0 $ is equivalent to $ f' \circ \varphi = 0 $, then the cokernel cofork for $ f' $ constructed using the same projection $ c.\pi $ is also a colimit.

CategoryTheory.Limits.CokernelCofork.mapOfIsColimit definition

 {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f') (φ : Arrow.mk f ⟶ Arrow.mk f') : cc.pt ⟶ cc'.pt

Full source

/-- The morphism between points of cokernel coforks induced by a morphism
in the category of arrows. -/
def mapOfIsColimit {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f')
    (φ : Arrow.mkArrow.mk f ⟶ Arrow.mk f') : cc.pt ⟶ cc'.pt :=
  hf.desc (CokernelCofork.ofπ (φ.right ≫ cc'.π) (by
    erw [← Arrow.w_assoc φ, condition, comp_zero]))

Morphism between cokernel coforks induced by a morphism of arrows

Informal description

Given a cokernel cofork `cc` for a morphism `f : X → Y` in a category with zero morphisms, where `cc` is a colimit, and another cokernel cofork `cc'` for a morphism `f' : X' → Y'`, along with a morphism `φ` between the corresponding arrows `(f : X → Y)` and `(f' : X' → Y')`, the function constructs a morphism from the vertex of `cc` to the vertex of `cc'` that commutes with the cofork projections.

CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit theorem

 {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f') (φ : Arrow.mk f ⟶ Arrow.mk f') :
  cc.π ≫ mapOfIsColimit hf cc' φ = φ.right ≫ cc'.π

Full source

@[reassoc (attr := simp)]
lemma π_mapOfIsColimit {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f')
    (φ : Arrow.mkArrow.mk f ⟶ Arrow.mk f') :
    cc.π ≫ mapOfIsColimit hf cc' φ = φ.right ≫ cc'.π :=
  hf.fac _ _

Commutativity of Induced Map Between Cokernel Coforks

Informal description

Let $\mathcal{C}$ be a category with zero morphisms. Given: - A colimit cokernel cofork $cc$ for a morphism $f : X \to Y$ (with $hf$ witnessing its colimit property) - Another cokernel cofork $cc'$ for a morphism $f' : X' \to Y'$ - A morphism $\varphi$ between the corresponding arrows $(f : X \to Y)$ and $(f' : X' \to Y')$ Then the diagram commutes, meaning the composition of the cokernel projection $\pi_{cc} : Y \to cc.pt$ with the induced map $mapOfIsColimit\ hf\ cc'\ \varphi : cc.pt \to cc'.pt$ equals the composition of $\varphi_{\text{right}} : Y \to Y'$ with the cokernel projection $\pi_{cc'} : Y' \to cc'.pt$. In symbols: $\pi_{cc} \circ mapOfIsColimit\ hf\ cc'\ \varphi = \varphi_{\text{right}} \circ \pi_{cc'}$

CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit definition

 {cc : CokernelCofork f} {cc' : CokernelCofork f'} (hf : IsColimit cc) (hf' : IsColimit cc')
  (φ : Arrow.mk f ≅ Arrow.mk f') : cc.pt ≅ cc'.pt

Full source

/-- The isomorphism between points of limit cokernel coforks induced by an isomorphism
in the category of arrows. -/
@[simps]
def mapIsoOfIsColimit {cc : CokernelCofork f} {cc' : CokernelCofork f'}
    (hf : IsColimit cc) (hf' : IsColimit cc')
    (φ : Arrow.mkArrow.mk f ≅ Arrow.mk f') : cc.pt ≅ cc'.pt where
  hom := mapOfIsColimit hf cc' φ.hom
  inv := mapOfIsColimit hf' cc φ.inv
  hom_inv_id := Cofork.IsColimit.hom_ext hf (by simp)
  inv_hom_id := Cofork.IsColimit.hom_ext hf' (by simp)

Isomorphism between cokernel coforks induced by an isomorphism of arrows

Informal description

Given two cokernel coforks `cc` and `cc'` for morphisms `f : X → Y` and `f' : X' → Y'` respectively, where both coforks are colimits, and an isomorphism `φ` between the corresponding arrows `(f : X → Y)` and `(f' : X' → Y')`, this constructs an isomorphism between the vertices of the two coforks that commutes with the cofork projections.

CategoryTheory.Limits.cokernel abbrev

: C

Full source

/-- The cokernel of a morphism, expressed as the coequalizer with the 0 morphism. -/
abbrev cokernel : C :=
  coequalizer f 0

Cokernel as Coequalizer with Zero Morphism

Informal description

In a category $\mathcal{C}$ with zero morphisms, the cokernel of a morphism $f : X \to Y$ is the coequalizer of $f$ and the zero morphism $0 : X \to Y$. It is an object $\text{cokernel}(f)$ in $\mathcal{C}$ equipped with a morphism $\pi : Y \to \text{cokernel}(f)$ satisfying $\pi \circ f = 0$, and it is universal among all such objects.

CategoryTheory.Limits.cokernel.π abbrev

: Y ⟶ cokernel f

Full source

/-- The map from the target of `f` to `cokernel f`. -/
abbrev cokernel.π : Y ⟶ cokernel f :=
  coequalizer.π f 0

Universal Cokernel Projection $\pi$ for Morphism $f$

Informal description

Given a morphism $f : X \to Y$ in a category with zero morphisms, the cokernel projection $\pi : Y \to \text{cokernel}(f)$ is the universal morphism satisfying $f \circ \pi = 0$.

CategoryTheory.Limits.coequalizer_as_cokernel theorem

: coequalizer.π f 0 = cokernel.π f

Full source

@[simp]
theorem coequalizer_as_cokernel : coequalizer.π f 0 = cokernel.π f :=
  rfl

Cokernel as Coequalizer of Morphism and Zero Morphism

Informal description

In a category with zero morphisms, the coequalizer projection $\pi$ for the parallel morphisms $f$ and $0$ is equal to the cokernel projection $\pi$ of $f$, i.e., $\text{coequalizer.π}(f, 0) = \text{cokernel.π}(f)$.

CategoryTheory.Limits.cokernel.condition theorem

: f ≫ cokernel.π f = 0

Full source

@[reassoc (attr := simp)]
theorem cokernel.condition : f ≫ cokernel.π f = 0 :=
  CokernelCofork.condition _

Cokernel Condition: $f \circ \pi = 0$

Informal description

For any morphism $f \colon X \to Y$ in a category with zero morphisms, the composition of $f$ with its cokernel projection $\pi \colon Y \to \text{cokernel}(f)$ equals the zero morphism, i.e., $f \circ \pi = 0$.

CategoryTheory.Limits.cokernelIsCokernel definition

: IsColimit (Cofork.ofπ (cokernel.π f) ((cokernel.condition f).trans zero_comp.symm))

Full source

/-- The cokernel built from `cokernel.π f` is colimiting. -/
def cokernelIsCokernel :
    IsColimit (Cofork.ofπ (cokernel.π f) ((cokernel.condition f).trans zero_comp.symm)) :=
  IsColimit.ofIsoColimit (colimit.isColimit _) (Cofork.ext (Iso.refl _))

Universal property of the cokernel cofork

Informal description

The cofork formed by the cokernel projection $\pi \colon Y \to \text{cokernel}(f)$ is a colimit cocone for the parallel pair of morphisms $f$ and the zero morphism $0 \colon X \to Y$ in a category with zero morphisms. This means it satisfies the universal property of cokernels: for any other cofork $(W, k \colon Y \to W)$ with $f \circ k = 0$, there exists a unique morphism $\text{cokernel}(f) \to W$ making the appropriate diagram commute.

CategoryTheory.Limits.cokernel.desc abbrev

{W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : cokernel f ⟶ W

Full source

/-- Given any morphism `k : Y ⟶ W` such that `f ≫ k = 0`, `k` factors through `cokernel.π f`
    via `cokernel.desc : cokernel f ⟶ W`. -/
abbrev cokernel.desc {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : cokernelcokernel f ⟶ W :=
  (cokernelIsCokernel f).desc (CokernelCofork.ofπ k h)

Universal Property of Cokernel: Factorization of Morphisms Annihilated by $f$

Informal description

Given a morphism $k \colon Y \to W$ in a category with zero morphisms such that $f \circ k = 0$, there exists a unique morphism $\text{cokernel}(f) \to W$ factoring $k$ through the cokernel projection $\pi \colon Y \to \text{cokernel}(f)$.

CategoryTheory.Limits.cokernel.π_desc theorem

{W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : cokernel.π f ≫ cokernel.desc f k h = k

Full source

@[reassoc (attr := simp)]
theorem cokernel.π_desc {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) :
    cokernel.πcokernel.π f ≫ cokernel.desc f k h = k :=
  (cokernelIsCokernel f).fac (CokernelCofork.ofπ k h) WalkingParallelPair.one

Factorization Property of Cokernel: $\pi \circ \text{desc}(f, k, h) = k$

Informal description

Given a morphism $k \colon Y \to W$ in a category with zero morphisms such that $f \circ k = 0$, the composition of the cokernel projection $\pi \colon Y \to \text{cokernel}(f)$ with the induced morphism $\text{cokernel}(f) \to W$ equals $k$, i.e., $\pi \circ \text{cokernel.desc}(f, k, h) = k$.

CategoryTheory.Limits.colimit_ι_zero_cokernel_desc theorem

 {C : Type*} [Category C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : f ≫ g = 0) [HasCokernel f] :
  colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h = 0

Full source

@[reassoc (attr := simp)]
lemma colimit_ι_zero_cokernel_desc {C : Type*} [Category C]
    [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : f ≫ g = 0) [HasCokernel f] :
    colimit.ιcolimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h = 0 := by
  rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]
  simp

Composition of Cokernel Descent with Coprojection is Zero

Informal description

Let $\mathcal{C}$ be a category with zero morphisms, and let $f \colon X \to Y$ and $g \colon Y \to Z$ be morphisms in $\mathcal{C}$ such that $f \circ g = 0$. If $\mathcal{C}$ has a cokernel for $f$, then the composition of the coprojection $\iota_0 \colon X \to \text{colimit}(\text{parallelPair}(f, 0))$ with the cokernel descent morphism $\text{cokernel.desc}(f, g, h) \colon \text{cokernel}(f) \to Z$ equals the zero morphism, i.e., $\iota_0 \circ \text{cokernel.desc}(f, g, h) = 0$.

CategoryTheory.Limits.cokernel.desc_zero theorem

{W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0

Full source

@[simp]
theorem cokernel.desc_zero {W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0 := by
  ext; simp

Cokernel Descent of Zero Morphism is Zero

Informal description

For any object $W$ in a category with zero morphisms, the cokernel descent morphism $\text{cokernel.desc}(f, 0, h) \colon \text{cokernel}(f) \to W$ is equal to the zero morphism $0 \colon \text{cokernel}(f) \to W$.

CategoryTheory.Limits.cokernel.desc_epi instance

{W : C} (k : Y ⟶ W) (h : f ≫ k = 0) [Epi k] : Epi (cokernel.desc f k h)

Full source

instance cokernel.desc_epi {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) [Epi k] :
    Epi (cokernel.desc f k h) :=
  ⟨fun {Z} g g' w => by
    replace w := cokernel.π f ≫= w
    simp only [cokernel.π_desc_assoc] at w
    exact (cancel_epi k).1 w⟩

Epimorphism Property of Cokernel Descent for Epimorphisms

Informal description

For any epimorphism $k \colon Y \to W$ in a category with zero morphisms such that $f \circ k = 0$, the induced morphism $\text{cokernel}(f) \to W$ obtained via the universal property of the cokernel is also an epimorphism.

CategoryTheory.Limits.cokernel.desc' definition

{W : C} (k : Y ⟶ W) (h : f ≫ k = 0) : { l : cokernel f ⟶ W // cokernel.π f ≫ l = k }

Full source

/-- Any morphism `k : Y ⟶ W` satisfying `f ≫ k = 0` induces `l : cokernel f ⟶ W` such that
    `cokernel.π f ≫ l = k`. -/
def cokernel.desc' {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) :
    { l : cokernel f ⟶ W // cokernel.π f ≫ l = k } :=
  ⟨cokernel.desc f k h, cokernel.π_desc _ _ _⟩

Factorization of morphisms through cokernel

Informal description

Given a morphism $ k : Y \to W $ in a category with zero morphisms such that $ f \circ k = 0 $, there exists a unique morphism $ l : \text{cokernel}(f) \to W $ such that the composition $ \pi \circ l = k $, where $ \pi : Y \to \text{cokernel}(f) $ is the cokernel projection of $ f $.

CategoryTheory.Limits.cokernel.map abbrev

 {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : f ≫ q = p ≫ f') : cokernel f ⟶ cokernel f'

Full source

/-- A commuting square induces a morphism of cokernels. -/
abbrev cokernel.map {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y')
    (w : f ≫ q = p ≫ f') : cokernelcokernel f ⟶ cokernel f' :=
  cokernel.desc f (q ≫ cokernel.π f') (by
    have : f ≫ q ≫ π f' = p ≫ f' ≫ π f' := by
      simp only [← Category.assoc]
      apply congrArg (· ≫ π f') w
    simp [this])

Induced Cokernel Morphism from Commutative Square

Informal description

Given a commutative square in a category with zero morphisms, where morphisms $f \colon X \to Y$ and $f' \colon X' \to Y'$ have cokernels, and morphisms $p \colon X \to X'$ and $q \colon Y \to Y'$ satisfy $f \circ q = p \circ f'$, there exists an induced morphism $\text{cokernel}(f) \to \text{cokernel}(f')$.

CategoryTheory.Limits.cokernel.map_desc theorem

 {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g : Y ⟶ Z) (w : f ≫ g = 0) (f' : X' ⟶ Y') [HasCokernel f']
  (g' : Y' ⟶ Z') (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
  cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r

Full source

/-- Given a commutative diagram
    X --f--> Y --g--> Z
    |        |        |
    |        |        |
    v        v        v
    X' -f'-> Y' -g'-> Z'
with horizontal arrows composing to zero,
then we obtain a commutative square
   cokernel f ---> Z
   |               |
   | cokernel.map  |
   |               |
   v               v
   cokernel f' --> Z'
-/
theorem cokernel.map_desc {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g : Y ⟶ Z)
    (w : f ≫ g = 0) (f' : X' ⟶ Y') [HasCokernel f'] (g' : Y' ⟶ Z') (w' : f' ≫ g' = 0) (p : X ⟶ X')
    (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
    cokernel.mapcokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desccokernel.desc f g w ≫ r := by
  ext; simp [h₂]

Commutativity of Cokernel Maps in a Double Commutative Diagram

Informal description

Given a commutative diagram in a category with zero morphisms: \[ \begin{array}{cccccc} X & \xrightarrow{f} & Y & \xrightarrow{g} & Z \\ \downarrow{p} & & \downarrow{q} & & \downarrow{r} \\ X' & \xrightarrow{f'} & Y' & \xrightarrow{g'} & Z' \end{array} \] where the horizontal compositions satisfy $f \circ g = 0$ and $f' \circ g' = 0$, and the squares commute ($f \circ q = p \circ f'$ and $g \circ r = q \circ g'$), the induced morphisms between cokernels satisfy: \[ \text{cokernel.map}(f, f', p, q, h_1) \circ \text{cokernel.desc}(f', g', w') = \text{cokernel.desc}(f, g, w) \circ r \]

CategoryTheory.Limits.cokernel.mapIso definition

 {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : f ≫ q.hom = p.hom ≫ f') :
  cokernel f ≅ cokernel f'

Full source

/-- A commuting square of isomorphisms induces an isomorphism of cokernels. -/
@[simps]
def cokernel.mapIso {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y')
    (w : f ≫ q.hom = p.hom ≫ f') : cokernelcokernel f ≅ cokernel f' where
  hom := cokernel.map f f' p.hom q.hom w
  inv := cokernel.map f' f p.inv q.inv (by
          refine (cancel_mono q.hom).1 ?_
          simp [w])

Isomorphism of cokernels induced by a commutative square of isomorphisms

Informal description

Given a commutative square of isomorphisms in a category with zero morphisms, where $f \colon X \to Y$ and $f' \colon X' \to Y'$ have cokernels, and isomorphisms $p \colon X \cong X'$ and $q \colon Y \cong Y'$ satisfy $f \circ q = p \circ f'$, there exists an induced isomorphism $\text{cokernel}(f) \cong \text{cokernel}(f')$.

CategoryTheory.Limits.cokernel.π_zero_isIso instance

: IsIso (cokernel.π (0 : X ⟶ Y))

Full source

/-- The cokernel of the zero morphism is an isomorphism -/
instance cokernel.π_zero_isIso : IsIso (cokernel.π (0 : X ⟶ Y)) :=
  coequalizer.π_of_self _

Cokernel Projection of Zero Morphism is an Isomorphism

Informal description

In a category with zero morphisms, the cokernel projection $\pi : Y \to \text{cokernel}(0)$ of the zero morphism $0 : X \to Y$ is an isomorphism.

CategoryTheory.Limits.cokernelZeroIsoTarget definition

: cokernel (0 : X ⟶ Y) ≅ Y

Full source

/-- The cokernel of a zero morphism is isomorphic to the target. -/
def cokernelZeroIsoTarget : cokernelcokernel (0 : X ⟶ Y) ≅ Y :=
  coequalizer.isoTargetOfSelf 0

Cokernel of zero morphism is isomorphic to target

Informal description

In a category with zero morphisms, the cokernel of the zero morphism $ 0 : X \to Y $ is isomorphic to the target object $ Y $. This isomorphism is constructed using the fact that the coequalizer of a morphism with itself is isomorphic to its target.

CategoryTheory.Limits.cokernelZeroIsoTarget_hom theorem

: cokernelZeroIsoTarget.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp)

Full source

@[simp]
theorem cokernelZeroIsoTarget_hom :
    cokernelZeroIsoTarget.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) := by
  ext; simp [cokernelZeroIsoTarget]

Homomorphism of Cokernel-Zero Isomorphism via Universal Property

Informal description

The homomorphism component of the isomorphism $\text{cokernel}(0 : X \to Y) \cong Y$ is equal to the cokernel's universal morphism $\text{cokernel.desc}$ applied to the zero morphism $0 : X \to Y$ and the identity morphism $\text{id}_Y$ on $Y$.

CategoryTheory.Limits.cokernelZeroIsoTarget_inv theorem

: cokernelZeroIsoTarget.inv = cokernel.π (0 : X ⟶ Y)

Full source

@[simp]
theorem cokernelZeroIsoTarget_inv : cokernelZeroIsoTarget.inv = cokernel.π (0 : X ⟶ Y) :=
  rfl

Inverse of Cokernel-Zero Isomorphism Equals Cokernel Projection

Informal description

The inverse of the isomorphism $\text{cokernelZeroIsoTarget}$ is equal to the cokernel projection $\pi$ of the zero morphism $0 : X \to Y$.

CategoryTheory.Limits.cokernelIsoOfEq definition

{f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel f ≅ cokernel g

Full source

/-- If two morphisms are known to be equal, then their cokernels are isomorphic. -/
def cokernelIsoOfEq {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernelcokernel f ≅ cokernel g :=
  HasColimit.isoOfNatIso (by simp [h]; rfl)

Isomorphism of cokernels for equal morphisms

Informal description

Given two equal morphisms $ f, g : X \to Y $ in a category with zero morphisms, where both $ f $ and $ g $ have cokernels, the cokernel objects $ \text{cokernel}(f) $ and $ \text{cokernel}(g) $ are isomorphic. The isomorphism is induced by the equality $ h : f = g $ and the universal properties of the cokernels.

CategoryTheory.Limits.cokernelIsoOfEq_refl theorem

{h : f = f} : cokernelIsoOfEq h = Iso.refl (cokernel f)

Full source

@[simp]
theorem cokernelIsoOfEq_refl {h : f = f} : cokernelIsoOfEq h = Iso.refl (cokernel f) := by
  ext; simp [cokernelIsoOfEq]

Identity Isomorphism for Cokernel of Equal Morphisms

Informal description

For any morphism $f : X \to Y$ in a category with zero morphisms, the isomorphism $\text{cokernelIsoOfEq}(h)$ induced by the equality $h : f = f$ is equal to the identity isomorphism on $\text{cokernel}(f)$.

CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom theorem

{f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel.π f ≫ (cokernelIsoOfEq h).hom = cokernel.π g

Full source

@[reassoc (attr := simp)]
theorem π_comp_cokernelIsoOfEq_hom {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.πcokernel.π f ≫ (cokernelIsoOfEq h).hom = cokernel.π g := by
  cases h; simp

Compatibility of Cokernel Projections with Isomorphism Induced by Equality of Morphisms

Informal description

Given two equal morphisms $f, g : X \to Y$ in a category with zero morphisms, where both $f$ and $g$ have cokernels, the composition of the cokernel projection $\pi_f : Y \to \text{cokernel}(f)$ with the isomorphism $(cokernelIsoOfEq h).hom : \text{cokernel}(f) \to \text{cokernel}(g)$ induced by the equality $h : f = g$ equals the cokernel projection $\pi_g : Y \to \text{cokernel}(g)$.

CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv theorem

{f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel.π _ ≫ (cokernelIsoOfEq h).inv = cokernel.π _

Full source

@[reassoc (attr := simp)]
theorem π_comp_cokernelIsoOfEq_inv {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) :
    cokernel.πcokernel.π _ ≫ (cokernelIsoOfEq h).inv = cokernel.π _ := by
  cases h; simp

Compatibility of Cokernel Projection with Cokernel Isomorphism Inverse

Informal description

For any two equal morphisms $f, g : X \to Y$ in a category with zero morphisms, where both $f$ and $g$ have cokernels, the composition of the cokernel projection $\pi$ with the inverse of the isomorphism $\text{cokernelIsoOfEq}(h)$ (induced by the equality $h : f = g$) equals the cokernel projection $\pi$.

CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc theorem

 {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he) :
  (cokernelIsoOfEq h).hom ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [h, he])

Full source

@[reassoc (attr := simp)]
theorem cokernelIsoOfEq_hom_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g)
    (e : Y ⟶ Z) (he) :
    (cokernelIsoOfEq h).hom ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [h, he]) := by
  cases h; simp

Compatibility of Cokernel Isomorphism with Descent Morphism for Equal Morphisms

Informal description

Let $f, g : X \to Y$ be morphisms in a category with zero morphisms, where both $f$ and $g$ have cokernels. Given an equality $h : f = g$, a morphism $e : Y \to Z$, and a proof $he$ that $g \circ e = 0$, the composition of the isomorphism $(cokernelIsoOfEq h).hom : cokernel(f) \to cokernel(g)$ with the cokernel descent morphism $cokernel.desc\ g\ e\ he$ equals the cokernel descent morphism $cokernel.desc\ f\ e\ (by\ simp [h, he])$.

CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc theorem

 {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he) :
  (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he])

Full source

@[reassoc (attr := simp)]
theorem cokernelIsoOfEq_inv_comp_desc {Z} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g)
    (e : Y ⟶ Z) (he) :
    (cokernelIsoOfEq h).inv ≫ cokernel.desc _ e he = cokernel.desc _ e (by simp [← h, he]) := by
  cases h; simp

Inverse Cokernel Isomorphism Composes with Descent Morphism for Equal Morphisms

Informal description

Let $f, g \colon X \to Y$ be morphisms in a category with zero morphisms, where both $f$ and $g$ have cokernels. Given an equality $h \colon f = g$, a morphism $e \colon Y \to Z$, and a proof $he$ that $f \circ e = 0$, the composition of the inverse of the isomorphism $\text{cokernelIsoOfEq}(h)$ with the cokernel descent morphism $\text{cokernel.desc}(f, e, he)$ equals the cokernel descent morphism $\text{cokernel.desc}(g, e, \text{by simp } [\leftarrow h, he])$.

CategoryTheory.Limits.cokernelIsoOfEq_trans theorem

 {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h] (w₁ : f = g) (w₂ : g = h) :
  cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq (w₁.trans w₂)

Full source

@[simp]
theorem cokernelIsoOfEq_trans {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h]
    (w₁ : f = g) (w₂ : g = h) :
    cokernelIsoOfEqcokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq (w₁.trans w₂) := by
  cases w₁; cases w₂; ext; simp [cokernelIsoOfEq]

Composition of Cokernel Isomorphisms for Transitive Equalities

Informal description

Let $f, g, h \colon X \to Y$ be morphisms in a category with zero morphisms, where $f$, $g$, and $h$ all have cokernels. Given equalities $w_1 \colon f = g$ and $w_2 \colon g = h$, the composition of the induced isomorphisms $\text{cokernel}(f) \cong \text{cokernel}(g)$ and $\text{cokernel}(g) \cong \text{cokernel}(h)$ is equal to the isomorphism $\text{cokernel}(f) \cong \text{cokernel}(h)$ induced by the equality $w_1 \circ w_2 \colon f = h$.

CategoryTheory.Limits.cokernel_not_mono_of_nonzero theorem

(w : f ≠ 0) : ¬Mono (cokernel.π f)

Full source

theorem cokernel_not_mono_of_nonzero (w : f ≠ 0) : ¬Mono (cokernel.π f) := fun _ =>
  w (eq_zero_of_mono_cokernel f)

Nonzero morphism implies cokernel projection is not mono

Informal description

If a morphism $f : X \to Y$ in a category with zero morphisms is nonzero, then the cokernel projection $\pi : Y \to \text{cokernel}(f)$ is not a monomorphism.

CategoryTheory.Limits.cokernel_not_iso_of_nonzero theorem

(w : f ≠ 0) : IsIso (cokernel.π f) → False

Full source

theorem cokernel_not_iso_of_nonzero (w : f ≠ 0) : IsIso (cokernel.π f) → False := fun _ =>
  cokernel_not_mono_of_nonzero w inferInstance

Nonzero morphism implies cokernel projection is not an isomorphism

Informal description

For any nonzero morphism $f \colon X \to Y$ in a category with zero morphisms, the cokernel projection $\pi \colon Y \to \text{cokernel}(f)$ cannot be an isomorphism.

CategoryTheory.Limits.hasCokernel_comp_iso instance

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : HasCokernel (f ≫ g)

Full source

instance hasCokernel_comp_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] :
    HasCokernel (f ≫ g) where
  exists_colimit :=
    ⟨{  cocone := CokernelCofork.ofπ (inv g ≫ cokernel.π f) (by simp)
        isColimit :=
          isColimitAux _
            (fun s =>
              cokernel.desc _ (g ≫ s.π) (by rw [← Category.assoc, CokernelCofork.condition]))
            (by simp) fun s m w => by
            simp_rw [← w]
            symm
            apply coequalizer.hom_ext
            simp }⟩

Existence of Cokernel for Composition with Isomorphism

Informal description

In a category with zero morphisms, given a morphism $f \colon X \to Y$ that has a cokernel and an isomorphism $g \colon Y \to Z$, the composition $f \circ g$ also has a cokernel.

CategoryTheory.Limits.cokernelCompIsIso definition

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : cokernel (f ≫ g) ≅ cokernel f

Full source

/-- When `g` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `f`.
-/
@[simps]
def cokernelCompIsIso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] :
    cokernelcokernel (f ≫ g) ≅ cokernel f where
  hom := cokernel.desc _ (inv g ≫ cokernel.π f) (by simp)
  inv := cokernel.desc _ (g ≫ cokernel.π (f ≫ g)) (by rw [← Category.assoc, cokernel.condition])

Cokernel of composition with isomorphism is isomorphic to cokernel

Informal description

Given a morphism $ f : X \to Y $ and an isomorphism $ g : Y \to Z $ in a category with zero morphisms, if $ f $ has a cokernel, then the cokernel of the composition $ f \circ g $ is isomorphic to the cokernel of $ f $. More precisely, there exists an isomorphism $ \text{cokernel}(f \circ g) \cong \text{cokernel}(f) $ given by: - The forward morphism is the universal morphism induced by $ g^{-1} \circ \pi_f $, where $ \pi_f $ is the cokernel projection of $ f $. - The inverse morphism is the universal morphism induced by $ g \circ \pi_{f \circ g} $, where $ \pi_{f \circ g} $ is the cokernel projection of $ f \circ g $.

CategoryTheory.Limits.hasCokernel_epi_comp instance

{X Y : C} (f : X ⟶ Y) [HasCokernel f] {W} (g : W ⟶ X) [Epi g] : HasCokernel (g ≫ f)

Full source

instance hasCokernel_epi_comp {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W} (g : W ⟶ X) [Epi g] :
    HasCokernel (g ≫ f) :=
  ⟨⟨{   cocone := _
        isColimit := isCokernelEpiComp (colimit.isColimit _) g rfl }⟩⟩

Existence of Cokernel for Composition with Epimorphism

Informal description

In a category with zero morphisms, given a morphism $ f : X \to Y $ that has a cokernel, and an epimorphism $ g : W \to X $, the composition $ g \circ f $ also has a cokernel.

CategoryTheory.Limits.cokernelEpiComp definition

{X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel g] : cokernel (f ≫ g) ≅ cokernel g

Full source

/-- When `f` is an epimorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.
-/
@[simps]
def cokernelEpiComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel g] :
    cokernelcokernel (f ≫ g) ≅ cokernel g where
  hom := cokernel.desc _ (cokernel.π g) (by simp)
  inv :=
    cokernel.desc _ (cokernel.π (f ≫ g))
      (by
        rw [← cancel_epi f, ← Category.assoc]
        simp)

Cokernel of composition with epimorphism is isomorphic to cokernel

Informal description

Given an epimorphism $ f : X \to Y $ and a morphism $ g : Y \to Z $ in a category with zero morphisms, if $ g $ has a cokernel, then the cokernel of the composition $ f \circ g $ is isomorphic to the cokernel of $ g $.

CategoryTheory.Limits.cokernel.congr definition

{X Y : C} (f g : X ⟶ Y) [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel f ≅ cokernel g

Full source

/-- Equal maps have isomorphic cokernels. -/
@[simps] def cokernel.congr {X Y : C} (f g : X ⟶ Y) [HasCokernel f] [HasCokernel g]
    (h : f = g) : cokernelcokernel f ≅ cokernel g where
  hom := cokernel.desc _ (cokernel.π g) (by simp [h])
  inv := cokernel.desc _ (cokernel.π f) (by simp [← h])

Isomorphism of cokernels for equal morphisms

Informal description

Given two equal morphisms $f, g : X \to Y$ in a category with zero morphisms, where both $f$ and $g$ have cokernels, there exists an isomorphism between their cokernel objects $\text{cokernel}(f) \cong \text{cokernel}(g)$.

CategoryTheory.Limits.cokernel.zeroCokernelCofork definition

: CokernelCofork f

Full source

/-- The morphism to the zero object determines a cocone on a cokernel diagram -/
def cokernel.zeroCokernelCofork : CokernelCofork f where
  pt := 0
  ι := { app := fun _ => 0 }

Zero cokernel cofork

Informal description

The cokernel cofork of a morphism $ f : X \to Y $ in a category with zero morphisms, where the cocone object is the zero object and all morphisms in the cocone are zero morphisms.

CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone definition

[Epi f] : IsColimit (cokernel.zeroCokernelCofork f)

Full source

/-- The morphism to the zero object is a cokernel of an epimorphism -/
def cokernel.isColimitCoconeZeroCocone [Epi f] : IsColimit (cokernel.zeroCokernelCofork f) :=
  Cofork.IsColimit.mk _ (fun _ => 0)
    (fun s => by
      erw [zero_comp]
      refine (zero_of_epi_comp f ?_).symm
      exact CokernelCofork.condition _)
    fun _ _ _ => zero_of_from_zero _

Zero cokernel cofork is colimit for epimorphism

Informal description

In a category with zero morphisms, if a morphism $ f : X \to Y $ is an epimorphism, then the zero cokernel cofork (where the cocone object is the zero object and all morphisms are zero morphisms) is a colimit cocone for $ f $. This means that the zero object serves as the cokernel of $ f $ when $ f $ is epic.

CategoryTheory.Limits.cokernel.ofEpi definition

[HasCokernel f] [Epi f] : cokernel f ≅ 0

Full source

/-- The cokernel of an epimorphism is isomorphic to the zero object -/
def cokernel.ofEpi [HasCokernel f] [Epi f] : cokernelcokernel f ≅ 0 :=
  Functor.mapIso (Cocones.forget _) <|
    IsColimit.uniqueUpToIso (colimit.isColimit (parallelPair f 0))
      (cokernel.isColimitCoconeZeroCocone f)

Cokernel of an epimorphism is zero

Informal description

In a category with zero morphisms and a zero object, if a morphism $ f : X \to Y $ is an epimorphism and has a cokernel, then the cokernel of $ f $ is isomorphic to the zero object.

CategoryTheory.Limits.cokernel.π_of_epi theorem

[HasCokernel f] [Epi f] : cokernel.π f = 0

Full source

/-- The cokernel morphism of an epimorphism is a zero morphism -/
theorem cokernel.π_of_epi [HasCokernel f] [Epi f] : cokernel.π f = 0 :=
  zero_of_target_iso_zero _ (cokernel.ofEpi f)

Cokernel Projection of Epimorphism is Zero Morphism

Informal description

In a category with zero morphisms and a zero object, if a morphism $f : X \to Y$ is an epimorphism and has a cokernel, then the cokernel projection $\pi : Y \to \text{cokernel}(f)$ is equal to the zero morphism, i.e., $\pi = 0$.

CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp theorem

[HasKernel f] (F : MonoFactorisation f) : kernel.ι f ≫ F.e = 0

Full source

@[simp]
theorem MonoFactorisation.kernel_ι_comp [HasKernel f] (F : MonoFactorisation f) :
    kernel.ιkernel.ι f ≫ F.e = 0 := by
  rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

Kernel Inclusion Composed with Monomorphism Factorization Morphism is Zero

Informal description

In a category with zero morphisms, given a monomorphism factorization $F$ of a morphism $f \colon X \to Y$ (i.e., $f = F.m \circ F.e$ where $F.m$ is a monomorphism), the composition of the kernel inclusion $\iota \colon \mathrm{kernel}(f) \to X$ with the morphism $F.e \colon X \to F.I$ is the zero morphism, i.e., $\iota \circ F.e = 0$.

CategoryTheory.Limits.cokernelImageι definition

 {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι f)] [HasCokernel f] [Epi (factorThruImage f)] :
  cokernel (image.ι f) ≅ cokernel f

Full source

/-- The cokernel of the image inclusion of a morphism `f` is isomorphic to the cokernel of `f`.

(This result requires that the factorisation through the image is an epimorphism.
This holds in any category with equalizers.)
-/
@[simps]
def cokernelImageι {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι f)] [HasCokernel f]
    [Epi (factorThruImage f)] : cokernelcokernel (image.ι f) ≅ cokernel f where
  hom :=
    cokernel.desc _ (cokernel.π f)
      (by
        have w := cokernel.condition f
        conv at w =>
          lhs
          congr
          rw [← image.fac f]
        rw [← HasZeroMorphisms.comp_zero (Limits.factorThruImage f), Category.assoc,
          cancel_epi] at w
        exact w)
  inv :=
    cokernel.desc _ (cokernel.π _)
      (by
        conv =>
          lhs
          congr
          rw [← image.fac f]
        rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero])

Isomorphism between cokernel of image inclusion and cokernel of morphism

Informal description

Given a morphism $ f : X \to Y $ in a category with zero morphisms, where $ f $ has an image factorization and both $ f $ and its image inclusion $ \iota : \text{image}(f) \to Y $ have cokernels, and the factorization through the image is an epimorphism, the cokernel of the image inclusion $ \iota $ is isomorphic to the cokernel of $ f $.

CategoryTheory.Limits.kernelFactorThruImage definition

: kernel (factorThruImage f) ≅ kernel f

Full source

/-- The kernel of the morphism `X ⟶ image f` is just the kernel of `f`. -/
def kernelFactorThruImage : kernelkernel (factorThruImage f) ≅ kernel f :=
  (kernelCompMono (factorThruImage f) (image.ι f)).symm ≪≫ (kernel.congr _ _ (by simp))

Isomorphism between kernels of morphism and its image factorization

Informal description

The kernel of the morphism $ X \to \text{image}(f) $ is isomorphic to the kernel of $ f $. More precisely, there exists an isomorphism $ \text{kernel}(X \to \text{image}(f)) \cong \text{kernel}(f) $ that commutes with the kernel inclusion morphisms.

CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι theorem

: (kernelFactorThruImage f).hom ≫ kernel.ι f = kernel.ι (factorThruImage f)

Full source

@[reassoc (attr := simp)]
theorem kernelFactorThruImage_hom_comp_ι :
    (kernelFactorThruImage f).hom ≫ kernel.ι f = kernel.ι (factorThruImage f) := by
  simp [kernelFactorThruImage]

Compatibility of Kernel Isomorphism with Kernel Inclusions

Informal description

Let $f : X \to Y$ be a morphism in a category with zero morphisms that has an image factorization. The composition of the homomorphism part of the kernel isomorphism $\text{kernel}(X \to \text{image}(f)) \cong \text{kernel}(f)$ with the kernel inclusion $\iota : \text{kernel}(f) \to X$ equals the kernel inclusion $\iota : \text{kernel}(X \to \text{image}(f)) \to X$.

CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι theorem

: (kernelFactorThruImage f).inv ≫ kernel.ι (factorThruImage f) = kernel.ι f

Full source

@[reassoc (attr := simp)]
theorem kernelFactorThruImage_inv_comp_ι :
    (kernelFactorThruImage f).inv ≫ kernel.ι (factorThruImage f) = kernel.ι f := by
  simp [kernelFactorThruImage]

Compatibility of Kernel Isomorphism Inverse with Kernel Inclusions

Informal description

Let $\mathcal{C}$ be a category with zero morphisms and let $f : X \to Y$ be a morphism in $\mathcal{C}$ that has an image factorization. The inverse of the isomorphism $\text{kernel}(X \to \text{image}(f)) \cong \text{kernel}(f)$, when composed with the kernel inclusion $\iota : \text{kernel}(X \to \text{image}(f)) \to X$, equals the kernel inclusion $\iota : \text{kernel}(f) \to X$. In symbols, if $\varphi := \text{kernelFactorThruImage}(f)^{-1}$, then $\varphi \circ \iota_{X \to \text{image}(f)} = \iota_f$.

CategoryTheory.Limits.cokernel.π_of_zero theorem

: IsIso (cokernel.π (0 : X ⟶ Y))

Full source

/-- The cokernel of a zero morphism is an isomorphism -/
theorem cokernel.π_of_zero : IsIso (cokernel.π (0 : X ⟶ Y)) :=
  coequalizer.π_of_self _

Cokernel Projection of Zero Morphism is Isomorphism

Informal description

In a category with zero morphisms, the cokernel projection $\pi : Y \to \text{cokernel}(0)$ of the zero morphism $0 : X \to Y$ is an isomorphism.

CategoryTheory.Limits.kernel.of_cokernel_of_epi instance

[HasCokernel f] [HasKernel (cokernel.π f)] [Epi f] : IsIso (kernel.ι (cokernel.π f))

Full source

/-- The kernel of the cokernel of an epimorphism is an isomorphism -/
instance kernel.of_cokernel_of_epi [HasCokernel f] [HasKernel (cokernel.π f)] [Epi f] :
    IsIso (kernel.ι (cokernel.π f)) :=
  equalizer.ι_of_eq <| cokernel.π_of_epi f

Kernel of Cokernel Projection is Isomorphism for Epimorphisms

Informal description

In a category with zero morphisms and a zero object, given an epimorphism $f : X \to Y$ that has a cokernel, the kernel inclusion $\iota : \text{kernel}(\pi) \to Y$ of the cokernel projection $\pi : Y \to \text{cokernel}(f)$ is an isomorphism.

CategoryTheory.Limits.cokernel.of_kernel_of_mono instance

[HasKernel f] [HasCokernel (kernel.ι f)] [Mono f] : IsIso (cokernel.π (kernel.ι f))

Full source

/-- The cokernel of the kernel of a monomorphism is an isomorphism -/
instance cokernel.of_kernel_of_mono [HasKernel f] [HasCokernel (kernel.ι f)] [Mono f] :
    IsIso (cokernel.π (kernel.ι f)) :=
  coequalizer.π_of_eq <| kernel.ι_of_mono f

Cokernel of Kernel Inclusion for Monomorphism is Isomorphism

Informal description

In a category with zero morphisms and a zero object, for any monomorphism $f : X \to Y$ that has a kernel and whose kernel inclusion $\iota : \text{kernel}(f) \to X$ has a cokernel, the cokernel projection $\pi : X \to \text{cokernel}(\iota)$ is an isomorphism.

CategoryTheory.Limits.zeroCokernelOfZeroCancel definition

 {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z) (_ : f ≫ g = 0), g = 0) :
  IsColimit (CokernelCofork.ofπ (0 : Y ⟶ 0) (show f ≫ 0 = 0 by simp))

Full source

/-- If `f ≫ g = 0` implies `g = 0` for all `g`, then `0 : Y ⟶ 0` is a cokernel of `f`. -/
def zeroCokernelOfZeroCancel {X Y : C} (f : X ⟶ Y)
    (hf : ∀ (Z : C) (g : Y ⟶ Z) (_ : f ≫ g = 0), g = 0) :
    IsColimit (CokernelCofork.ofπ (0 : Y ⟶ 0) (show f ≫ 0 = 0 by simp)) :=
  Cofork.IsColimit.mk _ (fun _ => 0)
    (fun s => by rw [hf _ _ (CokernelCofork.condition s), comp_zero]) fun s m _ => by
      apply HasZeroObject.from_zero_ext

Zero morphism as cokernel under zero-cancellation condition

Informal description

Given a morphism $ f \colon X \to Y $ in a category $ C $ with zero morphisms and a zero object, if for every object $ Z $ and every morphism $ g \colon Y \to Z $ the condition $ f \circ g = 0 $ implies $ g = 0 $, then the zero morphism $ 0 \colon Y \to 0 $ is a cokernel of $ f $.

CategoryTheory.Limits.IsCokernel.ofIsoComp definition

 {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : i.hom ≫ l = f) {s : CokernelCofork f} (hs : IsColimit s) :
  IsColimit (CokernelCofork.ofπ (Cofork.π s) <| show l ≫ Cofork.π s = 0 by simp [i.eq_inv_comp.2 h])

Full source

/-- If `i` is an isomorphism such that `i.hom ≫ l = f`, then any cokernel of `f` is a cokernel of
    `l`. -/
def IsCokernel.ofIsoComp {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : i.hom ≫ l = f) {s : CokernelCofork f}
    (hs : IsColimit s) :
    IsColimit
      (CokernelCofork.ofπ (Cofork.π s) <| show l ≫ Cofork.π s = 0 by simp [i.eq_inv_comp.2 h]) :=
  Cofork.IsColimit.mk _ (fun s => hs.desc <| CokernelCofork.ofπ (Cofork.π s) <| by simp [← h])
    (fun s => by simp) fun s m h => by
      apply Cofork.IsColimit.hom_ext hs
      simpa using h

Cokernel preservation under isomorphism composition

Informal description

Given an isomorphism $i \colon X \cong Z$ such that $i_{\text{hom}} \circ l = f$, and a colimit cokernel cofork $s$ of $f$, then the cokernel cofork obtained by composing $l$ with the projection $\pi_s$ of $s$ is also a colimit. In other words, any cokernel of $f$ is also a cokernel of $l$ under these conditions.

CategoryTheory.Limits.cokernel.ofIsoComp definition

 [HasCokernel f] {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : i.hom ≫ l = f) :
  IsColimit (CokernelCofork.ofπ (cokernel.π f) <| show l ≫ cokernel.π f = 0 by simp [i.eq_inv_comp.2 h])

Full source

/-- If `i` is an isomorphism such that `i.hom ≫ l = f`, then the cokernel of `f` is a cokernel of
    `l`. -/
def cokernel.ofIsoComp [HasCokernel f] {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : i.hom ≫ l = f) :
    IsColimit
      (CokernelCofork.ofπ (cokernel.π f) <|
        show l ≫ cokernel.π f = 0 by simp [i.eq_inv_comp.2 h]) :=
  IsCokernel.ofIsoComp f l i h <| colimit.isColimit _

Cokernel preservation under isomorphism composition

Informal description

Given a morphism $f \colon X \to Y$ in a category with zero morphisms, suppose there exists an isomorphism $i \colon X \cong Z$ and a morphism $l \colon Z \to Y$ such that $i_{\text{hom}} \circ l = f$. If the cokernel of $f$ exists, then the cokernel projection $\pi_f \colon Y \to \text{cokernel}(f)$ also serves as a cokernel for $l$, meaning that $l \circ \pi_f = 0$ and $\pi_f$ satisfies the universal property of a cokernel for $l$.

CategoryTheory.Limits.IsCokernel.cokernelIso definition

 {Z : C} (l : Y ⟶ Z) {s : CokernelCofork f} (hs : IsColimit s) (i : s.pt ≅ Z) (h : Cofork.π s ≫ i.hom = l) :
  IsColimit (CokernelCofork.ofπ l <| show f ≫ l = 0 by simp [← h])

Full source

/-- If `s` is any colimit cokernel cocone over `f` and `i` is an isomorphism such that
    `s.π ≫ i.hom = l`, then `l` is a cokernel of `f`. -/
def IsCokernel.cokernelIso {Z : C} (l : Y ⟶ Z) {s : CokernelCofork f} (hs : IsColimit s)
    (i : s.pt ≅ Z) (h : Cofork.πCofork.π s ≫ i.hom = l) :
    IsColimit (CokernelCofork.ofπ l <| show f ≫ l = 0 by simp [← h]) :=
  IsColimit.ofIsoColimit hs <|
    Cocones.ext i fun j => by
      cases j
      · dsimp; rw [← h]; simp
      · exact h

Cokernel property preserved under isomorphism

Informal description

Given a morphism $ f : X \to Y $ in a category with zero morphisms, a morphism $ l : Y \to Z $, a cokernel cofork $ s $ for $ f $ with colimit property $ hs $, and an isomorphism $ i : s.pt \cong Z $ such that the cofork projection $ \pi_s $ composed with $ i.hom $ equals $ l $, then $ l $ is a cokernel of $ f $. Specifically, the cokernel cofork constructed from $ l $ and the condition $ f \circ l = 0 $ is a colimit cocone.

CategoryTheory.Limits.cokernel.cokernelIso definition

 [HasCokernel f] {Z : C} (l : Y ⟶ Z) (i : cokernel f ≅ Z) (h : cokernel.π f ≫ i.hom = l) :
  IsColimit (@CokernelCofork.ofπ _ _ _ _ _ f _ l <| by simp [← h])

Full source

/-- If `i` is an isomorphism such that `cokernel.π f ≫ i.hom = l`, then `l` is a cokernel of `f`. -/
def cokernel.cokernelIso [HasCokernel f] {Z : C} (l : Y ⟶ Z) (i : cokernelcokernel f ≅ Z)
    (h : cokernel.πcokernel.π f ≫ i.hom = l) :
    IsColimit (@CokernelCofork.ofπ _ _ _ _ _ f _ l <| by simp [← h]) :=
  IsCokernel.cokernelIso f l (colimit.isColimit _) i h

Cokernel property preserved under isomorphism

Informal description

Given a morphism $ f : X \to Y $ in a category with zero morphisms, suppose $ f $ has a cokernel. For any object $ Z $ and morphism $ l : Y \to Z $, if there exists an isomorphism $ i : \text{cokernel}(f) \cong Z $ such that the cokernel projection $ \pi : Y \to \text{cokernel}(f) $ composed with $ i $ equals $ l $, then $ l $ is a cokernel of $ f $. In other words, the cokernel cofork constructed from $ l $ and the condition $ f \circ l = 0 $ is a colimit cocone.

CategoryTheory.Limits.kernelComparison definition

[HasKernel f] [HasKernel (G.map f)] : G.obj (kernel f) ⟶ kernel (G.map f)

Full source

/-- The comparison morphism for the kernel of `f`.
This is an isomorphism iff `G` preserves the kernel of `f`; see
`CategoryTheory/Limits/Preserves/Shapes/Kernels.lean`
-/
def kernelComparison [HasKernel f] [HasKernel (G.map f)] : G.obj (kernel f) ⟶ kernel (G.map f) :=
  kernel.lift _ (G.map (kernel.ι f))
    (by simp only [← G.map_comp, kernel.condition, Functor.map_zero])

Kernel Comparison Morphism

Informal description

Given a functor $ G : C \to D $ between categories with zero morphisms, and a morphism $ f : X \to Y $ in $ C $ that has a kernel, the *kernel comparison morphism* is the canonical morphism $ G(\text{kernel}(f)) \to \text{kernel}(G(f)) $ in $ D $. This morphism is constructed using the universal property of the kernel of $ G(f) $, applied to the image under $ G $ of the kernel inclusion $ \iota : \text{kernel}(f) \to X $.

CategoryTheory.Limits.kernelComparison_comp_ι theorem

[HasKernel f] [HasKernel (G.map f)] : kernelComparison f G ≫ kernel.ι (G.map f) = G.map (kernel.ι f)

Full source

@[reassoc (attr := simp)]
theorem kernelComparison_comp_ι [HasKernel f] [HasKernel (G.map f)] :
    kernelComparisonkernelComparison f G ≫ kernel.ι (G.map f) = G.map (kernel.ι f) :=
  kernel.lift_ι _ _ _

Composition of Kernel Comparison with Kernel Inclusion Equals Image of Kernel Inclusion

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with zero morphisms, and let $G : \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. Given a morphism $f : X \to Y$ in $\mathcal{C}$ that has a kernel, and assuming $G(f)$ also has a kernel in $\mathcal{D}$, the composition of the kernel comparison morphism $\text{kernelComparison}(f, G) : G(\text{kernel}(f)) \to \text{kernel}(G(f))$ with the kernel inclusion $\iota_{G(f)} : \text{kernel}(G(f)) \to G(X)$ equals the image under $G$ of the kernel inclusion $\iota_f : \text{kernel}(f) \to X$, i.e., \[ \text{kernelComparison}(f, G) \circ \iota_{G(f)} = G(\iota_f). \]

CategoryTheory.Limits.map_lift_kernelComparison theorem

 [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X} (w : h ≫ f = 0) :
  G.map (kernel.lift _ h w) ≫ kernelComparison f G =
    kernel.lift _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero])

Full source

@[reassoc (attr := simp)]
theorem map_lift_kernelComparison [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X}
    (w : h ≫ f = 0) :
    G.map (kernel.lift _ h w) ≫ kernelComparison f G =
      kernel.lift _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) := by
  ext; simp [← G.map_comp]

Naturality of Kernel Lift with Respect to Functor Application: $G(\text{lift}) \circ \text{comparison} = \text{lift}(G(h))$

Informal description

Let $\mathcal{C}$ and $\mathcal{D}$ be categories with zero morphisms, and let $G : \mathcal{C} \to \mathcal{D}$ be a functor that preserves zero morphisms. Given a morphism $f : X \to Y$ in $\mathcal{C}$ that has a kernel, and assuming $G(f)$ also has a kernel in $\mathcal{D}$, then for any object $Z$ in $\mathcal{C}$ and morphism $h : Z \to X$ satisfying $h \circ f = 0$, the following diagram commutes: \[ G(\text{kernel.lift}(f, h, w)) \circ \text{kernelComparison}(f, G) = \text{kernel.lift}(G(f), G(h), \text{by simp only } [\leftarrow G.map_comp, w, Functor.map_zero]) \] where $w$ is the proof that $h \circ f = 0$.

CategoryTheory.Limits.cokernelComparison definition

[HasCokernel f] [HasCokernel (G.map f)] : cokernel (G.map f) ⟶ G.obj (cokernel f)

Full source

/-- The comparison morphism for the cokernel of `f`. -/
def cokernelComparison [HasCokernel f] [HasCokernel (G.map f)] :
    cokernelcokernel (G.map f) ⟶ G.obj (cokernel f) :=
  cokernel.desc _ (G.map (coequalizer.π _ _))
    (by simp only [← G.map_comp, cokernel.condition, Functor.map_zero])

Comparison morphism for cokernels under a functor

Informal description

Given a functor $ G : C \to D $ between categories with zero morphisms, and a morphism $ f : X \to Y $ in $ C $ that has a cokernel, the comparison morphism $ \text{cokernelComparison} $ is the unique morphism from the cokernel of $ G(f) $ in $ D $ to $ G $ applied to the cokernel of $ f $ in $ C $. This morphism satisfies the condition that the composition of the cokernel projection $ \pi $ of $ G(f) $ with $ \text{cokernelComparison} $ equals $ G $ applied to the cokernel projection $ \pi $ of $ f $.

CategoryTheory.Limits.π_comp_cokernelComparison theorem

[HasCokernel f] [HasCokernel (G.map f)] : cokernel.π (G.map f) ≫ cokernelComparison f G = G.map (cokernel.π _)

Full source

@[reassoc (attr := simp)]
theorem π_comp_cokernelComparison [HasCokernel f] [HasCokernel (G.map f)] :
    cokernel.πcokernel.π (G.map f) ≫ cokernelComparison f G = G.map (cokernel.π _) :=
  cokernel.π_desc _ _ _

Commutativity of Cokernel Projection with Comparison Morphism under Functor $G$

Informal description

Let $G \colon C \to D$ be a functor between categories with zero morphisms, and let $f \colon X \to Y$ be a morphism in $C$ that has a cokernel. Suppose $G(f)$ also has a cokernel in $D$. Then the composition of the cokernel projection $\pi \colon Y \to \text{cokernel}(G(f))$ with the comparison morphism $\text{cokernelComparison}(f, G) \colon \text{cokernel}(G(f)) \to G(\text{cokernel}(f))$ equals $G$ applied to the cokernel projection $\pi \colon Y \to \text{cokernel}(f)$.

CategoryTheory.Limits.cokernelComparison_map_desc theorem

 [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z} (w : f ≫ h = 0) :
  cokernelComparison f G ≫ G.map (cokernel.desc _ h w) =
    cokernel.desc _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero])

Full source

@[reassoc (attr := simp)]
theorem cokernelComparison_map_desc [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z}
    (w : f ≫ h = 0) :
    cokernelComparisoncokernelComparison f G ≫ G.map (cokernel.desc _ h w) =
      cokernel.desc _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) := by
  ext; simp [← G.map_comp]

Naturality of Cokernel Comparison with Respect to Descending Morphisms

Informal description

Let $G \colon C \to D$ be a functor between categories with zero morphisms, and let $f \colon X \to Y$ be a morphism in $C$ that has a cokernel. Suppose $G(f)$ also has a cokernel in $D$. Given a morphism $h \colon Y \to Z$ in $C$ such that $f \circ h = 0$, the following diagram commutes: \[ \text{cokernelComparison}(f, G) \circ G(\text{cokernel.desc}(f, h, w)) = \text{cokernel.desc}(G(f), G(h), \text{by simp}) \] where $w$ is the proof that $f \circ h = 0$.

CategoryTheory.Limits.cokernel_map_comp_cokernelComparison theorem

 {X' Y' : C} [HasCokernel f] [HasCokernel (G.map f)] (g : X' ⟶ Y') [HasCokernel g] [HasCokernel (G.map g)] (p : X ⟶ X')
  (q : Y ⟶ Y') (hpq : f ≫ q = p ≫ g) :
  cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) ≫
      cokernelComparison _ G =
    cokernelComparison _ G ≫ G.map (cokernel.map f g p q hpq)

Full source

@[reassoc]
theorem cokernel_map_comp_cokernelComparison {X' Y' : C} [HasCokernel f] [HasCokernel (G.map f)]
    (g : X' ⟶ Y') [HasCokernel g] [HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y')
    (hpq : f ≫ q = p ≫ g) :
    cokernel.mapcokernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) ≫
        cokernelComparison _ G =
      cokernelComparisoncokernelComparison _ G ≫ G.map (cokernel.map f g p q hpq) :=
  cokernel.map_desc _ _ (by rw [← G.map_comp, cokernel.condition, G.map_zero]) _ _
    (by rw [← G.map_comp, cokernel.condition, G.map_zero]) _ _ _ _
    (by simp only [← G.map_comp]; exact G.congr_map (cokernel.π_desc _ _ _))

Naturality of Cokernel Comparison with Respect to Functor Application

Informal description

Let $C$ and $D$ be categories with zero morphisms, and let $G \colon C \to D$ be a functor that preserves zero morphisms. Given morphisms $f \colon X \to Y$ in $C$ and $g \colon X' \to Y'$ in $C$ with cokernels, and morphisms $p \colon X \to X'$, $q \colon Y \to Y'$ such that $f \circ q = p \circ g$, the following diagram commutes: \[ \text{cokernel.map}(G(f), G(g), G(p), G(q)) \circ \text{cokernelComparison}(f, G) = \text{cokernelComparison}(g, G) \circ G(\text{cokernel.map}(f, g, p, q)) \] where $\text{cokernelComparison}(f, G) \colon \text{cokernel}(G(f)) \to G(\text{cokernel}(f))$ is the comparison morphism induced by $G$.

CategoryTheory.Limits.HasKernels structure

Full source

/-- `HasKernels` represents the existence of kernels for every morphism. -/
class HasKernels : Prop where
  has_limit : ∀ {X Y : C} (f : X ⟶ Y), HasKernel f := by infer_instance

Category with kernels

Informal description

A category $ C $ is said to "have kernels" if for every morphism $ f: X \to Y $ in $ C $, there exists a kernel object $ \text{kernel}(f) $ and a kernel morphism $ \iota: \text{kernel}(f) \to X $ satisfying the universal property that for any morphism $ k: W \to X $ with $ k \circ f = 0 $, there exists a unique lift $ \text{lift}(k): W \to \text{kernel}(f) $ such that $ \text{lift}(k) \circ \iota = k $.

CategoryTheory.Limits.HasCokernels structure

Full source

/-- `HasCokernels` represents the existence of cokernels for every morphism. -/
class HasCokernels : Prop where
  has_colimit : ∀ {X Y : C} (f : X ⟶ Y), HasCokernel f := by infer_instance

Category with Cokernels

Informal description

A category $ C $ is said to "have cokernels" if for every morphism $ f : X \to Y $ in $ C $, the cokernel of $ f $ exists. The cokernel of $ f $ is the coequalizer of $ f $ and the zero morphism $ 0 : X \to Y $, which is a universal morphism that makes the diagram commute.

CategoryTheory.Limits.hasKernels_of_hasEqualizers instance

[HasEqualizers C] : HasKernels C

Full source

instance (priority := 100) hasKernels_of_hasEqualizers [HasEqualizers C] : HasKernels C where

Existence of Kernels in Categories with Equalizers

Informal description

In a category $\mathcal{C}$ with equalizers, every morphism has a kernel. That is, for any morphism $f : X \to Y$ in $\mathcal{C}$, there exists an object $\text{kernel}(f)$ and a morphism $\iota : \text{kernel}(f) \to X$ such that $\iota \circ f = 0$, and $\text{kernel}(f)$ is universal with this property.

CategoryTheory.Limits.hasCokernels_of_hasCoequalizers instance

[HasCoequalizers C] : HasCokernels C

Full source

instance (priority := 100) hasCokernels_of_hasCoequalizers [HasCoequalizers C] :
    HasCokernels C where

Existence of Cokernels from Coequalizers

Informal description

In any category $\mathcal{C}$ with coequalizers, $\mathcal{C}$ also has cokernels for all morphisms. Specifically, the cokernel of a morphism $f : X \to Y$ is given by the coequalizer of $f$ and the zero morphism $0 : X \to Y$.

Mathlib.CategoryTheory.Limits.Shapes.Kernels

Main statements

Future work

Implementation notes

References