Kernels and cokernels

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.ιZeroIsIso: 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.ofMono: the kernel of a monomorphism is the zero object
• kernel.liftMono: the lift of a monomorphism k : W ⟶ X such that k ≫ f = 0 is still a monomorphism
• kernel.isLimitConeZeroCone: if our category has a zero object, then the map from the zero object is a kernel map of any monomorphism
• kernel.ιOfZero: kernel.ι (0 : X ⟶ Y) is an isomorphism

and the corresponding dual statements.

Future work

• TODO: connect this with existing work 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 abbrevs of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

References

• F. Borceux, Handbook of Categorical Algebra 2

@[reducible, inline]

abbrev CategoryTheory.Limits.HasKernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) : Prop

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

Equations

• CategoryTheory.Limits.HasKernel f = CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f 0)

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCokernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) : Prop

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

Equations

• CategoryTheory.Limits.HasCokernel f = CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f 0)

@[reducible, inline]

abbrev CategoryTheory.Limits.KernelFork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {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.

Equations

• CategoryTheory.Limits.KernelFork f = CategoryTheory.Limits.Fork f 0

@[simp]

theorem CategoryTheory.Limits.KernelFork.condition {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : KernelFork f) : CategoryStruct.comp (Fork.ι s) f = 0

@[simp]

theorem CategoryTheory.Limits.KernelFork.condition_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : KernelFork f) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (Fork.ι s) (CategoryStruct.comp f h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Limits.KernelFork.app_one {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : KernelFork f) : s.π.app WalkingParallelPair.one = 0

@[reducible, inline]

abbrev CategoryTheory.Limits.KernelFork.ofι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} (ι : Z ⟶ X) (w : CategoryStruct.comp ι f = 0) : KernelFork f

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

Equations

• CategoryTheory.Limits.KernelFork.ofι ι w = CategoryTheory.Limits.Fork.ofι ι ⋯

@[simp]

theorem CategoryTheory.Limits.KernelFork.ι_ofι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y P : C} (f : X ⟶ Y) (ι : P ⟶ X) (w : CategoryStruct.comp ι f = 0) : Fork.ι (ofι ι w) = ι

def CategoryTheory.Limits.isoOfι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : Fork f 0) : s ≅ Fork.ofι s.ι ⋯

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

Equations

• CategoryTheory.Limits.isoOfι s = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl s.pt) ⋯

def CategoryTheory.Limits.ofιCongr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {P : C} {ι ι' : P ⟶ X} {w : CategoryStruct.comp ι f = 0} (h : ι = ι') : KernelFork.ofι ι w ≅ KernelFork.ofι ι' ⋯

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

Equations

• CategoryTheory.Limits.ofιCongr h = CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (CategoryTheory.Limits.KernelFork.ofι ι w).pt) ⋯

def CategoryTheory.Limits.compNatIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {D : Type u'} [Category.{v, u'} D] [HasZeroMorphisms D] (F : Functor C D) [F.IsEquivalence] : (parallelPair f 0).comp F ≅ parallelPair (F.map f) 0

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

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.KernelFork.IsLimit.lift' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {s : KernelFork f} (hs : IsLimit s) {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : { l : W ⟶ s.pt // CategoryStruct.comp l (Fork.ι s) = k }

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

• CategoryTheory.Limits.KernelFork.IsLimit.lift' hs k h = ⟨hs.lift (CategoryTheory.Limits.KernelFork.ofι k h), ⋯⟩

def CategoryTheory.Limits.isLimitAux {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (t : KernelFork f) (lift : (s : KernelFork f) → s.pt ⟶ t.pt) (fac : ∀ (s : KernelFork f), CategoryStruct.comp (lift s) (Fork.ι t) = Fork.ι s) (uniq : ∀ (s : KernelFork f) (m : s.pt ⟶ t.pt), CategoryStruct.comp m (Fork.ι t) = Fork.ι s → m = lift s) : IsLimit t

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

• CategoryTheory.Limits.isLimitAux t lift fac uniq = { lift := lift, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.KernelFork.IsLimit.ofι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {W : C} (g : W ⟶ X) (eq : CategoryStruct.comp g f = 0) (lift : {W' : C} → (g' : W' ⟶ X) → CategoryStruct.comp g' f = 0 → (W' ⟶ W)) (fac : ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryStruct.comp g' f = 0), CategoryStruct.comp (lift g' eq') g = g') (uniq : ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryStruct.comp g' f = 0) (m : W' ⟶ W), CategoryStruct.comp m g = g' → m = lift g' eq') : IsLimit (KernelFork.ofι g eq)

This is a more convenient formulation to show that a KernelFork constructed using KernelFork.ofι is a limit cone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.KernelFork.IsLimit.ofι' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y K : C} {f : X ⟶ Y} (i : K ⟶ X) (w : CategoryStruct.comp i f = 0) (h : {A : C} → (k : A ⟶ X) → CategoryStruct.comp k f = 0 → { l : A ⟶ K // CategoryStruct.comp l i = k }) [hi : Mono i] : IsLimit (KernelFork.ofι i w)

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.isKernelCompMono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : KernelFork f} (i : IsLimit c) {Z : C} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z} (hh : h = CategoryStruct.comp f g) : IsLimit (KernelFork.ofι (Fork.ι c) ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.isKernelCompMono_lift {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : KernelFork f} (i : IsLimit c) {Z : C} (g : Y ⟶ Z) [hg : Mono g] {h : X ⟶ Z} (hh : h = CategoryStruct.comp f g) (s : KernelFork h) : (isKernelCompMono i g hh).lift s = i.lift (Fork.ofι (Fork.ι s) ⋯)

def CategoryTheory.Limits.isKernelOfComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {W : C} (g : Y ⟶ W) (h : X ⟶ W) {c : KernelFork h} (i : IsLimit c) (hf : CategoryStruct.comp (Fork.ι c) f = 0) (hfg : CategoryStruct.comp f g = h) : IsLimit (KernelFork.ofι (Fork.ι c) hf)

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.KernelFork.IsLimit.ofId {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (hf : f = 0) : IsLimit (KernelFork.ofι (CategoryStruct.id X) ⋯)

X identifies to the kernel of a zero map X ⟶ Y.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hf : Mono f) (h : IsZero c.pt) : IsLimit c

Any zero object identifies to the kernel of a given monomorphisms.

Equations

• CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero c hf h = CategoryTheory.Limits.isLimitAux c (fun (x : CategoryTheory.Limits.KernelFork f) => 0) ⋯ ⋯

theorem CategoryTheory.Limits.KernelFork.IsLimit.isIso_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : KernelFork f) (hc : IsLimit c) (hf : f = 0) : IsIso (Fork.ι c)

def CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {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), CategoryStruct.comp φ g = 0 ↔ CategoryStruct.comp φ (CategoryStruct.comp e.hom g') = 0) : IsLimit (ofι (CategoryStruct.comp (Fork.ι c) e.hom) ⋯)

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.KernelFork.isLimitOfIsLimitOfIff' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {g : X ⟶ Y} {c : KernelFork g} (hc : IsLimit c) {Y' : C} (g' : X ⟶ Y') (iff : ∀ ⦃W : C⦄ (φ : W ⟶ X), CategoryStruct.comp φ g = 0 ↔ CategoryStruct.comp φ g' = 0) : IsLimit (ofι (Fork.ι c) ⋯)

If c is a limit kernel fork for g : X ⟶ Y, and g' : X ⟶ Y' is 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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.KernelFork.IsLimit.isZero_of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : KernelFork f} (hc : IsLimit c) [Mono f] : IsZero c.pt

def CategoryTheory.Limits.KernelFork.mapOfIsLimit {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') : kf.pt ⟶ kf'.pt

The morphism between points of kernel forks induced by a morphism in the category of arrows.

Equations

• kf.mapOfIsLimit hf' φ = hf'.lift (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) φ.left) ⋯)

@[simp]

theorem CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') : CategoryStruct.comp (kf.mapOfIsLimit hf' φ) (Fork.ι kf') = CategoryStruct.comp (Fork.ι kf) φ.left

@[simp]

theorem CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') {Z : C} (h : (parallelPair f' 0).obj WalkingParallelPair.zero ⟶ Z) : CategoryStruct.comp (kf.mapOfIsLimit hf' φ) (CategoryStruct.comp (Fork.ι kf') h) = CategoryStruct.comp (CategoryStruct.comp (Fork.ι kf) φ.left) h

def CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : KernelFork f} {kf' : KernelFork f'} (hf : IsLimit kf) (hf' : IsLimit kf') (φ : Arrow.mk f ≅ Arrow.mk f') : kf.pt ≅ kf'.pt

The isomorphism between points of limit kernel forks induced by an isomorphism in the category of arrows.

Equations

• CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit hf hf' φ = { hom := kf.mapOfIsLimit hf' φ.hom, inv := kf'.mapOfIsLimit hf φ.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : KernelFork f} {kf' : KernelFork f'} (hf : IsLimit kf) (hf' : IsLimit kf') (φ : Arrow.mk f ≅ Arrow.mk f') : (mapIsoOfIsLimit hf hf' φ).inv = kf'.mapOfIsLimit hf φ.inv

@[simp]

theorem CategoryTheory.Limits.KernelFork.mapIsoOfIsLimit_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {kf : KernelFork f} {kf' : KernelFork f'} (hf : IsLimit kf) (hf' : IsLimit kf') (φ : Arrow.mk f ≅ Arrow.mk f') : (mapIsoOfIsLimit hf hf' φ).hom = kf.mapOfIsLimit hf' φ.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.kernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] : C

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

Equations

• CategoryTheory.Limits.kernel f = CategoryTheory.Limits.equalizer f 0

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.kernel.ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] : kernel f ⟶ X

The map from kernel f into the source of f.

Equations

• CategoryTheory.Limits.kernel.ι f = CategoryTheory.Limits.equalizer.ι f 0

@[simp]

theorem CategoryTheory.Limits.equalizer_as_kernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] : equalizer.ι f 0 = kernel.ι f

@[simp]

theorem CategoryTheory.Limits.kernel.condition {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] : CategoryStruct.comp (ι f) f = 0

@[simp]

theorem CategoryTheory.Limits.kernel.condition_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (ι f) (CategoryStruct.comp f h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Limits.kernelIsKernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] : IsLimit (Fork.ofι (kernel.ι f) ⋯)

The kernel built from kernel.ι f is limiting.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.kernel.lift {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : W ⟶ kernel f

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

Equations

• CategoryTheory.Limits.kernel.lift f k h = (CategoryTheory.Limits.kernelIsKernel f).lift (CategoryTheory.Limits.KernelFork.ofι k h)

@[simp]

theorem CategoryTheory.Limits.kernel.lift_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : CategoryStruct.comp (lift f k h) (ι f) = k

@[simp]

theorem CategoryTheory.Limits.kernel.lift_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (lift f k h) (CategoryStruct.comp (ι f) h✝) = CategoryStruct.comp k h✝

@[simp]

theorem CategoryTheory.Limits.kernel.lift_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} {h : CategoryStruct.comp 0 f = 0} : lift f 0 h = 0

instance CategoryTheory.Limits.kernel.lift_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) [Mono k] : Mono (lift f k h)

noncomputable def CategoryTheory.Limits.kernel.lift' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {W : C} (k : W ⟶ X) (h : CategoryStruct.comp k f = 0) : { l : W ⟶ kernel f // CategoryStruct.comp l (ι f) = k }

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

Equations

• CategoryTheory.Limits.kernel.lift' f k h = ⟨CategoryTheory.Limits.kernel.lift f k h, ⋯⟩

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.kernel.map {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : CategoryStruct.comp f q = CategoryStruct.comp p f') : kernel f ⟶ kernel f'

A commuting square induces a morphism of kernels.

Equations

• CategoryTheory.Limits.kernel.map f f' p q w = CategoryTheory.Limits.kernel.lift f' (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) p) ⋯

@[simp]

theorem CategoryTheory.Limits.kernel.map_id {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] (q : Y ⟶ Y) (w : CategoryStruct.comp f q = CategoryStruct.comp (CategoryStruct.id X) f) : map f f (CategoryStruct.id X) q w = CategoryStruct.id (kernel f)

instance CategoryTheory.Limits.instIsIsoMapOfMono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : CategoryStruct.comp f q = CategoryStruct.comp p f') [IsIso p] [Mono q] : IsIso (kernel.map f f' p q w)

theorem CategoryTheory.Limits.kernel.lift_map {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel g] (w : CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') (g' : Y' ⟶ Z') [HasKernel g'] (w' : CategoryStruct.comp f' g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : CategoryStruct.comp f q = CategoryStruct.comp p f') (h₂ : CategoryStruct.comp g r = CategoryStruct.comp q g') : CategoryStruct.comp (lift g f w) (map g g' q r h₂) = CategoryStruct.comp p (lift g' f' w')

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 CategoryTheory.Limits.kernel.map_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y') [HasKernel f] [HasKernel f'] (q : Y ⟶ Y') (w : CategoryStruct.comp f q = CategoryStruct.comp 0 f') : map f f' 0 q w = 0

noncomputable def CategoryTheory.Limits.kernel.mapIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : kernel f ≅ kernel f'

A commuting square of isomorphisms induces an isomorphism of kernels.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.kernel.mapIso_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : (mapIso f f' p q w).hom = map f f' p.hom q.hom w

@[simp]

theorem CategoryTheory.Limits.kernel.mapIso_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : (mapIso f f' p q w).inv = map f' f p.inv q.inv ⋯

instance CategoryTheory.Limits.kernel.ι_zero_isIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : IsIso (ι 0)

Every kernel of the zero morphism is an isomorphism

theorem CategoryTheory.Limits.eq_zero_of_epi_kernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [Epi (kernel.ι f)] : f = 0

noncomputable def CategoryTheory.Limits.kernelZeroIsoSource {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : kernel 0 ≅ X

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

Equations

• CategoryTheory.Limits.kernelZeroIsoSource = CategoryTheory.Limits.equalizer.isoSourceOfSelf 0

@[simp]

theorem CategoryTheory.Limits.kernelZeroIsoSource_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : kernelZeroIsoSource.hom = kernel.ι 0

@[simp]

theorem CategoryTheory.Limits.kernelZeroIsoSource_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : kernelZeroIsoSource.inv = kernel.lift 0 (CategoryStruct.id X) ⋯

noncomputable def CategoryTheory.Limits.kernelIsoOfEq {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : kernel f ≅ kernel g

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

Equations

• CategoryTheory.Limits.kernelIsoOfEq h = CategoryTheory.Limits.HasLimit.isoOfNatIso (⋯.mpr (CategoryTheory.Iso.refl (CategoryTheory.Limits.parallelPair g 0)))

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_refl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {h : f = f} : kernelIsoOfEq h = Iso.refl (kernel f)

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : CategoryStruct.comp (kernelIsoOfEq h).hom (kernel.ι g) = kernel.ι f

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (kernelIsoOfEq h).hom (CategoryStruct.comp (kernel.ι g) h✝) = CategoryStruct.comp (kernel.ι f) h✝

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) : CategoryStruct.comp (kernelIsoOfEq h).inv (kernel.ι f) = kernel.ι g

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) {Z : C} (h✝ : X ⟶ Z) : CategoryStruct.comp (kernelIsoOfEq h).inv (CategoryStruct.comp (kernel.ι f) h✝) = CategoryStruct.comp (kernel.ι g) h✝

@[simp]

theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he : CategoryStruct.comp e f = 0) : CategoryStruct.comp (kernel.lift f e he) (kernelIsoOfEq h).hom = kernel.lift g e ⋯

@[simp]

theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he : CategoryStruct.comp e f = 0) {Z✝ : C} (h✝ : kernel g ⟶ Z✝) : CategoryStruct.comp (kernel.lift f e he) (CategoryStruct.comp (kernelIsoOfEq h).hom h✝) = CategoryStruct.comp (kernel.lift g e ⋯) h✝

@[simp]

theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he : CategoryStruct.comp e g = 0) : CategoryStruct.comp (kernel.lift g e he) (kernelIsoOfEq h).inv = kernel.lift f e ⋯

@[simp]

theorem CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasKernel f] [HasKernel g] (h : f = g) (e : Z ⟶ X) (he : CategoryStruct.comp e g = 0) {Z✝ : C} (h✝ : kernel f ⟶ Z✝) : CategoryStruct.comp (kernel.lift g e he) (CategoryStruct.comp (kernelIsoOfEq h).inv h✝) = CategoryStruct.comp (kernel.lift f e ⋯) h✝

@[simp]

theorem CategoryTheory.Limits.kernelIsoOfEq_trans {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g h : X ⟶ Y} [HasKernel f] [HasKernel g] [HasKernel h] (w₁ : f = g) (w₂ : g = h) : kernelIsoOfEq w₁ ≪≫ kernelIsoOfEq w₂ = kernelIsoOfEq ⋯

theorem CategoryTheory.Limits.kernel_not_epi_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasKernel f] (w : f ≠ 0) : ¬Epi (kernel.ι f)

theorem CategoryTheory.Limits.kernel_not_iso_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasKernel f] (w : f ≠ 0) : IsIso (kernel.ι f) → False

instance CategoryTheory.Limits.hasKernel_comp_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) [HasKernel f] (g : Y ⟶ Z) [Mono g] : HasKernel (CategoryStruct.comp f g)

noncomputable def CategoryTheory.Limits.kernelCompMono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g] : kernel (CategoryStruct.comp f g) ≅ kernel f

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.kernelCompMono_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g] : (kernelCompMono f g).hom = kernel.lift f (kernel.ι (CategoryStruct.comp f g)) ⋯

@[simp]

theorem CategoryTheory.Limits.kernelCompMono_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g] : (kernelCompMono f g).inv = kernel.lift (CategoryStruct.comp f g) (kernel.ι f) ⋯

instance CategoryTheory.Limits.hasKernel_iso_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : HasKernel (CategoryStruct.comp f g)

noncomputable def CategoryTheory.Limits.kernelIsIsoComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : kernel (CategoryStruct.comp f g) ≅ kernel g

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.kernelIsIsoComp_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : (kernelIsIsoComp f g).hom = kernel.lift g (CategoryStruct.comp (kernel.ι (CategoryStruct.comp f g)) f) ⋯

@[simp]

theorem CategoryTheory.Limits.kernelIsIsoComp_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] : (kernelIsIsoComp f g).inv = kernel.lift (CategoryStruct.comp f g) (CategoryStruct.comp (kernel.ι g) (inv f)) ⋯

noncomputable def CategoryTheory.Limits.kernel.congr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasKernel f] [HasKernel g] (h : f = g) : kernel f ≅ kernel g

Equal maps have isomorphic kernels.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.kernel.congr_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasKernel f] [HasKernel g] (h : f = g) : (congr f g h).hom = lift g (ι f) ⋯

@[simp]

theorem CategoryTheory.Limits.kernel.congr_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasKernel f] [HasKernel g] (h : f = g) : (congr f g h).inv = lift f (ι g) ⋯

theorem CategoryTheory.Limits.isZero_kernel_of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Mono f] [HasKernel f] : IsZero (kernel f)

noncomputable def CategoryTheory.Limits.kernel.zeroKernelFork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] : KernelFork f

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

Equations

• CategoryTheory.Limits.kernel.zeroKernelFork f = { pt := 0, π := { app := fun (x : CategoryTheory.Limits.WalkingParallelPair) => 0, naturality := ⋯ } }

noncomputable def CategoryTheory.Limits.kernel.isLimitConeZeroCone {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [Mono f] : IsLimit (zeroKernelFork f)

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

Equations

• CategoryTheory.Limits.kernel.isLimitConeZeroCone f = CategoryTheory.Limits.Fork.IsLimit.mk (CategoryTheory.Limits.kernel.zeroKernelFork f) (fun (x : CategoryTheory.Limits.Fork f 0) => 0) ⋯ ⋯

noncomputable def CategoryTheory.Limits.kernel.ofMono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasKernel f] [Mono f] : kernel f ≅ 0

The kernel of a monomorphism is isomorphic to the zero object

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.kernel.ι_of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasKernel f] [Mono f] : ι f = 0

The kernel morphism of a monomorphism is a zero morphism

noncomputable def CategoryTheory.Limits.zeroKernelOfCancelZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Z ⟶ X), CategoryStruct.comp g f = 0 → g = 0) : IsLimit (KernelFork.ofι 0 ⋯)

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

Equations

• CategoryTheory.Limits.zeroKernelOfCancelZero f hf = CategoryTheory.Limits.Fork.IsLimit.mk (CategoryTheory.Limits.KernelFork.ofι 0 ⋯) (fun (x : CategoryTheory.Limits.Fork f 0) => 0) ⋯ ⋯

def CategoryTheory.Limits.IsKernel.ofIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {X' Y' : C} {f' : X' ⟶ Y'} {s : KernelFork f} (hs : IsLimit s) (s' : KernelFork f') (eX : X ≅ X') (eY : Y ≅ Y') (e : s.pt ≅ s'.pt) (H : CategoryStruct.comp eX.hom f' = CategoryStruct.comp f eY.hom) (H' : CategoryStruct.comp e.hom (Fork.ι s') = CategoryStruct.comp (Fork.ι s) eX.hom) : IsLimit s'

Transport an IsKernel across isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.IsKernel.ofCompIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : CategoryStruct.comp l i.hom = f) {s : KernelFork f} (hs : IsLimit s) : IsLimit (KernelFork.ofι (Fork.ι s) ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.kernel.ofCompIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {Z : C} (l : X ⟶ Z) (i : Z ≅ Y) (h : CategoryStruct.comp l i.hom = f) : IsLimit (KernelFork.ofι (ι f) ⋯)

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

Equations

• CategoryTheory.Limits.kernel.ofCompIso f l i h = CategoryTheory.Limits.IsKernel.ofCompIso f l i h (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair f 0))

def CategoryTheory.Limits.IsKernel.isoKernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : Z ⟶ X) {s : KernelFork f} (hs : IsLimit s) (i : Z ≅ s.pt) (h : CategoryStruct.comp i.hom (Fork.ι s) = l) : IsLimit (KernelFork.ofι 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

• CategoryTheory.Limits.IsKernel.isoKernel f l hs i h = hs.ofIsoLimit (CategoryTheory.Limits.Cone.ext i.symm ⋯)

noncomputable def CategoryTheory.Limits.kernel.isoKernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] {Z : C} (l : Z ⟶ X) (i : Z ≅ kernel f) (h : CategoryStruct.comp i.hom (ι f) = l) : IsLimit (KernelFork.ofι l ⋯)

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

Equations

• CategoryTheory.Limits.kernel.isoKernel f l i h = CategoryTheory.Limits.IsKernel.isoKernel f l (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.parallelPair f 0)) i h

theorem CategoryTheory.Limits.kernel.ι_of_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) : IsIso (ι 0)

The kernel morphism of a zero morphism is an isomorphism

@[reducible, inline]

abbrev CategoryTheory.Limits.CokernelCofork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {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.

Equations

• CategoryTheory.Limits.CokernelCofork f = CategoryTheory.Limits.Cofork f 0

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.condition {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CokernelCofork f) : CategoryStruct.comp f (Cofork.π s) = 0

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.condition_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CokernelCofork f) {Z : C} (h : ((Functor.const WalkingParallelPair).obj s.pt).obj WalkingParallelPair.one ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (Cofork.π s) h) = CategoryStruct.comp 0 h

theorem CategoryTheory.Limits.CokernelCofork.π_eq_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : CokernelCofork f) : s.ι.app WalkingParallelPair.zero = 0

@[reducible, inline]

abbrev CategoryTheory.Limits.CokernelCofork.ofπ {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} (π : Y ⟶ Z) (w : CategoryStruct.comp f π = 0) : CokernelCofork f

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

Equations

• CategoryTheory.Limits.CokernelCofork.ofπ π w = CategoryTheory.Limits.Cofork.ofπ π ⋯

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.π_ofπ {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y P : C} (f : X ⟶ Y) (π : Y ⟶ P) (w : CategoryStruct.comp f π = 0) : Cofork.π (ofπ π w) = π

def CategoryTheory.Limits.isoOfπ {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (s : Cofork f 0) : s ≅ Cofork.ofπ s.π ⋯

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

Equations

• CategoryTheory.Limits.isoOfπ s = CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl s.pt) ⋯

def CategoryTheory.Limits.ofπCongr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {P : C} {π π' : Y ⟶ P} {w : CategoryStruct.comp f π = 0} (h : π = π') : CokernelCofork.ofπ π w ≅ CokernelCofork.ofπ π' ⋯

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

Equations

• CategoryTheory.Limits.ofπCongr h = CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl (CategoryTheory.Limits.CokernelCofork.ofπ π w).pt) ⋯

def CategoryTheory.Limits.CokernelCofork.IsColimit.desc' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {s : CokernelCofork f} (hs : IsColimit s) {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) : { l : s.pt ⟶ W // CategoryStruct.comp (Cofork.π s) l = k }

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

• CategoryTheory.Limits.CokernelCofork.IsColimit.desc' hs k h = ⟨hs.desc (CategoryTheory.Limits.CokernelCofork.ofπ k h), ⋯⟩

def CategoryTheory.Limits.isColimitAux {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (t : CokernelCofork f) (desc : (s : CokernelCofork f) → t.pt ⟶ s.pt) (fac : ∀ (s : CokernelCofork f), CategoryStruct.comp (Cofork.π t) (desc s) = Cofork.π s) (uniq : ∀ (s : CokernelCofork f) (m : t.pt ⟶ s.pt), CategoryStruct.comp (Cofork.π t) m = Cofork.π s → m = desc s) : IsColimit t

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

• CategoryTheory.Limits.isColimitAux t desc fac uniq = { desc := desc, fac := ⋯, uniq := ⋯ }

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {Z : C} (g : Y ⟶ Z) (eq : CategoryStruct.comp f g = 0) (desc : {Z' : C} → (g' : Y ⟶ Z') → CategoryStruct.comp f g' = 0 → (Z ⟶ Z')) (fac : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryStruct.comp f g' = 0), CategoryStruct.comp g (desc g' eq') = g') (uniq : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryStruct.comp f g' = 0) (m : Z ⟶ Z'), CategoryStruct.comp g m = g' → m = desc g' eq') : IsColimit (CokernelCofork.ofπ g eq)

This is a more convenient formulation to show that a CokernelCofork constructed using CokernelCofork.ofπ is a limit cone.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Q : C} {f : X ⟶ Y} (p : Y ⟶ Q) (w : CategoryStruct.comp f p = 0) (h : {A : C} → (k : Y ⟶ A) → CategoryStruct.comp f k = 0 → { l : Q ⟶ A // CategoryStruct.comp p l = k }) [hp : Epi p] : IsColimit (CokernelCofork.ofπ p w)

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.isCokernelEpiComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (i : IsColimit c) {W : C} (g : W ⟶ X) [hg : Epi g] {h : W ⟶ Y} (hh : h = CategoryStruct.comp g f) : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.isCokernelEpiComp_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (i : IsColimit c) {W : C} (g : W ⟶ X) [hg : Epi g] {h : W ⟶ Y} (hh : h = CategoryStruct.comp g f) (s : CokernelCofork h) : (isCokernelEpiComp i g hh).desc s = i.desc (Cofork.ofπ (Cofork.π s) ⋯)

def CategoryTheory.Limits.isCokernelOfComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {W : C} (g : W ⟶ X) (h : W ⟶ Y) {c : CokernelCofork h} (i : IsColimit c) (hf : CategoryStruct.comp f (Cofork.π c) = 0) (hfg : CategoryStruct.comp g f = h) : IsColimit (CokernelCofork.ofπ (Cofork.π c) hf)

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofId {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) (hf : f = 0) : IsColimit (CokernelCofork.ofπ (CategoryStruct.id Y) ⋯)

Y identifies to the cokernel of a zero map X ⟶ Y.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hf : Epi f) (h : IsZero c.pt) : IsColimit c

Any zero object identifies to the cokernel of a given epimorphisms.

Equations

• CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero c hf h = CategoryTheory.Limits.isColimitAux c (fun (x : CategoryTheory.Limits.CokernelCofork f) => 0) ⋯ ⋯

theorem CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f) (hc : IsColimit c) (hf : f = 0) : IsIso (Cofork.π c)

def CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {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), CategoryStruct.comp f φ = 0 ↔ CategoryStruct.comp f' (CategoryStruct.comp e.hom φ) = 0) : IsColimit (ofπ (CategoryStruct.comp e.hom (Cofork.π c)) ⋯)

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.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.CokernelCofork.isColimitOfIsColimitOfIff' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (hc : IsColimit c) {X' : C} (f' : X' ⟶ Y) (iff : ∀ ⦃W : C⦄ (φ : Y ⟶ W), CategoryStruct.comp f φ = 0 ↔ CategoryStruct.comp f' φ = 0) : IsColimit (ofπ (Cofork.π c) ⋯)

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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.CokernelCofork.IsColimit.isZero_of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {c : CokernelCofork f} (hc : IsColimit c) [Epi f] : IsZero c.pt

def CategoryTheory.Limits.CokernelCofork.mapOfIsColimit {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f') (φ : Arrow.mk f ⟶ Arrow.mk f') : cc.pt ⟶ cc'.pt

The morphism between points of cokernel coforks induced by a morphism in the category of arrows.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f') (φ : Arrow.mk f ⟶ Arrow.mk f') : CategoryStruct.comp (Cofork.π cc) (mapOfIsColimit hf cc' φ) = CategoryStruct.comp φ.right (Cofork.π cc')

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} (hf : IsColimit cc) (cc' : CokernelCofork f') (φ : Arrow.mk f ⟶ Arrow.mk f') {Z : C} (h : cc'.pt ⟶ Z) : CategoryStruct.comp (Cofork.π cc) (CategoryStruct.comp (mapOfIsColimit hf cc' φ) h) = CategoryStruct.comp (CategoryStruct.comp φ.right (Cofork.π cc')) h

def CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} {cc' : CokernelCofork f'} (hf : IsColimit cc) (hf' : IsColimit cc') (φ : Arrow.mk f ≅ Arrow.mk f') : cc.pt ≅ cc'.pt

The isomorphism between points of limit cokernel coforks induced by an isomorphism in the category of arrows.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} {cc' : CokernelCofork f'} (hf : IsColimit cc) (hf' : IsColimit cc') (φ : Arrow.mk f ≅ Arrow.mk f') : (mapIsoOfIsColimit hf hf' φ).inv = mapOfIsColimit hf' cc φ.inv

@[simp]

theorem CategoryTheory.Limits.CokernelCofork.mapIsoOfIsColimit_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CokernelCofork f} {cc' : CokernelCofork f'} (hf : IsColimit cc) (hf' : IsColimit cc') (φ : Arrow.mk f ≅ Arrow.mk f') : (mapIsoOfIsColimit hf hf' φ).hom = mapOfIsColimit hf cc' φ.hom

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.cokernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] : C

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

Equations

• CategoryTheory.Limits.cokernel f = CategoryTheory.Limits.coequalizer f 0

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.cokernel.π {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] : Y ⟶ cokernel f

The map from the target of f to cokernel f.

Equations

• CategoryTheory.Limits.cokernel.π f = CategoryTheory.Limits.coequalizer.π f 0

@[simp]

theorem CategoryTheory.Limits.coequalizer_as_cokernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] : coequalizer.π f 0 = cokernel.π f

@[simp]

theorem CategoryTheory.Limits.cokernel.condition {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] : CategoryStruct.comp f (π f) = 0

@[simp]

theorem CategoryTheory.Limits.cokernel.condition_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {Z : C} (h : cokernel f ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (π f) h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Limits.cokernelIsCokernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] : IsColimit (Cofork.ofπ (cokernel.π f) ⋯)

The cokernel built from cokernel.π f is colimiting.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.cokernel.desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) : cokernel f ⟶ W

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

Equations

• CategoryTheory.Limits.cokernel.desc f k h = (CategoryTheory.Limits.cokernelIsCokernel f).desc (CategoryTheory.Limits.CokernelCofork.ofπ k h)

@[simp]

theorem CategoryTheory.Limits.cokernel.π_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) : CategoryStruct.comp (π f) (desc f k h) = k

@[simp]

theorem CategoryTheory.Limits.cokernel.π_desc_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) {Z : C} (h✝ : W ⟶ Z) : CategoryStruct.comp (π f) (CategoryStruct.comp (desc f k h) h✝) = CategoryStruct.comp k h✝

@[simp]

theorem CategoryTheory.Limits.colimit_ι_zero_cokernel_desc {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryStruct.comp f g = 0) [HasCokernel f] : CategoryStruct.comp (colimit.ι (parallelPair f 0) WalkingParallelPair.zero) (cokernel.desc f g h) = 0

@[simp]

theorem CategoryTheory.Limits.colimit_ι_zero_cokernel_desc_assoc {C : Type u_1} [Category.{v_1, u_1} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : CategoryStruct.comp f g = 0) [HasCokernel f] {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (colimit.ι (parallelPair f 0) WalkingParallelPair.zero) (CategoryStruct.comp (cokernel.desc f g h) h✝) = CategoryStruct.comp 0 h✝

@[simp]

theorem CategoryTheory.Limits.cokernel.desc_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} {h : CategoryStruct.comp f 0 = 0} : desc f 0 h = 0

instance CategoryTheory.Limits.cokernel.desc_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) [Epi k] : Epi (desc f k h)

noncomputable def CategoryTheory.Limits.cokernel.desc' {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (k : Y ⟶ W) (h : CategoryStruct.comp f k = 0) : { l : cokernel f ⟶ W // CategoryStruct.comp (π f) l = k }

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

Equations

• CategoryTheory.Limits.cokernel.desc' f k h = ⟨CategoryTheory.Limits.cokernel.desc f k h, ⋯⟩

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.cokernel.map {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : CategoryStruct.comp f q = CategoryStruct.comp p f') : cokernel f ⟶ cokernel f'

A commuting square induces a morphism of cokernels.

Equations

• CategoryTheory.Limits.cokernel.map f f' p q w = CategoryTheory.Limits.cokernel.desc f (CategoryTheory.CategoryStruct.comp q (CategoryTheory.Limits.cokernel.π f')) ⋯

instance CategoryTheory.Limits.instIsIsoMapOfEpi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ⟶ X') (q : Y ⟶ Y') (w : CategoryStruct.comp f q = CategoryStruct.comp p f') [Epi p] [IsIso q] : IsIso (cokernel.map f f' p q w)

@[simp]

theorem CategoryTheory.Limits.cokernel.map_id {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] (q : X ⟶ X) (w : CategoryStruct.comp f (CategoryStruct.id Y) = CategoryStruct.comp q f) : map f f q (CategoryStruct.id Y) w = CategoryStruct.id (cokernel f)

theorem CategoryTheory.Limits.cokernel.map_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g : Y ⟶ Z) (w : CategoryStruct.comp f g = 0) (f' : X' ⟶ Y') [HasCokernel f'] (g' : Y' ⟶ Z') (w' : CategoryStruct.comp f' g' = 0) (p : X ⟶ X') (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : CategoryStruct.comp f q = CategoryStruct.comp p f') (h₂ : CategoryStruct.comp g r = CategoryStruct.comp q g') : CategoryStruct.comp (map f f' p q h₁) (desc f' g' w') = CategoryStruct.comp (desc f g w) r

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 CategoryTheory.Limits.cokernel.map_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y') [HasCokernel f] [HasCokernel f'] (q : X ⟶ X') (w : CategoryStruct.comp f 0 = CategoryStruct.comp q f') : map f f' q 0 w = 0

noncomputable def CategoryTheory.Limits.cokernel.mapIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : cokernel f ≅ cokernel f'

A commuting square of isomorphisms induces an isomorphism of cokernels.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.cokernel.mapIso_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : (mapIso f f' p q w).hom = map f f' p.hom q.hom w

@[simp]

theorem CategoryTheory.Limits.cokernel.mapIso_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y') (w : CategoryStruct.comp f q.hom = CategoryStruct.comp p.hom f') : (mapIso f f' p q w).inv = map f' f p.inv q.inv ⋯

instance CategoryTheory.Limits.cokernel.π_zero_isIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : IsIso (π 0)

The cokernel of the zero morphism is an isomorphism

theorem CategoryTheory.Limits.eq_zero_of_mono_cokernel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] [Mono (cokernel.π f)] : f = 0

noncomputable def CategoryTheory.Limits.cokernelZeroIsoTarget {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : cokernel 0 ≅ Y

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

Equations

• CategoryTheory.Limits.cokernelZeroIsoTarget = CategoryTheory.Limits.coequalizer.isoTargetOfSelf 0

@[simp]

theorem CategoryTheory.Limits.cokernelZeroIsoTarget_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : cokernelZeroIsoTarget.hom = cokernel.desc 0 (CategoryStruct.id Y) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelZeroIsoTarget_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} : cokernelZeroIsoTarget.inv = cokernel.π 0

noncomputable def CategoryTheory.Limits.cokernelIsoOfEq {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel f ≅ cokernel g

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

Equations

• CategoryTheory.Limits.cokernelIsoOfEq h = CategoryTheory.Limits.HasColimit.isoOfNatIso (⋯.mpr (CategoryTheory.Iso.refl (CategoryTheory.Limits.parallelPair g 0)))

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_refl {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {h : f = f} : cokernelIsoOfEq h = Iso.refl (cokernel f)

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : CategoryStruct.comp (cokernel.π f) (cokernelIsoOfEq h).hom = cokernel.π g

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) {Z : C} (h✝ : cokernel g ⟶ Z) : CategoryStruct.comp (cokernel.π f) (CategoryStruct.comp (cokernelIsoOfEq h).hom h✝) = CategoryStruct.comp (cokernel.π g) h✝

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) : CategoryStruct.comp (cokernel.π g) (cokernelIsoOfEq h).inv = cokernel.π f

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) {Z : C} (h✝ : cokernel f ⟶ Z) : CategoryStruct.comp (cokernel.π g) (CategoryStruct.comp (cokernelIsoOfEq h).inv h✝) = CategoryStruct.comp (cokernel.π f) h✝

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he : CategoryStruct.comp g e = 0) : CategoryStruct.comp (cokernelIsoOfEq h).hom (cokernel.desc g e he) = cokernel.desc f e ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he : CategoryStruct.comp g e = 0) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (cokernelIsoOfEq h).hom (CategoryStruct.comp (cokernel.desc g e he) h✝) = CategoryStruct.comp (cokernel.desc f e ⋯) h✝

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he : CategoryStruct.comp f e = 0) : CategoryStruct.comp (cokernelIsoOfEq h).inv (cokernel.desc f e he) = cokernel.desc g e ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} {f g : X ⟶ Y} [HasCokernel f] [HasCokernel g] (h : f = g) (e : Y ⟶ Z) (he : CategoryStruct.comp f e = 0) {Z✝ : C} (h✝ : Z ⟶ Z✝) : CategoryStruct.comp (cokernelIsoOfEq h).inv (CategoryStruct.comp (cokernel.desc f e he) h✝) = CategoryStruct.comp (cokernel.desc g e ⋯) h✝

@[simp]

theorem CategoryTheory.Limits.cokernelIsoOfEq_trans {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f g h : X ⟶ Y} [HasCokernel f] [HasCokernel g] [HasCokernel h] (w₁ : f = g) (w₂ : g = h) : cokernelIsoOfEq w₁ ≪≫ cokernelIsoOfEq w₂ = cokernelIsoOfEq ⋯

theorem CategoryTheory.Limits.cokernel_not_mono_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasCokernel f] (w : f ≠ 0) : ¬Mono (cokernel.π f)

theorem CategoryTheory.Limits.cokernel_not_iso_of_nonzero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasCokernel f] (w : f ≠ 0) : IsIso (cokernel.π f) → False

instance CategoryTheory.Limits.hasCokernel_comp_iso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : HasCokernel (CategoryStruct.comp f g)

noncomputable def CategoryTheory.Limits.cokernelCompIsIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : cokernel (CategoryStruct.comp f g) ≅ cokernel f

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.cokernelCompIsIso_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : (cokernelCompIsIso f g).hom = cokernel.desc (CategoryStruct.comp f g) (CategoryStruct.comp (inv g) (cokernel.π f)) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelCompIsIso_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [IsIso g] : (cokernelCompIsIso f g).inv = cokernel.desc f (CategoryStruct.comp g (cokernel.π (CategoryStruct.comp f g))) ⋯

instance CategoryTheory.Limits.hasCokernel_epi_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W : C} (g : W ⟶ X) [Epi g] : HasCokernel (CategoryStruct.comp g f)

noncomputable def CategoryTheory.Limits.cokernelEpiComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel g] : cokernel (CategoryStruct.comp f g) ≅ cokernel g

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.cokernelEpiComp_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel g] : (cokernelEpiComp f g).hom = cokernel.desc (CategoryStruct.comp f g) (cokernel.π g) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelEpiComp_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel g] : (cokernelEpiComp f g).inv = cokernel.desc g (cokernel.π (CategoryStruct.comp f g)) ⋯

noncomputable def CategoryTheory.Limits.cokernel.congr {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasCokernel f] [HasCokernel g] (h : f = g) : cokernel f ≅ cokernel g

Equal maps have isomorphic cokernels.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.cokernel.congr_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasCokernel f] [HasCokernel g] (h : f = g) : (congr f g h).hom = desc f (π g) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernel.congr_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f g : X ⟶ Y) [HasCokernel f] [HasCokernel g] (h : f = g) : (congr f g h).inv = desc g (π f) ⋯

theorem CategoryTheory.Limits.isZero_cokernel_of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [Epi f] [HasCokernel f] : IsZero (cokernel f)

noncomputable def CategoryTheory.Limits.cokernel.zeroCokernelCofork {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] : CokernelCofork f

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

Equations

• CategoryTheory.Limits.cokernel.zeroCokernelCofork f = { pt := 0, ι := { app := fun (x : CategoryTheory.Limits.WalkingParallelPair) => 0, naturality := ⋯ } }

noncomputable def CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [Epi f] : IsColimit (zeroCokernelCofork f)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.cokernel.ofEpi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasCokernel f] [Epi f] : cokernel f ≅ 0

The cokernel of an epimorphism is isomorphic to the zero object

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Limits.cokernel.π_of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasCokernel f] [Epi f] : π f = 0

The cokernel morphism of an epimorphism is a zero morphism

@[simp]

theorem CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} {f : X ⟶ Y} [HasKernel f] (F : MonoFactorisation f) : CategoryStruct.comp (kernel.ι f) F.e = 0

noncomputable def CategoryTheory.Limits.cokernelImageι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι f)] [HasCokernel f] [Epi (factorThruImage f)] : cokernel (image.ι f) ≅ cokernel f

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

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.cokernelImageι_hom {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι f)] [HasCokernel f] [Epi (factorThruImage f)] : (cokernelImageι f).hom = cokernel.desc (image.ι f) (cokernel.π f) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelImageι_inv {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι f)] [HasCokernel f] [Epi (factorThruImage f)] : (cokernelImageι f).inv = cokernel.desc f (cokernel.π (image.ι f)) ⋯

noncomputable def CategoryTheory.Limits.kernelFactorThruImage {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [HasImage f] [HasKernel (factorThruImage f)] : kernel (factorThruImage f) ≅ kernel f

The kernel of the morphism X ⟶ image f is just the kernel of f.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [HasImage f] [HasKernel (factorThruImage f)] : CategoryStruct.comp (kernelFactorThruImage f).hom (kernel.ι f) = kernel.ι (factorThruImage f)

@[simp]

theorem CategoryTheory.Limits.kernelFactorThruImage_hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [HasImage f] [HasKernel (factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (kernelFactorThruImage f).hom (CategoryStruct.comp (kernel.ι f) h) = CategoryStruct.comp (kernel.ι (factorThruImage f)) h

@[simp]

theorem CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [HasImage f] [HasKernel (factorThruImage f)] : CategoryStruct.comp (kernelFactorThruImage f).inv (kernel.ι (factorThruImage f)) = kernel.ι f

@[simp]

theorem CategoryTheory.Limits.kernelFactorThruImage_inv_comp_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasKernel f] [HasImage f] [HasKernel (factorThruImage f)] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (kernelFactorThruImage f).inv (CategoryStruct.comp (kernel.ι (factorThruImage f)) h) = CategoryStruct.comp (kernel.ι f) h

theorem CategoryTheory.Limits.cokernel.π_of_zero {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] (X Y : C) : IsIso (π 0)

The cokernel of a zero morphism is an isomorphism

instance CategoryTheory.Limits.kernel.of_cokernel_of_epi {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasCokernel f] [HasKernel (cokernel.π f)] [Epi f] : IsIso (ι (cokernel.π f))

The kernel of the cokernel of an epimorphism is an isomorphism

instance CategoryTheory.Limits.cokernel.of_kernel_of_mono {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasZeroObject C] [HasKernel f] [HasCokernel (kernel.ι f)] [Mono f] : IsIso (π (kernel.ι f))

The cokernel of the kernel of a monomorphism is an isomorphism

noncomputable def CategoryTheory.Limits.zeroCokernelOfZeroCancel {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] [HasZeroObject C] {X Y : C} (f : X ⟶ Y) (hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryStruct.comp f g = 0 → g = 0) : IsColimit (CokernelCofork.ofπ 0 ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Limits.IsCokernel.ofIsoComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : CategoryStruct.comp i.hom l = f) {s : CokernelCofork f} (hs : IsColimit s) : IsColimit (CokernelCofork.ofπ (Cofork.π s) ⋯)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.cokernel.ofIsoComp {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {Z : C} (l : Z ⟶ Y) (i : X ≅ Z) (h : CategoryStruct.comp i.hom l = f) : IsColimit (CokernelCofork.ofπ (π f) ⋯)

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

Equations

• CategoryTheory.Limits.cokernel.ofIsoComp f l i h = CategoryTheory.Limits.IsCokernel.ofIsoComp f l i h (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair f 0))

def CategoryTheory.Limits.IsCokernel.cokernelIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {Z : C} (l : Y ⟶ Z) {s : CokernelCofork f} (hs : IsColimit s) (i : s.pt ≅ Z) (h : CategoryStruct.comp (Cofork.π s) i.hom = l) : IsColimit (CokernelCofork.ofπ 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

• CategoryTheory.Limits.IsCokernel.cokernelIso f l hs i h = hs.ofIsoColimit (CategoryTheory.Limits.Cocone.ext i ⋯)

def CategoryTheory.Limits.IsCokernel.ofIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {X' Y' : C} {f' : X' ⟶ Y'} {s : CokernelCofork f} (hs : IsColimit s) (s' : CokernelCofork f') (eX : X ≅ X') (eY : Y ≅ Y') (e : s.pt ≅ s'.pt) (H : CategoryStruct.comp eX.hom f' = CategoryStruct.comp f eY.hom) (H' : CategoryStruct.comp eY.hom (Cofork.π s') = CategoryStruct.comp (Cofork.π s) e.hom) : IsColimit s'

Transport an IsCokernel across isomorphisms.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.cokernel.cokernelIso {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) [HasCokernel f] {Z : C} (l : Y ⟶ Z) (i : cokernel f ≅ Z) (h : CategoryStruct.comp (π f) i.hom = l) : IsColimit (CokernelCofork.ofπ l ⋯)

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

Equations

• CategoryTheory.Limits.cokernel.cokernelIso f l i h = CategoryTheory.Limits.IsCokernel.cokernelIso f l (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair f 0)) i h

noncomputable def CategoryTheory.Limits.kernelComparison {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasKernel f] [HasKernel (G.map f)] : G.obj (kernel f) ⟶ kernel (G.map f)

The comparison morphism for the kernel of f. This is an isomorphism iff G preserves the kernel of f; see Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean

Equations

• CategoryTheory.Limits.kernelComparison f G = CategoryTheory.Limits.kernel.lift (G.map f) (G.map (CategoryTheory.Limits.kernel.ι f)) ⋯

@[simp]

theorem CategoryTheory.Limits.kernelComparison_comp_ι {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasKernel f] [HasKernel (G.map f)] : CategoryStruct.comp (kernelComparison f G) (kernel.ι (G.map f)) = G.map (kernel.ι f)

@[simp]

theorem CategoryTheory.Limits.kernelComparison_comp_ι_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasKernel f] [HasKernel (G.map f)] {Z : D} (h : G.obj X ⟶ Z) : CategoryStruct.comp (kernelComparison f G) (CategoryStruct.comp (kernel.ι (G.map f)) h) = CategoryStruct.comp (G.map (kernel.ι f)) h

@[simp]

theorem CategoryTheory.Limits.map_lift_kernelComparison {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X} (w : CategoryStruct.comp h f = 0) : CategoryStruct.comp (G.map (kernel.lift f h w)) (kernelComparison f G) = kernel.lift (G.map f) (G.map h) ⋯

@[simp]

theorem CategoryTheory.Limits.map_lift_kernelComparison_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X} (w : CategoryStruct.comp h f = 0) {Z✝ : D} (h✝ : kernel (G.map f) ⟶ Z✝) : CategoryStruct.comp (G.map (kernel.lift f h w)) (CategoryStruct.comp (kernelComparison f G) h✝) = CategoryStruct.comp (kernel.lift (G.map f) (G.map h) ⋯) h✝

theorem CategoryTheory.Limits.kernelComparison_comp_kernel_map {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] {X' Y' : C} [HasKernel f] [HasKernel (G.map f)] (g : X' ⟶ Y') [HasKernel g] [HasKernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryStruct.comp f q = CategoryStruct.comp p g) : CategoryStruct.comp (kernelComparison f G) (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) = CategoryStruct.comp (G.map (kernel.map f g p q hpq)) (kernelComparison g G)

theorem CategoryTheory.Limits.kernelComparison_comp_kernel_map_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] {X' Y' : C} [HasKernel f] [HasKernel (G.map f)] (g : X' ⟶ Y') [HasKernel g] [HasKernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y') (hpq : CategoryStruct.comp f q = CategoryStruct.comp p g) {Z : D} (h : kernel (G.map g) ⟶ Z) : CategoryStruct.comp (kernelComparison f G) (CategoryStruct.comp (kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) h) = CategoryStruct.comp (G.map (kernel.map f g p q hpq)) (CategoryStruct.comp (kernelComparison g G) h)

noncomputable def CategoryTheory.Limits.cokernelComparison {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasCokernel f] [HasCokernel (G.map f)] : cokernel (G.map f) ⟶ G.obj (cokernel f)

The comparison morphism for the cokernel of f.

Equations

• CategoryTheory.Limits.cokernelComparison f G = CategoryTheory.Limits.cokernel.desc (G.map f) (G.map (CategoryTheory.Limits.coequalizer.π f 0)) ⋯

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelComparison {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasCokernel f] [HasCokernel (G.map f)] : CategoryStruct.comp (cokernel.π (G.map f)) (cokernelComparison f G) = G.map (cokernel.π f)

@[simp]

theorem CategoryTheory.Limits.π_comp_cokernelComparison_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasCokernel f] [HasCokernel (G.map f)] {Z : D} (h : G.obj (cokernel f) ⟶ Z) : CategoryStruct.comp (cokernel.π (G.map f)) (CategoryStruct.comp (cokernelComparison f G) h) = CategoryStruct.comp (G.map (cokernel.π f)) h

@[simp]

theorem CategoryTheory.Limits.cokernelComparison_map_desc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z} (w : CategoryStruct.comp f h = 0) : CategoryStruct.comp (cokernelComparison f G) (G.map (cokernel.desc f h w)) = cokernel.desc (G.map f) (G.map h) ⋯

@[simp]

theorem CategoryTheory.Limits.cokernelComparison_map_desc_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] [HasCokernel f] [HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z} (w : CategoryStruct.comp f h = 0) {Z✝ : D} (h✝ : G.obj Z ⟶ Z✝) : CategoryStruct.comp (cokernelComparison f G) (CategoryStruct.comp (G.map (cokernel.desc f h w)) h✝) = CategoryStruct.comp (cokernel.desc (G.map f) (G.map h) ⋯) h✝

theorem CategoryTheory.Limits.cokernel_map_comp_cokernelComparison {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] {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 : CategoryStruct.comp f q = CategoryStruct.comp p g) : CategoryStruct.comp (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) (cokernelComparison g G) = CategoryStruct.comp (cokernelComparison f G) (G.map (cokernel.map f g p q hpq))

theorem CategoryTheory.Limits.cokernel_map_comp_cokernelComparison_assoc {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {X Y : C} (f : X ⟶ Y) {D : Type u₂} [Category.{v₂, u₂} D] [HasZeroMorphisms D] (G : Functor C D) [G.PreservesZeroMorphisms] {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 : CategoryStruct.comp f q = CategoryStruct.comp p g) {Z : D} (h : G.obj (cokernel g) ⟶ Z) : CategoryStruct.comp (cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯) (CategoryStruct.comp (cokernelComparison g G) h) = CategoryStruct.comp (cokernelComparison f G) (CategoryStruct.comp (G.map (cokernel.map f g p q hpq)) h)

class CategoryTheory.Limits.HasKernels (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] : Prop

HasKernels represents the existence of kernels for every morphism.

• has_limit {X Y : C} (f : X ⟶ Y) : HasKernel f

class CategoryTheory.Limits.HasCokernels (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] : Prop

HasCokernels represents the existence of cokernels for every morphism.

• has_colimit {X Y : C} (f : X ⟶ Y) : HasCokernel f

@[instance 100]

instance CategoryTheory.Limits.hasKernels_of_hasEqualizers (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasEqualizers C] : HasKernels C

@[instance 100]

instance CategoryTheory.Limits.hasCokernels_of_hasCoequalizers (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCoequalizers C] : HasCokernels C

noncomputable def CategoryTheory.Limits.ker (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] : Functor (Arrow C) C

The kernel of an arrow is natural.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.ker_obj (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] (f : Arrow C) : (ker C).obj f = kernel f.hom

@[simp]

theorem CategoryTheory.Limits.ker_map (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] {f g : Arrow C} (u : f ⟶ g) : (ker C).map u = kernel.lift g.hom (CategoryStruct.comp (kernel.ι f.hom) u.left) ⋯

noncomputable def CategoryTheory.Limits.ker.ι (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] : ker C ⟶ Arrow.leftFunc

The kernel inclusion is natural.

Equations

• CategoryTheory.Limits.ker.ι C = { app := fun (f : CategoryTheory.Arrow C) => CategoryTheory.Limits.kernel.ι f.hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Limits.ker.ι_app (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] (f : Arrow C) : (ι C).app f = kernel.ι f.hom

@[simp]

theorem CategoryTheory.Limits.ker.condition (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] : CategoryStruct.comp (ι C) Arrow.leftToRight = 0

@[simp]

theorem CategoryTheory.Limits.ker.condition_assoc (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasKernels C] {Z : Functor (Arrow C) C} (h : Arrow.rightFunc ⟶ Z) : CategoryStruct.comp (ι C) (CategoryStruct.comp Arrow.leftToRight h) = CategoryStruct.comp 0 h

noncomputable def CategoryTheory.Limits.coker (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] : Functor (Arrow C) C

The cokernel of an arrow is natural.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.coker_obj (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] (f : Arrow C) : (coker C).obj f = cokernel f.hom

@[simp]

theorem CategoryTheory.Limits.coker_map (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] {f g : Arrow C} (u : f ⟶ g) : (coker C).map u = cokernel.desc f.hom (CategoryStruct.comp u.right (cokernel.π g.hom)) ⋯

noncomputable def CategoryTheory.Limits.coker.π (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] : Arrow.rightFunc ⟶ coker C

The cokernel projection is natural.

Equations

• CategoryTheory.Limits.coker.π C = { app := fun (f : CategoryTheory.Arrow C) => CategoryTheory.Limits.cokernel.π f.hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Limits.coker.π_app (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] (f : Arrow C) : (π C).app f = cokernel.π f.hom

@[simp]

theorem CategoryTheory.Limits.coker.condition (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] : CategoryStruct.comp Arrow.leftToRight (π C) = 0

@[simp]

theorem CategoryTheory.Limits.coker.condition_assoc (C : Type u) [Category.{v, u} C] [HasZeroMorphisms C] [HasCokernels C] {Z : Functor (Arrow C) C} (h : coker C ⟶ Z) : CategoryStruct.comp Arrow.leftToRight (CategoryStruct.comp (π C) h) = CategoryStruct.comp 0 h