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) → Ckernel.ι : kernel f ⟶ Xkernel.condition : kernel.ι f ≫ f = 0andkernel.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.ι fis an epimorphism, thenf = 0kernel.of_mono: the kernel of a monomorphism is the zero objectkernel.lift_mono: the lift of a monomorphismk : W ⟶ Xsuch thatk ≫ f = 0is 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
abbreviations of the general statements for limits, so all the simp lemmas and theorems about
general limits can be used.
References
- [F. Borceux, Handbook of Categorical Algebra 2][borceux-vol2]
def
category_theory.limits.has_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
(X ⟶ Y) → Prop
A morphism f has a kernel if the functor parallel_pair f 0 has a limit.
def
category_theory.limits.has_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
(X ⟶ Y) → Prop
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} :
(X ⟶ Y) → Type (max u v)
A kernel fork is just a fork where the second morphism is a zero morphism.
@[simp]
theorem
category_theory.limits.kernel_fork.condition
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.kernel_fork f) :
category_theory.limits.fork.ι s ≫ f = 0
@[simp]
theorem
category_theory.limits.kernel_fork.condition_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.kernel_fork f)
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.fork.ι s ≫ f ≫ f' = 0 ≫ f'
@[simp]
theorem
category_theory.limits.kernel_fork.app_one
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.kernel_fork f) :
def
category_theory.limits.kernel_fork.of_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{Z : C}
(ι : Z ⟶ X) :
ι ≫ f = 0 → category_theory.limits.kernel_fork f
A morphism ι satisfying ι ≫ f = 0 determines a kernel fork over f.
@[simp]
theorem
category_theory.limits.kernel_fork.ι_of_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y P : C}
(f : X ⟶ Y)
(ι : P ⟶ X)
(w : ι ≫ f = 0) :
def
category_theory.limits.iso_of_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.fork f 0) :
Every kernel fork s is isomorphic (actually, equal) to fork.of_ι (fork.ι s) _.
def
category_theory.limits.of_ι_congr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{P : C}
{ι ι' : P ⟶ X}
{w : ι ≫ f = 0}
(h : ι = ι') :
If ι = ι', then fork.of_ι ι _ and fork.of_ι ι' _ are isomorphic.
def
category_theory.limits.comp_nat_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{D : Type u'}
[category_theory.category D]
[category_theory.limits.has_zero_morphisms D]
(F : C ⥤ D)
[category_theory.is_equivalence F] :
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)
def
category_theory.limits.kernel_fork.is_limit.lift'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{s : category_theory.limits.kernel_fork f}
(hs : category_theory.limits.is_limit s)
{W : C}
(k : W ⟶ X) :
k ≫ f = 0 → {l // l ≫ category_theory.limits.fork.ι s = k}
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
def
category_theory.limits.is_limit_aux
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(t : category_theory.limits.kernel_fork f)
(lift : Π (s : category_theory.limits.kernel_fork f), s.X ⟶ t.X) :
(∀ (s : category_theory.limits.kernel_fork f), lift s ≫ category_theory.limits.fork.ι t = category_theory.limits.fork.ι s) → (∀ (s : category_theory.limits.kernel_fork f) (m : s.X ⟶ t.X), m ≫ category_theory.limits.fork.ι t = category_theory.limits.fork.ι s → m = lift s) → category_theory.limits.is_limit t
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
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)) :
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) _) _ _
def
category_theory.limits.kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
C
The kernel of a morphism, expressed as the equalizer with the 0 morphism.
def
category_theory.limits.kernel.ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
The map from kernel f into the source of f.
@[simp]
theorem
category_theory.limits.equalizer_as_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
@[simp]
theorem
category_theory.limits.kernel.condition_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.kernel.ι f ≫ f ≫ f' = 0 ≫ f'
@[simp]
theorem
category_theory.limits.kernel.condition
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f] :
def
category_theory.limits.kernel.lift
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X) :
k ≫ f = 0 → (W ⟶ category_theory.limits.kernel f)
Given any morphism k : W ⟶ X satisfying k ≫ f = 0, k factors through kernel.ι f
via kernel.lift : W ⟶ kernel f.
@[simp]
theorem
category_theory.limits.kernel.lift_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X)
(h : k ≫ f = 0) :
@[simp]
theorem
category_theory.limits.kernel.lift_ι_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X)
(h : k ≫ f = 0)
{X' : C}
(f' : X ⟶ X') :
category_theory.limits.kernel.lift f k h ≫ category_theory.limits.kernel.ι f ≫ f' = k ≫ f'
@[simp]
theorem
category_theory.limits.kernel.lift_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
{h : 0 ≫ f = 0} :
category_theory.limits.kernel.lift f 0 h = 0
@[instance]
def
category_theory.limits.kernel.lift_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X)
(h : k ≫ f = 0)
[category_theory.mono k] :
def
category_theory.limits.kernel.lift'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{W : C}
(k : W ⟶ X) :
k ≫ f = 0 → {l // l ≫ category_theory.limits.kernel.ι f = k}
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, _⟩
@[instance]
def
category_theory.limits.kernel.ι_zero_is_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
Every kernel of the zero morphism is an isomorphism
theorem
category_theory.limits.eq_zero_of_epi_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
[category_theory.epi (category_theory.limits.kernel.ι f)] :
f = 0
def
category_theory.limits.kernel_zero_iso_source
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
The kernel of a zero morphism is isomorphic to the source.
@[simp]
theorem
category_theory.limits.kernel_zero_iso_source_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
@[simp]
theorem
category_theory.limits.kernel_zero_iso_source_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
def
category_theory.limits.kernel_iso_of_eq
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f g : X ⟶ Y}
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel g] :
f = g → (category_theory.limits.kernel f ≅ category_theory.limits.kernel g)
If two morphisms are known to be equal, then their kernels are isomorphic.
@[simp]
theorem
category_theory.limits.kernel_iso_of_eq_refl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{h : f = f} :
@[simp]
theorem
category_theory.limits.kernel_iso_of_eq_trans
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f g h : X ⟶ Y}
[category_theory.limits.has_kernel f]
[category_theory.limits.has_kernel g]
[category_theory.limits.has_kernel h]
(w₁ : f = g)
(w₂ : g = h) :
theorem
category_theory.limits.kernel_not_epi_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_kernel f] :
theorem
category_theory.limits.kernel_not_iso_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_kernel f] :
f ≠ 0 → category_theory.is_iso (category_theory.limits.kernel.ι f) → false
def
category_theory.limits.kernel_comp_is_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.limits.has_kernel f]
[category_theory.is_iso g] :
When g is an isomorphism, the kernel of f ≫ g is isomorphic to the kernel of f.
Equations
- category_theory.limits.kernel_comp_is_iso 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' := _}
@[simp]
theorem
category_theory.limits.kernel_comp_is_iso_hom_comp_kernel_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.limits.has_kernel f]
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.kernel_comp_is_iso_inv_comp_kernel_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.limits.has_kernel f]
[category_theory.is_iso g] :
def
category_theory.limits.kernel_is_iso_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_kernel g] :
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.is_iso.inv f) _, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.kernel_is_iso_comp_hom_comp_kernel_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_kernel g] :
@[simp]
theorem
category_theory.limits.kernel_is_iso_comp_inv_comp_kernel_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_kernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_kernel g] :
def
category_theory.limits.kernel.zero_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C] :
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' := _}}
def
category_theory.limits.kernel.is_limit_cone_zero_cone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.mono f] :
The map from the zero object is a kernel of a monomorphism
Equations
def
category_theory.limits.kernel.of_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_kernel f]
[category_theory.mono f] :
The kernel of a monomorphism is isomorphic to the zero object
Equations
theorem
category_theory.limits.kernel.ι_of_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_kernel f]
[category_theory.mono f] :
The kernel morphism of a monomorphism is a zero morphism
def
category_theory.limits.is_kernel.of_comp_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
{Z : C}
(l : X ⟶ Z)
(i : Z ≅ Y)
(h : l ≫ i.hom = f)
{s : category_theory.limits.kernel_fork f} :
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.ι _)) _ _
def
category_theory.limits.kernel.of_comp_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{Z : C}
(l : X ⟶ Z)
(i : Z ≅ Y)
(h : l ≫ i.hom = f) :
If i is an isomorphism such that l ≫ i.hom = f, then the kernel of f is a kernel of l.
def
category_theory.limits.is_kernel.iso_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Z ⟶ X)
{s : category_theory.limits.kernel_fork f}
(hs : category_theory.limits.is_limit s)
(i : Z ≅ s.X)
(h : i.hom ≫ category_theory.limits.fork.ι s = 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 _)
def
category_theory.limits.kernel.iso_kernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_kernel f]
{Z : C}
(l : Z ⟶ X)
(i : Z ≅ category_theory.limits.kernel f)
(h : i.hom ≫ category_theory.limits.kernel.ι f = l) :
If i is an isomorphism such that i.hom ≫ kernel.ι f = l, then l is a kernel of f.
def
category_theory.limits.kernel.ι_of_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C) :
The kernel morphism of a zero morphism is an isomorphism
def
category_theory.limits.cokernel_cofork
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
(X ⟶ Y) → Type (max u v)
A cokernel cofork is just a cofork where the second morphism is a zero morphism.
@[simp]
theorem
category_theory.limits.cokernel_cofork.condition_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.cokernel_cofork f)
{X' : C}
(f' : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj s.X).obj category_theory.limits.walking_parallel_pair.one ⟶ X') :
f ≫ category_theory.limits.cofork.π s ≫ f' = 0 ≫ f'
@[simp]
theorem
category_theory.limits.cokernel_cofork.condition
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.cokernel_cofork f) :
@[simp]
theorem
category_theory.limits.cokernel_cofork.app_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.cokernel_cofork f) :
def
category_theory.limits.cokernel_cofork.of_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{Z : C}
(π : Y ⟶ Z) :
f ≫ «π» = 0 → category_theory.limits.cokernel_cofork f
A morphism π satisfying f ≫ π = 0 determines a cokernel cofork on f.
@[simp]
theorem
category_theory.limits.cokernel_cofork.π_of_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y P : C}
(f : X ⟶ Y)
(π : Y ⟶ P)
(w : f ≫ «π» = 0) :
def
category_theory.limits.iso_of_π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(s : category_theory.limits.cofork f 0) :
Every cokernel cofork s is isomorphic (actually, equal) to cofork.of_π (cofork.π s) _.
def
category_theory.limits.of_π_congr
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{P : C}
{π π' : Y ⟶ P}
{w : f ≫ «π» = 0}
(h : «π» = π') :
If π = π', then cokernel_cofork.of_π π _ and cokernel_cofork.of_π π' _ are isomorphic.
def
category_theory.limits.cokernel_cofork.is_colimit.desc'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
{s : category_theory.limits.cokernel_cofork f}
(hs : category_theory.limits.is_colimit s)
{W : C}
(k : Y ⟶ W) :
f ≫ k = 0 → {l // category_theory.limits.cofork.π s ≫ l = k}
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
def
category_theory.limits.is_colimit_aux
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
(t : category_theory.limits.cokernel_cofork f)
(desc : Π (s : category_theory.limits.cokernel_cofork f), t.X ⟶ s.X) :
(∀ (s : category_theory.limits.cokernel_cofork f), category_theory.limits.cofork.π t ≫ desc s = category_theory.limits.cofork.π s) → (∀ (s : category_theory.limits.cokernel_cofork f) (m : t.X ⟶ s.X), category_theory.limits.cofork.π t ≫ m = category_theory.limits.cofork.π s → m = desc s) → category_theory.limits.is_colimit t
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
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')) :
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) _) _ _
def
category_theory.limits.cokernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f] :
C
The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.
def
category_theory.limits.cokernel.π
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f] :
The map from the target of f to cokernel f.
@[simp]
theorem
category_theory.limits.coequalizer_as_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f] :
@[simp]
theorem
category_theory.limits.cokernel.condition
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f] :
@[simp]
theorem
category_theory.limits.cokernel.condition_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{X' : C}
(f' : category_theory.limits.cokernel f ⟶ X') :
f ≫ category_theory.limits.cokernel.π f ≫ f' = 0 ≫ f'
def
category_theory.limits.cokernel.desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W) :
f ≫ k = 0 → (category_theory.limits.cokernel f ⟶ W)
Given any morphism k : Y ⟶ W such that f ≫ k = 0, k factors through cokernel.π f
via cokernel.desc : cokernel f ⟶ W.
@[simp]
theorem
category_theory.limits.cokernel.π_desc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W)
(h : f ≫ k = 0) :
@[simp]
theorem
category_theory.limits.cokernel.π_desc_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W)
(h : f ≫ k = 0)
{X' : C}
(f' : W ⟶ X') :
category_theory.limits.cokernel.π f ≫ category_theory.limits.cokernel.desc f k h ≫ f' = k ≫ f'
@[simp]
theorem
category_theory.limits.cokernel.desc_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
{h : f ≫ 0 = 0} :
@[instance]
def
category_theory.limits.cokernel.desc_epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W)
(h : f ≫ k = 0)
[category_theory.epi k] :
def
category_theory.limits.cokernel.desc'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{W : C}
(k : Y ⟶ W) :
f ≫ k = 0 → {l // category_theory.limits.cokernel.π f ≫ l = k}
Any morphism k : Y ⟶ W satisfying f ≫ k = 0 induces l : cokernel f ⟶ W such that
cokernel.π f ≫ l = k.
Equations
@[instance]
def
category_theory.limits.cokernel.π_zero_is_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
The cokernel of the zero morphism is an isomorphism
theorem
category_theory.limits.eq_zero_of_mono_cokernel
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
[category_theory.mono (category_theory.limits.cokernel.π f)] :
f = 0
def
category_theory.limits.cokernel_zero_iso_target
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
The cokernel of a zero morphism is isomorphic to the target.
@[simp]
theorem
category_theory.limits.cokernel_zero_iso_target_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C} :
@[simp]
def
category_theory.limits.cokernel_iso_of_eq
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f g : X ⟶ Y}
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel g] :
If two morphisms are known to be equal, then their cokernels are isomorphic.
@[simp]
theorem
category_theory.limits.cokernel_iso_of_eq_refl
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{h : f = f} :
@[simp]
theorem
category_theory.limits.cokernel_iso_of_eq_trans
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f g h : X ⟶ Y}
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel g]
[category_theory.limits.has_cokernel h]
(w₁ : f = g)
(w₂ : g = h) :
theorem
category_theory.limits.cokernel_not_mono_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_cokernel f] :
theorem
category_theory.limits.cokernel_not_iso_of_nonzero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
{f : X ⟶ Y}
[category_theory.limits.has_cokernel f] :
def
category_theory.limits.cokernel_comp_is_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.limits.has_cokernel f]
[category_theory.is_iso g] :
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.is_iso.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' := _}
@[simp]
theorem
category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.limits.has_cokernel f]
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.limits.cokernel_π_comp_cokernel_comp_is_iso_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.limits.has_cokernel f]
[category_theory.is_iso g] :
def
category_theory.limits.cokernel_is_iso_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_cokernel g] :
When f is an isomorphism, the cokernel of f ≫ g is isomorphic to the cokernel of g.
Equations
- category_theory.limits.cokernel_is_iso_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' := _}
@[simp]
theorem
category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_cokernel g] :
@[simp]
theorem
category_theory.limits.cokernel_π_comp_cokernel_is_iso_comp_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[category_theory.limits.has_cokernel (f ≫ g)]
[category_theory.is_iso f]
[category_theory.limits.has_cokernel g] :
def
category_theory.limits.cokernel.zero_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C] :
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' := _}}
def
category_theory.limits.cokernel.is_colimit_cocone_zero_cocone
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.epi f] :
The morphism to the zero object is a cokernel of an epimorphism
def
category_theory.limits.cokernel.of_epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_cokernel f]
[category_theory.epi f] :
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))
theorem
category_theory.limits.cokernel.π_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_cokernel f]
[category_theory.epi f] :
The cokernel morphism of an epimorphism is a zero morphism
def
category_theory.limits.cokernel_image_ι
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[category_theory.limits.has_cokernel (category_theory.limits.image.ι f)]
[category_theory.limits.has_cokernel f]
[category_theory.epi (category_theory.limits.factor_thru_image f)] :
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' := _}
@[simp]
theorem
category_theory.limits.cokernel_image_ι_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[category_theory.limits.has_cokernel (category_theory.limits.image.ι f)]
[category_theory.limits.has_cokernel f]
[category_theory.epi (category_theory.limits.factor_thru_image f)] :
@[simp]
theorem
category_theory.limits.cokernel_image_ι_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_image f]
[category_theory.limits.has_cokernel (category_theory.limits.image.ι f)]
[category_theory.limits.has_cokernel f]
[category_theory.epi (category_theory.limits.factor_thru_image f)] :
def
category_theory.limits.cokernel.π_of_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
(X Y : C) :
The cokernel of a zero morphism is an isomorphism
@[instance]
def
category_theory.limits.kernel.of_cokernel_of_epi
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_kernel (category_theory.limits.cokernel.π f)]
[category_theory.epi f] :
The kernel of the cokernel of an epimorphism is an isomorphism
@[instance]
def
category_theory.limits.cokernel.of_kernel_of_mono
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_kernel f]
[category_theory.limits.has_cokernel (category_theory.limits.kernel.ι f)]
[category_theory.mono f] :
The cokernel of the kernel of a monomorphism is an isomorphism
def
category_theory.limits.is_cokernel.of_iso_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Z ⟶ Y)
(i : X ≅ Z)
(h : i.hom ≫ l = f)
{s : category_theory.limits.cokernel_cofork f} :
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.π _)) _ _
def
category_theory.limits.cokernel.of_iso_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{Z : C}
(l : Z ⟶ Y)
(i : X ≅ Z)
(h : i.hom ≫ l = f) :
If i is an isomorphism such that i.hom ≫ l = f, then the cokernel of f is a cokernel of
l.
def
category_theory.limits.is_cokernel.cokernel_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Y ⟶ Z)
{s : category_theory.limits.cokernel_cofork f}
(hs : category_theory.limits.is_colimit s)
(i : s.X ≅ Z)
(h : category_theory.limits.cofork.π s ≫ i.hom = 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
def
category_theory.limits.cokernel.cokernel_iso
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C]
{X Y : C}
(f : X ⟶ Y)
[category_theory.limits.has_cokernel f]
{Z : C}
(l : Y ⟶ Z)
(i : category_theory.limits.cokernel f ≅ Z)
(h : category_theory.limits.cokernel.π f ≫ i.hom = l) :
If i is an isomorphism such that cokernel.π f ≫ i.hom = l, then l is a cokernel of f.
@[class]
structure
category_theory.limits.has_kernels
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Prop
- has_limit : ∀ {X Y : C} (f : X ⟶ Y), category_theory.limits.has_kernel f
has_kernels represents the existence of kernels for every morphism.
@[class]
structure
category_theory.limits.has_cokernels
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_zero_morphisms C] :
Prop
- has_colimit : ∀ {X Y : C} (f : X ⟶ Y), category_theory.limits.has_cokernel f
has_cokernels represents the existence of cokernels for every morphism.
@[instance]