# mathlib3documentation

category_theory.limits.shapes.kernels

# Kernels and cokernels #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In a category with zero morphisms, the kernel of a morphism `f : X ⟶ Y` is the equalizer of `f` and `0 : X ⟶ Y`. (Similarly the cokernel is the coequalizer.)

The basic definitions are

• `kernel : (X ⟶ Y) → C`

• `kernel.ι : kernel f ⟶ X`

• `kernel.condition : kernel.ι f ≫ f = 0` and

• `kernel.lift (k : W ⟶ X) (h : k ≫ f = 0) : W ⟶ kernel f` (as well as the dual versions)

## Main statements #

Besides the definition and lifts, we prove

• `kernel.ι_zero_is_iso`: a kernel map of a zero morphism is an isomorphism
• `kernel.eq_zero_of_epi_kernel`: if `kernel.ι f` is an epimorphism, then `f = 0`
• `kernel.of_mono`: the kernel of a monomorphism is the zero object
• `kernel.lift_mono`: the lift of a monomorphism `k : W ⟶ X` such that `k ≫ f = 0` is still a monomorphism
• `kernel.is_limit_cone_zero_cone`: if our category has a zero object, then the map from the zero obect is a kernel map of any monomorphism
• `kernel.ι_of_zero`: `kernel.ι (0 : X ⟶ Y)` is an isomorphism

and the corresponding dual statements.

## Future work #

• TODO: connect this with existing working in the group theory and ring theory libraries.

## Implementation notes #

As with the other special shapes in the limits library, all the definitions here are given as `abbreviation`s of the general statements for limits, so all the `simp` lemmas and theorems about general limits can be used.

## References #

@[reducible]
def category_theory.limits.has_kernel {C : Type u} {X Y : C} (f : X Y) :
Prop

A morphism `f` has a kernel if the functor `parallel_pair f 0` has a limit.

@[reducible]
def category_theory.limits.has_cokernel {C : Type u} {X Y : C} (f : X Y) :
Prop

A morphism `f` has a cokernel if the functor `parallel_pair f 0` has a colimit.

@[reducible]
def category_theory.limits.kernel_fork {C : Type u} {X Y : C} (f : X Y) :
Type (max u v)

A kernel fork is just a fork where the second morphism is a zero morphism.

@[simp]
theorem category_theory.limits.kernel_fork.condition {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.kernel_fork.condition_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C} (f' : Y X') :
= 0 f'
@[simp]
theorem category_theory.limits.kernel_fork.app_one {C : Type u} {X Y : C} {f : X Y}  :
@[reducible]
def category_theory.limits.kernel_fork.of_ι {C : Type u} {X Y : C} {f : X Y} {Z : C} (ι : Z X) (w : ι f = 0) :

A morphism `ι` satisfying `ι ≫ f = 0` determines a kernel fork over `f`.

@[simp]
theorem category_theory.limits.kernel_fork.ι_of_ι {C : Type u} {X Y P : C} (f : X Y) (ι : P X) (w : ι f = 0) :
def category_theory.limits.iso_of_ι {C : Type u} {X Y : C} {f : X Y} (s : 0) :

Every kernel fork `s` is isomorphic (actually, equal) to `fork.of_ι (fork.ι s) _`.

Equations
def category_theory.limits.of_ι_congr {C : Type u} {X Y : C} {f : X Y} {P : C} {ι ι' : P X} {w : ι f = 0} (h : ι = ι') :

If `ι = ι'`, then `fork.of_ι ι _` and `fork.of_ι ι' _` are isomorphic.

Equations
def category_theory.limits.comp_nat_iso {C : Type u} {X Y : C} {f : X Y} {D : Type u'} (F : C D)  :

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`.

Equations
def category_theory.limits.kernel_fork.is_limit.lift' {C : Type u} {X Y : C} {f : X Y} {W : C} (k : W X) (h : k f = 0) :
{l //

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`.

Equations
def category_theory.limits.is_limit_aux {C : Type u} {X Y : C} {f : X Y} (lift : Π (s : , s.X t.X) (fac : (s : , ) (uniq : (s : (m : s.X t.X), m = lift s) :

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

Equations
def category_theory.limits.kernel_fork.is_limit.of_ι {C : Type u} {X Y : C} {f : X Y} {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') :

This is a more convenient formulation to show that a `kernel_fork` constructed using `kernel_fork.of_ι` is a limit cone.

Equations
• fac uniq = _ _
def category_theory.limits.is_kernel_comp_mono {C : Type u} {X Y : C} {f : X Y} {Z : C} (g : Y Z) [hg : category_theory.mono g] {h : X Z} (hh : h = f g) :

Every kernel of `f` induces a kernel of `f ≫ g` if `g` is mono.

Equations
• = (λ (s : , let s' : := , l : {l // := in l.val, _⟩)
theorem category_theory.limits.is_kernel_comp_mono_lift {C : Type u} {X Y : C} {f : X Y} {Z : C} (g : Y Z) [hg : category_theory.mono g] {h : X Z} (hh : h = f g)  :
def category_theory.limits.is_kernel_of_comp {C : Type u} {X Y : C} {f : X Y} {W : C} (g : Y W) (h : X W) (hf : = 0) (hfg : f g = h) :

Every kernel of `f ≫ g` is also a kernel of `f`, as long as `c.ι ≫ f` vanishes.

Equations
• hfg =
@[reducible]
noncomputable def category_theory.limits.kernel {C : Type u} {X Y : C} (f : X Y)  :
C

The kernel of a morphism, expressed as the equalizer with the 0 morphism.

@[reducible]
noncomputable def category_theory.limits.kernel.ι {C : Type u} {X Y : C} (f : X Y)  :

The map from `kernel f` into the source of `f`.

@[simp]
theorem category_theory.limits.equalizer_as_kernel {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.kernel.condition_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
= 0 f'
@[simp]
theorem category_theory.limits.kernel.condition {C : Type u} {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.kernel_is_kernel {C : Type u} {X Y : C} (f : X Y)  :

The kernel built from `kernel.ι f` is limiting.

Equations
@[reducible]
noncomputable def category_theory.limits.kernel.lift {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0) :

Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through `kernel.ι f` via `kernel.lift : W ⟶ kernel f`.

@[simp]
theorem category_theory.limits.kernel.lift_ι {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0) :
@[simp]
theorem category_theory.limits.kernel.lift_ι_assoc {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0) {X' : C} (f' : X X') :
= k f'
@[simp]
theorem category_theory.limits.kernel.lift_zero {C : Type u} {X Y : C} (f : X Y) {W : C} {h : 0 f = 0} :
@[protected, instance]
def category_theory.limits.kernel.lift_mono {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0)  :
noncomputable def category_theory.limits.kernel.lift' {C : Type u} {X Y : C} (f : X Y) {W : C} (k : W X) (h : k f = 0) :
{l //

Any morphism `k : W ⟶ X` satisfying `k ≫ f = 0` induces a morphism `l : W ⟶ kernel f` such that `l ≫ kernel.ι f = k`.

Equations
@[reducible]
noncomputable def category_theory.limits.kernel.map {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q = p f') :

A commuting square induces a morphism of kernels.

theorem category_theory.limits.kernel.lift_map {C : Type u} {X Y Z X' Y' Z' : C} (f : X Y) (g : Y Z) (w : f g = 0) (f' : X' Y') (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') :
h₂ = p

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'

@[simp]
theorem category_theory.limits.kernel.map_iso_hom {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :
w).hom = q.hom w
noncomputable def category_theory.limits.kernel.map_iso {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :

A commuting square of isomorphisms induces an isomorphism of kernels.

Equations
@[simp]
theorem category_theory.limits.kernel.map_iso_inv {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :
w).inv = q.inv _
@[protected, instance]

Every kernel of the zero morphism is an isomorphism

theorem category_theory.limits.eq_zero_of_epi_kernel {C : Type u} {X Y : C} (f : X Y)  :
f = 0
noncomputable def category_theory.limits.kernel_zero_iso_source {C : Type u} {X Y : C} :

The kernel of a zero morphism is isomorphic to the source.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.kernel_iso_of_eq {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

If two morphisms are known to be equal, then their kernels are isomorphic.

Equations
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_refl {C : Type u} {X Y : C} (f : X Y) {h : f = f} :
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_hom_comp_ι {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_hom_comp_ι_assoc {C : Type u} {X Y : C} {f g : X Y} (h : f = g) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_inv_comp_ι {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_inv_comp_ι_assoc {C : Type u} {X Y : C} {f g : X Y} (h : f = g) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.lift_comp_kernel_iso_of_eq_hom {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Z X) (he : e f = 0) :
@[simp]
theorem category_theory.limits.lift_comp_kernel_iso_of_eq_hom_assoc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Z X) (he : e f = 0) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.lift_comp_kernel_iso_of_eq_inv_assoc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Z X) (he : e g = 0) {X' : C} (f' : X') :
@[simp]
theorem category_theory.limits.lift_comp_kernel_iso_of_eq_inv {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Z X) (he : e g = 0) :
@[simp]
theorem category_theory.limits.kernel_iso_of_eq_trans {C : Type u} {X Y : C} {f g h : X Y} (w₁ : f = g) (w₂ : g = h) :
theorem category_theory.limits.kernel_not_epi_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
theorem category_theory.limits.kernel_not_iso_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
@[protected, instance]
def category_theory.limits.has_kernel_comp_mono {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
noncomputable def category_theory.limits.kernel_comp_mono {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

When `g` is a monomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.

Equations
@[simp]
theorem category_theory.limits.kernel_comp_mono_hom {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[simp]
theorem category_theory.limits.kernel_comp_mono_inv {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[protected, instance]
def category_theory.limits.has_kernel_iso_comp {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[simp]
theorem category_theory.limits.kernel_is_iso_comp_inv {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
noncomputable def category_theory.limits.kernel_is_iso_comp {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

When `f` is an isomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `g`.

Equations
@[simp]
theorem category_theory.limits.kernel_is_iso_comp_hom {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
noncomputable def category_theory.limits.kernel.zero_kernel_fork {C : Type u} {X Y : C} (f : X Y)  :

The morphism from the zero object determines a cone on a kernel diagram

Equations
noncomputable def category_theory.limits.kernel.is_limit_cone_zero_cone {C : Type u} {X Y : C} (f : X Y)  :

The map from the zero object is a kernel of a monomorphism

Equations
noncomputable def category_theory.limits.kernel.of_mono {C : Type u} {X Y : C} (f : X Y)  :

The kernel of a monomorphism is isomorphic to the zero object

Equations
theorem category_theory.limits.kernel.ι_of_mono {C : Type u} {X Y : C} (f : X Y)  :

The kernel morphism of a monomorphism is a zero morphism

noncomputable def category_theory.limits.zero_kernel_of_cancel_zero {C : Type u} {X Y : C} (f : X Y) (hf : (Z : C) (g : Z X), g f = 0 g = 0) :

If `g ≫ f = 0` implies `g = 0` for all `g`, then `0 : 0 ⟶ X` is a kernel of `f`.

Equations
def category_theory.limits.is_kernel.of_comp_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : X Z) (i : Z Y) (h : l i.hom = f)  :

If `i` is an isomorphism such that `l ≫ i.hom = f`, then any kernel of `f` is a kernel of `l`.

Equations
• = _
noncomputable def category_theory.limits.kernel.of_comp_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : X Z) (i : Z Y) (h : l i.hom = f) :

If `i` is an isomorphism such that `l ≫ i.hom = f`, then the kernel of `f` is a kernel of `l`.

Equations
def category_theory.limits.is_kernel.iso_kernel {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Z X) (i : Z s.X) (h : = l) :

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`.

Equations
noncomputable def category_theory.limits.kernel.iso_kernel {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Z X) (i : Z ) (h : = l) :

If `i` is an isomorphism such that `i.hom ≫ kernel.ι f = l`, then `l` is a kernel of `f`.

Equations

The kernel morphism of a zero morphism is an isomorphism

@[reducible]
def category_theory.limits.cokernel_cofork {C : Type u} {X Y : C} (f : X Y) :
Type (max u v)

A cokernel cofork is just a cofork where the second morphism is a zero morphism.

@[simp]
theorem category_theory.limits.cokernel_cofork.condition_assoc {C : Type u} {X Y : C} {f : X Y} {X' : C}  :
= 0 f'
@[simp]
theorem category_theory.limits.cokernel_cofork.condition {C : Type u} {X Y : C} {f : X Y}  :
@[simp]
theorem category_theory.limits.cokernel_cofork.π_eq_zero {C : Type u} {X Y : C} {f : X Y}  :
@[reducible]
def category_theory.limits.cokernel_cofork.of_π {C : Type u} {X Y : C} {f : X Y} {Z : C} (π : Y Z) (w : f π = 0) :

A morphism `π` satisfying `f ≫ π = 0` determines a cokernel cofork on `f`.

@[simp]
theorem category_theory.limits.cokernel_cofork.π_of_π {C : Type u} {X Y P : C} (f : X Y) (π : Y P) (w : f π = 0) :
def category_theory.limits.iso_of_π {C : Type u} {X Y : C} {f : X Y} (s : 0) :

Every cokernel cofork `s` is isomorphic (actually, equal) to `cofork.of_π (cofork.π s) _`.

Equations
def category_theory.limits.of_π_congr {C : Type u} {X Y : C} {f : X Y} {P : C} {π π' : Y P} {w : f π = 0} (h : π = π') :

If `π = π'`, then `cokernel_cofork.of_π π _` and `cokernel_cofork.of_π π' _` are isomorphic.

Equations
def category_theory.limits.cokernel_cofork.is_colimit.desc' {C : Type u} {X Y : C} {f : X Y} {W : C} (k : Y W) (h : f k = 0) :
{l //

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`.

Equations
def category_theory.limits.is_colimit_aux {C : Type u} {X Y : C} {f : X Y} (desc : Π (s : , t.X s.X) (fac : (s : , ) (uniq : (s : (m : t.X s.X), m = desc s) :

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

Equations
def category_theory.limits.cokernel_cofork.is_colimit.of_π {C : Type u} {X Y : C} {f : X Y} {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') :

This is a more convenient formulation to show that a `cokernel_cofork` constructed using `cokernel_cofork.of_π` is a limit cone.

Equations
• uniq =
def category_theory.limits.is_cokernel_epi_comp {C : Type u} {X Y : C} {f : X Y} {W : C} (g : W X) [hg : category_theory.epi g] {h : W Y} (hh : h = g f) :

Every cokernel of `f` induces a cokernel of `g ≫ f` if `g` is epi.

Equations
@[simp]
theorem category_theory.limits.is_cokernel_epi_comp_desc {C : Type u} {X Y : C} {f : X Y} {W : C} (g : W X) [hg : category_theory.epi g] {h : W Y} (hh : h = g f)  :
def category_theory.limits.is_cokernel_of_comp {C : Type u} {X Y : C} {f : X Y} {W : C} (g : W X) (h : W Y) (hf : = 0) (hfg : g f = h) :

Every cokernel of `g ≫ f` is also a cokernel of `f`, as long as `f ≫ c.π` vanishes.

Equations
@[reducible]
noncomputable def category_theory.limits.cokernel {C : Type u} {X Y : C} (f : X Y)  :
C

The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.

@[reducible]
noncomputable def category_theory.limits.cokernel.π {C : Type u} {X Y : C} (f : X Y)  :

The map from the target of `f` to `cokernel f`.

@[simp]
@[simp]
theorem category_theory.limits.cokernel.condition {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.cokernel.condition_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : X') :
= 0 f'
noncomputable def category_theory.limits.cokernel_is_cokernel {C : Type u} {X Y : C} (f : X Y)  :

The cokernel built from `cokernel.π f` is colimiting.

Equations
@[reducible]
noncomputable def category_theory.limits.cokernel.desc {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0) :

Given any morphism `k : Y ⟶ W` such that `f ≫ k = 0`, `k` factors through `cokernel.π f` via `cokernel.desc : cokernel f ⟶ W`.

@[simp]
theorem category_theory.limits.cokernel.π_desc {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0) :
@[simp]
theorem category_theory.limits.cokernel.π_desc_assoc {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0) {X' : C} (f' : W X') :
= k f'
@[simp]
theorem category_theory.limits.cokernel.desc_zero {C : Type u} {X Y : C} (f : X Y) {W : C} {h : f 0 = 0} :
@[protected, instance]
def category_theory.limits.cokernel.desc_epi {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0)  :
noncomputable def category_theory.limits.cokernel.desc' {C : Type u} {X Y : C} (f : X Y) {W : C} (k : Y W) (h : f k = 0) :
{l //

Any morphism `k : Y ⟶ W` satisfying `f ≫ k = 0` induces `l : cokernel f ⟶ W` such that `cokernel.π f ≫ l = k`.

Equations
@[reducible]
noncomputable def category_theory.limits.cokernel.map {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q = p f') :

A commuting square induces a morphism of cokernels.

theorem category_theory.limits.cokernel.map_desc {C : Type u} {X Y Z X' Y' Z' : C} (f : X Y) (g : Y Z) (w : f g = 0) (f' : X' Y') (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') :
h₁ =

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'

@[simp]
theorem category_theory.limits.cokernel.map_iso_inv {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :
w).inv = _
@[simp]
theorem category_theory.limits.cokernel.map_iso_hom {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :
w).hom = w
noncomputable def category_theory.limits.cokernel.map_iso {C : Type u} {X Y : C} (f : X Y) {X' Y' : C} (f' : X' Y') (p : X X') (q : Y Y') (w : f q.hom = p.hom f') :

A commuting square of isomorphisms induces an isomorphism of cokernels.

Equations
@[protected, instance]

The cokernel of the zero morphism is an isomorphism

theorem category_theory.limits.eq_zero_of_mono_cokernel {C : Type u} {X Y : C} (f : X Y)  :
f = 0
noncomputable def category_theory.limits.cokernel_zero_iso_target {C : Type u} {X Y : C} :

The cokernel of a zero morphism is isomorphic to the target.

Equations
@[simp]
@[simp]
noncomputable def category_theory.limits.cokernel_iso_of_eq {C : Type u} {X Y : C} {f g : X Y} (h : f = g) :

If two morphisms are known to be equal, then their cokernels are isomorphic.

Equations
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_refl {C : Type u} {X Y : C} (f : X Y) {h : f = f} :
@[simp]
theorem category_theory.limits.π_comp_cokernel_iso_of_eq_hom_assoc {C : Type u} {X Y : C} {f g : X Y} (h : f = g) {X' : C} (f' : X') :
@[simp]
@[simp]
theorem category_theory.limits.π_comp_cokernel_iso_of_eq_inv_assoc {C : Type u} {X Y : C} {f g : X Y} (h : f = g) {X' : C} (f' : X') :
@[simp]
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_hom_comp_desc_assoc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Y Z) (he : g e = 0) {X' : C} (f' : Z X') :
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_hom_comp_desc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Y Z) (he : g e = 0) :
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_inv_comp_desc_assoc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Y Z) (he : f e = 0) {X' : C} (f' : Z X') :
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_inv_comp_desc {C : Type u} {X Y Z : C} {f g : X Y} (h : f = g) (e : Y Z) (he : f e = 0) :
@[simp]
theorem category_theory.limits.cokernel_iso_of_eq_trans {C : Type u} {X Y : C} {f g h : X Y} (w₁ : f = g) (w₂ : g = h) :
theorem category_theory.limits.cokernel_not_mono_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
theorem category_theory.limits.cokernel_not_iso_of_nonzero {C : Type u} {X Y : C} {f : X Y} (w : f 0) :
@[protected, instance]
def category_theory.limits.has_cokernel_comp_iso {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
noncomputable def category_theory.limits.cokernel_comp_is_iso {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

When `g` is an isomorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `f`.

Equations
@[simp]
theorem category_theory.limits.cokernel_comp_is_iso_hom {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[simp]
theorem category_theory.limits.cokernel_comp_is_iso_inv {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[protected, instance]
def category_theory.limits.has_cokernel_epi_comp {C : Type u} {X Y : C} (f : X Y) {W : C} (g : W X)  :
noncomputable def category_theory.limits.cokernel_epi_comp {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :

When `f` is an epimorphism, the cokernel of `f ≫ g` is isomorphic to the cokernel of `g`.

Equations
@[simp]
theorem category_theory.limits.cokernel_epi_comp_hom {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
@[simp]
theorem category_theory.limits.cokernel_epi_comp_inv {C : Type u} {X Y Z : C} (f : X Y) (g : Y Z)  :
noncomputable def category_theory.limits.cokernel.zero_cokernel_cofork {C : Type u} {X Y : C} (f : X Y)  :

The morphism to the zero object determines a cocone on a cokernel diagram

Equations

The morphism to the zero object is a cokernel of an epimorphism

Equations
noncomputable def category_theory.limits.cokernel.of_epi {C : Type u} {X Y : C} (f : X Y)  :

The cokernel of an epimorphism is isomorphic to the zero object

Equations
theorem category_theory.limits.cokernel.π_of_epi {C : Type u} {X Y : C} (f : X Y)  :

The cokernel morphism of an epimorphism is a zero morphism

@[simp]
theorem category_theory.limits.mono_factorisation.kernel_ι_comp {C : Type u} {X Y : C} {f : X Y}  :

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.)

Equations
@[simp]
@[simp]

The cokernel of a zero morphism is an isomorphism

@[protected, instance]

The kernel of the cokernel of an epimorphism is an isomorphism

@[protected, instance]

The cokernel of the kernel of a monomorphism is an isomorphism

noncomputable def category_theory.limits.zero_cokernel_of_zero_cancel {C : Type u} {X Y : C} (f : X Y) (hf : (Z : C) (g : Y Z), f g = 0 g = 0) :

If `f ≫ g = 0` implies `g = 0` for all `g`, then `0 : Y ⟶ 0` is a cokernel of `f`.

Equations
def category_theory.limits.is_cokernel.of_iso_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Z Y) (i : X Z) (h : i.hom l = f)  :

If `i` is an isomorphism such that `i.hom ≫ l = f`, then any cokernel of `f` is a cokernel of `l`.

Equations
noncomputable def category_theory.limits.cokernel.of_iso_comp {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Z Y) (i : X Z) (h : i.hom l = f) :

If `i` is an isomorphism such that `i.hom ≫ l = f`, then the cokernel of `f` is a cokernel of `l`.

Equations
def category_theory.limits.is_cokernel.cokernel_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Y Z) (i : s.X Z) (h : = l) :

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`.

Equations
noncomputable def category_theory.limits.cokernel.cokernel_iso {C : Type u} {X Y : C} (f : X Y) {Z : C} (l : Y Z) (i : Z) (h : = l) :

If `i` is an isomorphism such that `cokernel.π f ≫ i.hom = l`, then `l` is a cokernel of `f`.

Equations
noncomputable def category_theory.limits.kernel_comparison {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D)  :

The comparison morphism for the kernel of `f`. This is an isomorphism iff `G` preserves the kernel of `f`; see `category_theory/limits/preserves/shapes/kernels.lean`

Equations
Instances for `category_theory.limits.kernel_comparison`
@[simp]
theorem category_theory.limits.kernel_comparison_comp_ι_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' : D} (f' : G.obj X X') :
= f'
@[simp]
theorem category_theory.limits.kernel_comparison_comp_ι {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D)  :
@[simp]
theorem category_theory.limits.map_lift_kernel_comparison {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {Z : C} {h : Z X} (w : h f = 0) :
= (G.map h) _
@[simp]
theorem category_theory.limits.map_lift_kernel_comparison_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {Z : C} {h : Z X} (w : h f = 0) {X' : D} (f' : X') :
= (G.map h) _ f'
theorem category_theory.limits.kernel_comparison_comp_kernel_map {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' Y' : C} (g : X' Y') (p : X X') (q : Y Y') (hpq : f q = p g) :
(G.map g) (G.map p) (G.map q) _ = G.map hpq)
theorem category_theory.limits.kernel_comparison_comp_kernel_map_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' Y' : C} (g : X' Y') (p : X X') (q : Y Y') (hpq : f q = p g) {X'_1 : D} (f' : X'_1) :
(G.map g) (G.map p) (G.map q) _ f' = G.map hpq)
noncomputable def category_theory.limits.cokernel_comparison {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D)  :

The comparison morphism for the cokernel of `f`.

Equations
Instances for `category_theory.limits.cokernel_comparison`
@[simp]
theorem category_theory.limits.π_comp_cokernel_comparison {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D)  :
@[simp]
theorem category_theory.limits.π_comp_cokernel_comparison_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' : D} (f' : X') :
@[simp]
theorem category_theory.limits.cokernel_comparison_map_desc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {Z : C} {h : Y Z} (w : f h = 0) :
= (G.map h) _
@[simp]
theorem category_theory.limits.cokernel_comparison_map_desc_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {Z : C} {h : Y Z} (w : f h = 0) {X' : D} (f' : G.obj Z X') :
= (G.map h) _ f'
theorem category_theory.limits.cokernel_map_comp_cokernel_comparison_assoc {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' Y' : C} (g : X' Y') (p : X X') (q : Y Y') (hpq : f q = p g) {X'_1 : D} (f' : X'_1) :
(G.map g) (G.map p) (G.map q) _ = G.map hpq) f'
theorem category_theory.limits.cokernel_map_comp_cokernel_comparison {C : Type u} {X Y : C} (f : X Y) {D : Type u₂} (G : C D) {X' Y' : C} (g : X' Y') (p : X X') (q : Y Y') (hpq : f q = p g) :
(G.map g) (G.map p) (G.map q) _ = G.map hpq)
@[class]
structure category_theory.limits.has_kernels (C : Type u)  :
Prop
• has_limit : ( {X Y : C} (f : X Y), . "apply_instance"

`has_kernels` represents the existence of kernels for every morphism.

Instances of this typeclass
@[class]
structure category_theory.limits.has_cokernels (C : Type u)  :
Prop
• has_colimit : ( {X Y : C} (f : X Y), . "apply_instance"

`has_cokernels` represents the existence of cokernels for every morphism.

Instances of this typeclass
@[protected, instance]
@[protected, instance]