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.ι_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.kernel_fork.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) _) _ _
Every kernel of f
induces a kernel of f ≫ g
if g
is mono.
Equations
- category_theory.limits.is_kernel_comp_mono i g hh = category_theory.limits.fork.is_limit.mk' (category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι c) _) (λ (s : category_theory.limits.fork h 0), let s' : category_theory.limits.kernel_fork f := category_theory.limits.fork.of_ι s.ι _, l : {l // l ≫ category_theory.limits.fork.ι c = category_theory.limits.fork.ι s'} := category_theory.limits.kernel_fork.is_limit.lift' i (category_theory.limits.fork.ι s') _ in ⟨l.val, _⟩)
Every kernel of f ≫ g
is also a kernel of f
, as long as c.ι ≫ f
vanishes.
Equations
- category_theory.limits.is_kernel_of_comp g h i hf hfg = category_theory.limits.fork.is_limit.mk (category_theory.limits.kernel_fork.of_ι (category_theory.limits.fork.ι c) hf) (λ (s : category_theory.limits.fork f 0), i.lift (category_theory.limits.kernel_fork.of_ι s.ι _)) _ _
The kernel of a morphism, expressed as the equalizer with the 0 morphism.
The map from kernel f
into the source of f
.
The kernel built from kernel.ι f
is limiting.
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, _⟩
A commuting square induces a morphism of kernels.
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
- category_theory.limits.kernel.map_iso f f' p q w = {hom := category_theory.limits.kernel.map f f' p.hom q.hom w, inv := category_theory.limits.kernel.map f' f p.inv q.inv _, hom_inv_id' := _, inv_hom_id' := _}
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_kernel_fork 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
The kernel of a monomorphism is isomorphic to the zero object
Equations
The kernel morphism of a monomorphism is a zero morphism
If g ≫ f = 0
implies g = 0
for all g
, then 0 : 0 ⟶ X
is a kernel of f
.
Equations
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.cokernel_cofork.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) _) _ _
Every cokernel of f
induces a cokernel of g ≫ f
if g
is epi.
Equations
- category_theory.limits.is_cokernel_epi_comp i g hh = category_theory.limits.cofork.is_colimit.mk' (category_theory.limits.cokernel_cofork.of_π (category_theory.limits.cofork.π c) _) (λ (s : category_theory.limits.cofork h 0), let s' : category_theory.limits.cokernel_cofork f := category_theory.limits.cofork.of_π s.π _, l : {l // category_theory.limits.cofork.π c ≫ l = category_theory.limits.cofork.π s'} := category_theory.limits.cokernel_cofork.is_colimit.desc' i (category_theory.limits.cofork.π s') _ in ⟨l.val, _⟩)
Every cokernel of g ≫ f
is also a cokernel of f
, as long as f ≫ c.π
vanishes.
Equations
The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.
The map from the target of f
to cokernel f
.
The cokernel built from cokernel.π f
is colimiting.
Equations
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
A commuting square induces a morphism of cokernels.
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
- category_theory.limits.cokernel.map_iso f f' p q w = {hom := category_theory.limits.cokernel.map f f' p.hom q.hom w, inv := category_theory.limits.cokernel.map f' f p.inv q.inv _, hom_inv_id' := _, inv_hom_id' := _}
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_cokernel_cofork 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 f ≫ g = 0
implies g = 0
for all g
, then 0 : Y ⟶ 0
is a cokernel of f
.
Equations
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
.
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
Instances for category_theory.limits.kernel_comparison
The comparison morphism for the cokernel of f
.
Equations
Instances for category_theory.limits.cokernel_comparison
- 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.