mathlib documentation

category_theory.limits.shapes.kernels

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

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 #

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

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

def category_theory.limits.kernel_fork {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms 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.

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

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

Equations

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

Equations

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

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

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

The kernel morphism of a zero morphism is an isomorphism

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

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

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

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

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

has_kernels represents the existence of kernels for every morphism.

Instances
@[class]

has_cokernels represents the existence of cokernels for every morphism.

Instances