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.

Instances

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

Instances
def category_theory.limits.kernel_fork {C : Type u} [category_theory.category C] [category_theory.limits.has_zero_morphisms C] {X Y : C} :
(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 some l : W ⟶ s.X such that l ≫ 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)) :
(∀ {W' : C} (g' : W' X) (eq' : g' f = 0), lift g' eq' g = g')(∀ {W' : C} (g' : W' X) (eq' : g' f = 0) (m : W' W), m g = g'm = lift g' eq')category_theory.limits.is_limit (category_theory.limits.kernel_fork.of_ι 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

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

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')) :
(∀ {Z' : C} (g' : Y Z') (eq' : f g' = 0), g desc g' eq' = g')(∀ {Z' : C} (g' : Y Z') (eq' : f g' = 0) (m : Z Z'), g m = g'm = desc g' eq')category_theory.limits.is_colimit (category_theory.limits.cokernel_cofork.of_π 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