mathlib3 documentation

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

Main statements #

Besides the definition and lifts, we prove

and the corresponding dual statements.

Future work #

Implementation notes #

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

References #

@[reducible]

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

@[reducible]

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

@[reducible]

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

@[reducible]

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

If s is a limit kernel fork and k : W ⟶ X satisfies ``k ≫ f = 0, then there is somel : W ⟶ s.Xsuch thatl ≫ fork.ι s = k`.

Equations

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} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {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
@[reducible]

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

@[reducible]

The map from kernel f into the source of f.

@[reducible]

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

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

Equations
@[reducible]

A commuting square induces a morphism of kernels.

theorem category_theory.limits.kernel.lift_map {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z X' Y' Z' : C} (f : X Y) (g : Y Z) [category_theory.limits.has_kernel g] (w : f g = 0) (f' : X' Y') (g' : Y' Z') [category_theory.limits.has_kernel g'] (w' : f' g' = 0) (p : X X') (q : Y Y') (r : Z Z') (h₁ : f q = p f') (h₂ : g r = q g') :

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'

A commuting square of isomorphisms induces an isomorphism of kernels.

Equations
@[protected, instance]

Every kernel of the zero morphism is an isomorphism

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
@[reducible]

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

@[reducible]

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

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

Equations

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

Equations

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

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} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {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
@[reducible]

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

@[reducible]

The map from the target of f to cokernel f.

@[reducible]

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

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

Equations
@[reducible]

A commuting square induces a morphism of cokernels.

theorem category_theory.limits.cokernel.map_desc {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y Z X' Y' Z' : C} (f : X Y) [category_theory.limits.has_cokernel f] (g : Y Z) (w : f g = 0) (f' : X' Y') [category_theory.limits.has_cokernel f'] (g' : Y' Z') (w' : f' g' = 0) (p : X X') (q : Y Y') (r : Z Z') (h₁ : f q = p f') (h₂ : g r = q g') :

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'

A commuting square of isomorphisms induces an isomorphism of cokernels.

Equations
@[protected, instance]

The cokernel of the zero morphism is an isomorphism

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

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
@[class]

has_kernels represents the existence of kernels for every morphism.

Instances of this typeclass
@[class]

has_cokernels represents the existence of cokernels for every morphism.

Instances of this typeclass