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
andkernel.lift (k : W ⟶ X) (h : k ≫ f = 0) : W ⟶ kernel f
(as well as the dual versions)
Main statements #
Besides the definition and lifts, we prove
kernel.ι_zero_is_iso
: a kernel map of a zero morphism is an isomorphismkernel.eq_zero_of_epi_kernel
: ifkernel.ι f
is an epimorphism, thenf = 0
kernel.of_mono
: the kernel of a monomorphism is the zero objectkernel.lift_mono
: the lift of a monomorphismk : W ⟶ X
such thatk ≫ f = 0
is still a monomorphismkernel.is_limit_cone_zero_cone
: if our category has a zero object, then the map from the zero obect is a kernel map of any monomorphismkernel.ι_of_zero
:kernel.ι (0 : X ⟶ Y)
is an isomorphism
and the corresponding dual statements.
Future work #
- TODO: connect this with existing working in the group theory and ring theory libraries.
Implementation notes #
As with the other special shapes in the limits library, all the definitions here are given as
abbreviation
s of the general statements for limits, so all the simp
lemmas and theorems about
general limits can be used.
References #
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.
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) _
.
If ι = ι'
, then fork.of_ι ι _
and fork.of_ι ι' _
are isomorphic.
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
- category_theory.limits.comp_nat_iso F = category_theory.nat_iso.of_components (λ (j : category_theory.limits.walking_parallel_pair), category_theory.limits.comp_nat_iso._match_1 F j) _
- category_theory.limits.comp_nat_iso._match_1 F category_theory.limits.walking_parallel_pair.one = category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ F).obj category_theory.limits.walking_parallel_pair.one)
- category_theory.limits.comp_nat_iso._match_1 F category_theory.limits.walking_parallel_pair.zero = category_theory.iso.refl ((category_theory.limits.parallel_pair f 0 ⋙ F).obj category_theory.limits.walking_parallel_pair.zero)
If s
is a limit kernel fork and k : W ⟶ X
satisfies ``k ≫ f = 0, then there is some
l : W ⟶ s.Xsuch 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
This is a more convenient formulation to show that a kernel_fork
constructed using
kernel_fork.of_ι
is a limit cone.
Equations
- category_theory.limits.is_limit.of_ι g eq lift fac uniq = category_theory.limits.is_limit_aux (category_theory.limits.kernel_fork.of_ι g eq) (λ (s : category_theory.limits.kernel_fork f), lift (category_theory.limits.fork.ι s) _) _ _
The kernel of a morphism, expressed as the equalizer with the 0 morphism.
The map from kernel f
into the source of f
.
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
- category_theory.limits.kernel.lift' f k h = ⟨category_theory.limits.kernel.lift f k h, _⟩
Every kernel of the zero morphism is an isomorphism
The kernel of a zero morphism is isomorphic to the source.
If two morphisms are known to be equal, then their kernels are isomorphic.
When g
is a monomorphism, the kernel of f ≫ g
is isomorphic to the kernel of f
.
Equations
- category_theory.limits.kernel_comp_mono f g = {hom := category_theory.limits.kernel.lift f (category_theory.limits.kernel.ι (f ≫ g)) _, inv := category_theory.limits.kernel.lift (f ≫ g) (category_theory.limits.kernel.ι f) _, hom_inv_id' := _, inv_hom_id' := _}
When f
is an isomorphism, the kernel of f ≫ g
is isomorphic to the kernel of g
.
Equations
- category_theory.limits.kernel_is_iso_comp f g = {hom := category_theory.limits.kernel.lift g (category_theory.limits.kernel.ι (f ≫ g) ≫ f) _, inv := category_theory.limits.kernel.lift (f ≫ g) (category_theory.limits.kernel.ι g ≫ category_theory.inv f) _, hom_inv_id' := _, inv_hom_id' := _}
The morphism from the zero object determines a cone on a kernel diagram
Equations
- category_theory.limits.kernel.zero_cone f = {X := 0, π := {app := λ (j : category_theory.limits.walking_parallel_pair), 0, naturality' := _}}
The map from the zero object is a kernel of a monomorphism
Equations
The kernel of a monomorphism is isomorphic to the zero object
Equations
The kernel morphism of a monomorphism is a zero morphism
If i
is an isomorphism such that l ≫ i.hom = f
, then any kernel of f
is a kernel of l
.
Equations
- category_theory.limits.is_kernel.of_comp_iso f l i h hs = category_theory.limits.fork.is_limit.mk (category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι s) _) (λ (s_1 : category_theory.limits.fork l 0), hs.lift (category_theory.limits.kernel_fork.of_ι s_1.ι _)) _ _
If i
is an isomorphism such that l ≫ i.hom = f
, then the kernel of f
is a kernel 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
- category_theory.limits.is_kernel.iso_kernel f l hs i h = hs.of_iso_limit (category_theory.limits.cones.ext i.symm _)
If i
is an isomorphism such that i.hom ≫ kernel.ι f = l
, then l
is a kernel of f
.
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) _
.
If π = π'
, then cokernel_cofork.of_π π _
and cokernel_cofork.of_π π' _
are isomorphic.
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
This is a more convenient formulation to show that a cokernel_cofork
constructed using
cokernel_cofork.of_π
is a limit cone.
Equations
- category_theory.limits.is_colimit.of_π g eq desc fac uniq = category_theory.limits.is_colimit_aux (category_theory.limits.cokernel_cofork.of_π g eq) (λ (s : category_theory.limits.cokernel_cofork f), desc (category_theory.limits.cofork.π s) _) _ _
The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.
The map from the target of f
to cokernel f
.
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
The cokernel of the zero morphism is an isomorphism
The cokernel of a zero morphism is isomorphic to the target.
If two morphisms are known to be equal, then their cokernels are isomorphic.
When g
is an isomorphism, the cokernel of f ≫ g
is isomorphic to the cokernel of f
.
Equations
- category_theory.limits.cokernel_comp_is_iso f g = {hom := category_theory.limits.cokernel.desc (f ≫ g) (category_theory.inv g ≫ category_theory.limits.cokernel.π f) _, inv := category_theory.limits.cokernel.desc f (g ≫ category_theory.limits.cokernel.π (f ≫ g)) _, hom_inv_id' := _, inv_hom_id' := _}
When f
is an epimorphism, the cokernel of f ≫ g
is isomorphic to the cokernel of g
.
Equations
- category_theory.limits.cokernel_epi_comp f g = {hom := category_theory.limits.cokernel.desc (f ≫ g) (category_theory.limits.cokernel.π g) _, inv := category_theory.limits.cokernel.desc g (category_theory.limits.cokernel.π (f ≫ g)) _, hom_inv_id' := _, inv_hom_id' := _}
The morphism to the zero object determines a cocone on a cokernel diagram
Equations
- category_theory.limits.cokernel.zero_cocone f = {X := 0, ι := {app := λ (j : category_theory.limits.walking_parallel_pair), 0, naturality' := _}}
The morphism to the zero object is a cokernel of an epimorphism
The cokernel of an epimorphism is isomorphic to the zero object
Equations
- category_theory.limits.cokernel.of_epi f = (category_theory.limits.cocones.forget (category_theory.limits.parallel_pair f 0)).map_iso ((category_theory.limits.colimit.is_colimit (category_theory.limits.parallel_pair f 0)).unique_up_to_iso (category_theory.limits.cokernel.is_colimit_cocone_zero_cocone f))
The cokernel morphism of an epimorphism is a zero morphism
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
- category_theory.limits.cokernel_image_ι f = {hom := category_theory.limits.cokernel.desc (category_theory.limits.image.ι f) (category_theory.limits.cokernel.π f) _, inv := category_theory.limits.cokernel.desc f (category_theory.limits.cokernel.π (category_theory.limits.image.ι f)) _, hom_inv_id' := _, inv_hom_id' := _}
The cokernel of a zero morphism is an isomorphism
The kernel of the cokernel of an epimorphism is an isomorphism
The cokernel of the kernel of a monomorphism is an isomorphism
If i
is an isomorphism such that i.hom ≫ l = f
, then any cokernel of f
is a cokernel of
l
.
Equations
- category_theory.limits.is_cokernel.of_iso_comp f l i h hs = category_theory.limits.cofork.is_colimit.mk (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.cofork.π s) _) (λ (s_1 : category_theory.limits.cofork l 0), hs.desc (category_theory.limits.cokernel_cofork.of_π s_1.π _)) _ _
If i
is an isomorphism such that i.hom ≫ l = f
, then the cokernel of f
is a cokernel 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
If i
is an isomorphism such that cokernel.π f ≫ i.hom = l
, then l
is a cokernel of f
.
- has_limit : (∀ {X Y : C} (f : X ⟶ Y), category_theory.limits.has_kernel f) . "apply_instance"
has_kernels
represents the existence of kernels for every morphism.
- has_colimit : (∀ {X Y : C} (f : X ⟶ Y), category_theory.limits.has_cokernel f) . "apply_instance"
has_cokernels
represents the existence of cokernels for every morphism.