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.condition : kernel.ι f ≫ f = 0and -
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.ιZeroIsIso: a kernel map of a zero morphism is an isomorphismkernel.eq_zero_of_epi_kernel: ifkernel.ι fis an epimorphism, thenf = 0kernel.ofMono: the kernel of a monomorphism is the zero objectkernel.liftMono: the lift of a monomorphismk : W ⟶ Xsuch thatk ≫ f = 0is still a monomorphismkernel.isLimitConeZeroCone: if our category has a zero object, then the map from the zero object is a kernel map of any monomorphismkernel.ιOfZero:kernel.ι (0 : X ⟶ Y)is an isomorphism
and the corresponding dual statements.
Future work #
- TODO: connect this with existing work 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]
@[inline, reducible]
abbrev
CategoryTheory.Limits.HasKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A morphism f has a kernel if the functor ParallelPair f 0 has a limit.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.HasCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
A morphism f has a cokernel if the functor ParallelPair f 0 has a colimit.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.KernelFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type (max u v)
A kernel fork is just a fork where the second morphism is a zero morphism.
Instances For
@[simp]
theorem
CategoryTheory.Limits.KernelFork.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.KernelFork f)
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.KernelFork.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.KernelFork f)
:
theorem
CategoryTheory.Limits.KernelFork.app_one
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.KernelFork f)
:
@[inline, reducible]
abbrev
CategoryTheory.Limits.KernelFork.ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Z : C}
(ι : Z ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = 0)
:
A morphism ι satisfying ι ≫ f = 0 determines a kernel fork over f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.KernelFork.ι_ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{P : C}
(f : X ⟶ Y)
(ι : P ⟶ X)
(w : CategoryTheory.CategoryStruct.comp ι f = 0)
:
def
CategoryTheory.Limits.isoOfι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.Fork f 0)
:
Every kernel fork s is isomorphic (actually, equal) to fork.ofι (fork.ι s) _.
Instances For
def
CategoryTheory.Limits.ofιCongr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{P : C}
{ι : P ⟶ X}
{ι' : P ⟶ X}
{w : CategoryTheory.CategoryStruct.comp ι f = 0}
(h : ι = ι')
:
If ι = ι', then fork.ofι ι _ and fork.ofι ι' _ are isomorphic.
Instances For
def
CategoryTheory.Limits.compNatIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{D : Type u'}
[CategoryTheory.Category.{v, u'} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence 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.
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{s : CategoryTheory.Limits.KernelFork f}
(hs : CategoryTheory.Limits.IsLimit s)
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
:
{ l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.isLimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(t : CategoryTheory.Limits.KernelFork f)
(lift : (s : CategoryTheory.Limits.KernelFork f) → s.pt ⟶ t.pt)
(fac : ∀ (s : CategoryTheory.Limits.KernelFork f),
CategoryTheory.CategoryStruct.comp (lift s) (CategoryTheory.Limits.Fork.ι t) = CategoryTheory.Limits.Fork.ι s)
(uniq : ∀ (s : CategoryTheory.Limits.KernelFork f) (m : s.pt ⟶ t.pt),
CategoryTheory.CategoryStruct.comp m (CategoryTheory.Limits.Fork.ι t) = CategoryTheory.Limits.Fork.ι s → m = lift s)
:
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
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{W : C}
(g : W ⟶ X)
(eq : CategoryTheory.CategoryStruct.comp g f = 0)
(lift : {W' : C} → (g' : W' ⟶ X) → CategoryTheory.CategoryStruct.comp g' f = 0 → (W' ⟶ W))
(fac : ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0),
CategoryTheory.CategoryStruct.comp (lift W' g' eq') g = g')
(uniq : ∀ {W' : C} (g' : W' ⟶ X) (eq' : CategoryTheory.CategoryStruct.comp g' f = 0) (m : W' ⟶ W),
CategoryTheory.CategoryStruct.comp m g = g' → m = lift W' g' eq')
:
This is a more convenient formulation to show that a KernelFork constructed using
KernelFork.ofι is a limit cone.
Instances For
def
CategoryTheory.Limits.isKernelCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
{Z : C}
(g : Y ⟶ Z)
[hg : CategoryTheory.Mono g]
{h : X ⟶ Z}
(hh : h = CategoryTheory.CategoryStruct.comp f g)
:
Every kernel of f induces a kernel of f ≫ g if g is mono.
Instances For
theorem
CategoryTheory.Limits.isKernelCompMono_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.KernelFork f}
(i : CategoryTheory.Limits.IsLimit c)
{Z : C}
(g : Y ⟶ Z)
[hg : CategoryTheory.Mono g]
{h : X ⟶ Z}
(hh : h = CategoryTheory.CategoryStruct.comp f g)
(s : CategoryTheory.Limits.KernelFork h)
:
CategoryTheory.Limits.IsLimit.lift (CategoryTheory.Limits.isKernelCompMono i g hh) s = CategoryTheory.Limits.IsLimit.lift i
(CategoryTheory.Limits.Fork.ofι (CategoryTheory.Limits.Fork.ι s)
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι s) 0))
def
CategoryTheory.Limits.isKernelOfComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{W : C}
(g : Y ⟶ W)
(h : X ⟶ W)
{c : CategoryTheory.Limits.KernelFork h}
(i : CategoryTheory.Limits.IsLimit c)
(hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) f = 0)
(hfg : CategoryTheory.CategoryStruct.comp f g = h)
:
Every kernel of f ≫ g is also a kernel of f, as long as c.ι ≫ f vanishes.
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : f = 0)
:
X identifies to the kernel of a zero map X ⟶ Y.
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofMonoOfIsZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(hf : CategoryTheory.Mono f)
(h : CategoryTheory.Limits.IsZero c.pt)
:
Any zero object identifies to the kernel of a given monomorphisms.
Instances For
theorem
CategoryTheory.Limits.KernelFork.IsLimit.isIso_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(hc : CategoryTheory.Limits.IsLimit c)
(hf : f = 0)
:
@[inline, reducible]
abbrev
CategoryTheory.Limits.kernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
C
The kernel of a morphism, expressed as the equalizer with the 0 morphism.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.kernel.ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
The map from kernel f into the source of f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.equalizer_as_kernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
@[simp]
theorem
CategoryTheory.Limits.kernel.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(h : Y ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernel.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
def
CategoryTheory.Limits.kernelIsKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
:
The kernel built from kernel.ι f is limiting.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.kernel.lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
:
Given any morphism k : W ⟶ X satisfying k ≫ f = 0, k factors through kernel.ι f
via kernel.lift : W ⟶ kernel f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernel.lift_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernel.lift_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
:
@[simp]
theorem
CategoryTheory.Limits.kernel.lift_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
{h : CategoryTheory.CategoryStruct.comp 0 f = 0}
:
CategoryTheory.Limits.kernel.lift f 0 h = 0
instance
CategoryTheory.Limits.kernel.lift_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
[CategoryTheory.Mono k]
:
def
CategoryTheory.Limits.kernel.lift'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{W : C}
(k : W ⟶ X)
(h : CategoryTheory.CategoryStruct.comp k f = 0)
:
{ l // CategoryTheory.CategoryStruct.comp l (CategoryTheory.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.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.kernel.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel f']
(p : X ⟶ X')
(q : Y ⟶ Y')
(w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
:
A commuting square induces a morphism of kernels.
Instances For
theorem
CategoryTheory.Limits.kernel.lift_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(f' : X' ⟶ Y')
(g' : Y' ⟶ Z')
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(p : X ⟶ X')
(q : Y ⟶ Y')
(r : Z ⟶ Z')
(h₁ : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g')
:
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'
@[simp]
theorem
CategoryTheory.Limits.kernel.mapIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
(CategoryTheory.Limits.kernel.mapIso f f' p q w).hom = CategoryTheory.Limits.kernel.map f f' p.hom q.hom w
@[simp]
theorem
CategoryTheory.Limits.kernel.mapIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
(CategoryTheory.Limits.kernel.mapIso f f' p q w).inv = CategoryTheory.Limits.kernel.map f' f p.inv q.inv
(_ : CategoryTheory.CategoryStruct.comp f' q.inv = CategoryTheory.CategoryStruct.comp p.inv f)
def
CategoryTheory.Limits.kernel.mapIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
A commuting square of isomorphisms induces an isomorphism of kernels.
Instances For
instance
CategoryTheory.Limits.kernel.ι_zero_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
Every kernel of the zero morphism is an isomorphism
theorem
CategoryTheory.Limits.eq_zero_of_epi_kernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Epi (CategoryTheory.Limits.kernel.ι f)]
:
f = 0
def
CategoryTheory.Limits.kernelZeroIsoSource
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
The kernel of a zero morphism is isomorphic to the source.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelZeroIsoSource_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
CategoryTheory.Limits.kernelZeroIsoSource.hom = CategoryTheory.Limits.kernel.ι 0
@[simp]
theorem
CategoryTheory.Limits.kernelZeroIsoSource_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
CategoryTheory.Limits.kernelZeroIsoSource.inv = CategoryTheory.Limits.kernel.lift 0 (CategoryTheory.CategoryStruct.id X)
(_ : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) 0 = 0)
def
CategoryTheory.Limits.kernelIsoOfEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
:
If two morphisms are known to be equal, then their kernels are isomorphic.
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_refl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{h : f = f}
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_hom_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
{Z : C}
(h : X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
:
@[simp]
theorem
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
(e : Z ⟶ X)
(he : CategoryTheory.CategoryStruct.comp e f = 0)
{Z : C}
(h : CategoryTheory.Limits.kernel g ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
(e : Z ⟶ X)
(he : CategoryTheory.CategoryStruct.comp e f = 0)
:
@[simp]
theorem
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
(e : Z ⟶ X)
(he : CategoryTheory.CategoryStruct.comp e g = 0)
{Z : C}
(h : CategoryTheory.Limits.kernel f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.lift_comp_kernelIsoOfEq_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
(h : f = g)
(e : Z ⟶ X)
(he : CategoryTheory.CategoryStruct.comp e g = 0)
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsoOfEq_trans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{h : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasKernel h]
(w₁ : f = g)
(w₂ : g = h)
:
theorem
CategoryTheory.Limits.kernel_not_epi_of_nonzero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
(w : f ≠ 0)
:
theorem
CategoryTheory.Limits.kernel_not_iso_of_nonzero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
(w : f ≠ 0)
:
instance
CategoryTheory.Limits.hasKernel_comp_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
(g : Y ⟶ Z)
[CategoryTheory.Mono g]
:
@[simp]
theorem
CategoryTheory.Limits.kernelCompMono_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Mono g]
:
@[simp]
theorem
CategoryTheory.Limits.kernelCompMono_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Mono g]
:
def
CategoryTheory.Limits.kernelCompMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Mono g]
:
When g is a monomorphism, the kernel of f ≫ g is isomorphic to the kernel of f.
Instances For
instance
CategoryTheory.Limits.hasKernel_iso_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasKernel g]
:
@[simp]
theorem
CategoryTheory.Limits.kernelIsIsoComp_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasKernel g]
:
(CategoryTheory.Limits.kernelIsIsoComp f g).hom = CategoryTheory.Limits.kernel.lift g
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)) f)
(_ :
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g))
f)
g = 0)
@[simp]
theorem
CategoryTheory.Limits.kernelIsIsoComp_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasKernel g]
:
(CategoryTheory.Limits.kernelIsIsoComp f g).inv = CategoryTheory.Limits.kernel.lift (CategoryTheory.CategoryStruct.comp f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.inv f))
(_ :
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.inv f))
(CategoryTheory.CategoryStruct.comp f g) = 0)
def
CategoryTheory.Limits.kernelIsIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.IsIso f]
[CategoryTheory.Limits.HasKernel g]
:
When f is an isomorphism, the kernel of f ≫ g is isomorphic to the kernel of g.
Instances For
def
CategoryTheory.Limits.kernel.zeroKernelFork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
:
The morphism from the zero object determines a cone on a kernel diagram
Instances For
def
CategoryTheory.Limits.kernel.isLimitConeZeroCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Mono f]
:
The map from the zero object is a kernel of a monomorphism
Instances For
def
CategoryTheory.Limits.kernel.ofMono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Mono f]
:
The kernel of a monomorphism is isomorphic to the zero object
Instances For
theorem
CategoryTheory.Limits.kernel.ι_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Mono f]
:
The kernel morphism of a monomorphism is a zero morphism
def
CategoryTheory.Limits.zeroKernelOfCancelZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : ∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0)
:
If g ≫ f = 0 implies g = 0 for all g, then 0 : 0 ⟶ X is a kernel of f.
Instances For
def
CategoryTheory.Limits.IsKernel.ofCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(l : X ⟶ Z)
(i : Z ≅ Y)
(h : CategoryTheory.CategoryStruct.comp l i.hom = f)
{s : CategoryTheory.Limits.KernelFork f}
(hs : CategoryTheory.Limits.IsLimit s)
:
If i is an isomorphism such that l ≫ i.hom = f, then any kernel of f is a kernel of l.
Instances For
def
CategoryTheory.Limits.kernel.ofCompIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(l : X ⟶ Z)
(i : Z ≅ Y)
(h : CategoryTheory.CategoryStruct.comp 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.
Instances For
def
CategoryTheory.Limits.IsKernel.isoKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Z ⟶ X)
{s : CategoryTheory.Limits.KernelFork f}
(hs : CategoryTheory.Limits.IsLimit s)
(i : Z ≅ s.pt)
(h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.kernel.isoKernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
{Z : C}
(l : Z ⟶ X)
(i : Z ≅ CategoryTheory.Limits.kernel f)
(h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.kernel.ι f) = l)
:
If i is an isomorphism such that i.hom ≫ kernel.ι f = l, then l is a kernel of f.
Instances For
theorem
CategoryTheory.Limits.kernel.ι_of_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : C)
(Y : C)
:
The kernel morphism of a zero morphism is an isomorphism
@[inline, reducible]
abbrev
CategoryTheory.Limits.CokernelCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
:
Type (max u v)
A cokernel cofork is just a cofork where the second morphism is a zero morphism.
Instances For
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.CokernelCofork f)
{Z : C}
(h : ((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj s.pt).obj
CategoryTheory.Limits.WalkingParallelPair.one ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.CokernelCofork f)
:
theorem
CategoryTheory.Limits.CokernelCofork.π_eq_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.CokernelCofork f)
:
@[inline, reducible]
abbrev
CategoryTheory.Limits.CokernelCofork.ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Z : C}
(π : Y ⟶ Z)
(w : CategoryTheory.CategoryStruct.comp f π = 0)
:
A morphism π satisfying f ≫ π = 0 determines a cokernel cofork on f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.π_ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{P : C}
(f : X ⟶ Y)
(π : Y ⟶ P)
(w : CategoryTheory.CategoryStruct.comp f π = 0)
:
def
CategoryTheory.Limits.isoOfπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(s : CategoryTheory.Limits.Cofork f 0)
:
Every cokernel cofork s is isomorphic (actually, equal) to cofork.ofπ (cofork.π s) _.
Instances For
def
CategoryTheory.Limits.ofπCongr
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{P : C}
{π : Y ⟶ P}
{π' : Y ⟶ P}
{w : CategoryTheory.CategoryStruct.comp f π = 0}
(h : π = π')
:
If π = π', then CokernelCofork.of_π π _ and CokernelCofork.of_π π' _ are isomorphic.
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{s : CategoryTheory.Limits.CokernelCofork f}
(hs : CategoryTheory.Limits.IsColimit s)
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
:
{ l // CategoryTheory.CategoryStruct.comp (CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.isColimitAux
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(t : CategoryTheory.Limits.CokernelCofork f)
(desc : (s : CategoryTheory.Limits.CokernelCofork f) → t.pt ⟶ s.pt)
(fac : ∀ (s : CategoryTheory.Limits.CokernelCofork f),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) (desc s) = CategoryTheory.Limits.Cofork.π s)
(uniq : ∀ (s : CategoryTheory.Limits.CokernelCofork f) (m : t.pt ⟶ s.pt),
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π t) m = CategoryTheory.Limits.Cofork.π s →
m = desc s)
:
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
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{Z : C}
(g : Y ⟶ Z)
(eq : CategoryTheory.CategoryStruct.comp f g = 0)
(desc : {Z' : C} → (g' : Y ⟶ Z') → CategoryTheory.CategoryStruct.comp f g' = 0 → (Z ⟶ Z'))
(fac : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0),
CategoryTheory.CategoryStruct.comp g (desc Z' g' eq') = g')
(uniq : ∀ {Z' : C} (g' : Y ⟶ Z') (eq' : CategoryTheory.CategoryStruct.comp f g' = 0) (m : Z ⟶ Z'),
CategoryTheory.CategoryStruct.comp g m = g' → m = desc Z' g' eq')
:
This is a more convenient formulation to show that a CokernelCofork constructed using
CokernelCofork.ofπ is a limit cone.
Instances For
def
CategoryTheory.Limits.isCokernelEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
{W : C}
(g : W ⟶ X)
[hg : CategoryTheory.Epi g]
{h : W ⟶ Y}
(hh : h = CategoryTheory.CategoryStruct.comp g f)
:
Every cokernel of f induces a cokernel of g ≫ f if g is epi.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isCokernelEpiComp_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{c : CategoryTheory.Limits.CokernelCofork f}
(i : CategoryTheory.Limits.IsColimit c)
{W : C}
(g : W ⟶ X)
[hg : CategoryTheory.Epi g]
{h : W ⟶ Y}
(hh : h = CategoryTheory.CategoryStruct.comp g f)
(s : CategoryTheory.Limits.CokernelCofork h)
:
CategoryTheory.Limits.IsColimit.desc (CategoryTheory.Limits.isCokernelEpiComp i g hh) s = CategoryTheory.Limits.IsColimit.desc i
(CategoryTheory.Limits.Cofork.ofπ (CategoryTheory.Limits.Cofork.π s)
(_ :
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π s) = CategoryTheory.CategoryStruct.comp 0 (CategoryTheory.Limits.Cofork.π s)))
def
CategoryTheory.Limits.isCokernelOfComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{W : C}
(g : W ⟶ X)
(h : W ⟶ Y)
{c : CategoryTheory.Limits.CokernelCofork h}
(i : CategoryTheory.Limits.IsColimit c)
(hf : CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Cofork.π c) = 0)
(hfg : CategoryTheory.CategoryStruct.comp g f = h)
:
Every cokernel of g ≫ f is also a cokernel of f, as long as f ≫ c.π vanishes.
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofId
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : f = 0)
:
Y identifies to the cokernel of a zero map X ⟶ Y.
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofEpiOfIsZero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(hf : CategoryTheory.Epi f)
(h : CategoryTheory.Limits.IsZero c.pt)
:
Any zero object identifies to the cokernel of a given epimorphisms.
Instances For
theorem
CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(hc : CategoryTheory.Limits.IsColimit c)
(hf : f = 0)
:
@[inline, reducible]
abbrev
CategoryTheory.Limits.cokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
C
The cokernel of a morphism, expressed as the coequalizer with the 0 morphism.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.cokernel.π
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
The map from the target of f to cokernel f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.coequalizer_as_cokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
@[simp]
theorem
CategoryTheory.Limits.cokernel.condition_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{Z : C}
(h : CategoryTheory.Limits.cokernel f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cokernel.condition
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
def
CategoryTheory.Limits.cokernelIsCokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
:
The cokernel built from cokernel.π f is colimiting.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.cokernel.desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
:
Given any morphism k : Y ⟶ W such that f ≫ k = 0, k factors through cokernel.π f
via cokernel.desc : cokernel f ⟶ W.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cokernel.π_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
{Z : C}
(h : W ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cokernel.π_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
:
@[simp]
theorem
CategoryTheory.Limits.colimit_ι_zero_cokernel_desc_assoc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel f]
{Z : C}
(h : Z ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.colimit_ι_zero_cokernel_desc
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
(h : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel f]
:
@[simp]
theorem
CategoryTheory.Limits.cokernel.desc_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
{h : CategoryTheory.CategoryStruct.comp f 0 = 0}
:
CategoryTheory.Limits.cokernel.desc f 0 h = 0
instance
CategoryTheory.Limits.cokernel.desc_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
[CategoryTheory.Epi k]
:
def
CategoryTheory.Limits.cokernel.desc'
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(k : Y ⟶ W)
(h : CategoryTheory.CategoryStruct.comp f k = 0)
:
{ l // CategoryTheory.CategoryStruct.comp (CategoryTheory.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.
Instances For
@[inline, reducible]
abbrev
CategoryTheory.Limits.cokernel.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel f']
(p : X ⟶ X')
(q : Y ⟶ Y')
(w : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
:
A commuting square induces a morphism of cokernels.
Instances For
theorem
CategoryTheory.Limits.cokernel.map_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{X' : C}
{Y' : C}
{Z' : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
(g : Y ⟶ Z)
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel f']
(g' : Y' ⟶ Z')
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(p : X ⟶ X')
(q : Y ⟶ Y')
(r : Z ⟶ Z')
(h₁ : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f')
(h₂ : CategoryTheory.CategoryStruct.comp g r = CategoryTheory.CategoryStruct.comp q g')
:
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'
@[simp]
theorem
CategoryTheory.Limits.cokernel.mapIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
(CategoryTheory.Limits.cokernel.mapIso f f' p q w).hom = CategoryTheory.Limits.cokernel.map f f' p.hom q.hom w
@[simp]
theorem
CategoryTheory.Limits.cokernel.mapIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
(CategoryTheory.Limits.cokernel.mapIso f f' p q w).inv = CategoryTheory.Limits.cokernel.map f' f p.inv q.inv
(_ : CategoryTheory.CategoryStruct.comp f' q.inv = CategoryTheory.CategoryStruct.comp p.inv f)
def
CategoryTheory.Limits.cokernel.mapIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{X' : C}
{Y' : C}
(f' : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel f']
(p : X ≅ X')
(q : Y ≅ Y')
(w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f')
:
A commuting square of isomorphisms induces an isomorphism of cokernels.
Instances For
instance
CategoryTheory.Limits.cokernel.π_zero_isIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
The cokernel of the zero morphism is an isomorphism
theorem
CategoryTheory.Limits.eq_zero_of_mono_cokernel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Mono (CategoryTheory.Limits.cokernel.π f)]
:
f = 0
def
CategoryTheory.Limits.cokernelZeroIsoTarget
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
The cokernel of a zero morphism is isomorphic to the target.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cokernelZeroIsoTarget_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
CategoryTheory.Limits.cokernelZeroIsoTarget.hom = CategoryTheory.Limits.cokernel.desc 0 (CategoryTheory.CategoryStruct.id Y)
(_ : CategoryTheory.CategoryStruct.comp 0 (CategoryTheory.CategoryStruct.id Y) = 0)
@[simp]
theorem
CategoryTheory.Limits.cokernelZeroIsoTarget_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
:
CategoryTheory.Limits.cokernelZeroIsoTarget.inv = CategoryTheory.Limits.cokernel.π 0
def
CategoryTheory.Limits.cokernelIsoOfEq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
:
If two morphisms are known to be equal, then their cokernels are isomorphic.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_refl
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{h : f = f}
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
{Z : C}
(h : CategoryTheory.Limits.cokernel g ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
{Z : C}
(h : CategoryTheory.Limits.cokernel f ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelIsoOfEq_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
(e : Y ⟶ Z)
(he : CategoryTheory.CategoryStruct.comp g e = 0)
{Z : C}
(h : Z ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_hom_comp_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
(e : Y ⟶ Z)
(he : CategoryTheory.CategoryStruct.comp g e = 0)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
(e : Y ⟶ Z)
(he : CategoryTheory.CategoryStruct.comp f e = 0)
{Z : C}
(h : Z ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_inv_comp_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
(h : f = g)
(e : Y ⟶ Z)
(he : CategoryTheory.CategoryStruct.comp f e = 0)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelIsoOfEq_trans
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
{h : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel g]
[CategoryTheory.Limits.HasCokernel h]
(w₁ : f = g)
(w₂ : g = h)
:
theorem
CategoryTheory.Limits.cokernel_not_mono_of_nonzero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
(w : f ≠ 0)
:
theorem
CategoryTheory.Limits.cokernel_not_iso_of_nonzero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasCokernel f]
(w : f ≠ 0)
:
instance
CategoryTheory.Limits.hasCokernel_comp_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.IsIso g]
:
@[simp]
theorem
CategoryTheory.Limits.cokernelCompIsIso_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.cokernelCompIsIso f g).inv = CategoryTheory.Limits.cokernel.desc f
(CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g)))
(_ :
CategoryTheory.CategoryStruct.comp f
(CategoryTheory.CategoryStruct.comp g
(CategoryTheory.Limits.cokernel.π (CategoryTheory.CategoryStruct.comp f g))) = 0)
@[simp]
theorem
CategoryTheory.Limits.cokernelCompIsIso_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.IsIso g]
:
(CategoryTheory.Limits.cokernelCompIsIso f g).hom = CategoryTheory.Limits.cokernel.desc (CategoryTheory.CategoryStruct.comp f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) (CategoryTheory.Limits.cokernel.π f))
(_ :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) (CategoryTheory.Limits.cokernel.π f)) = 0)
def
CategoryTheory.Limits.cokernelCompIsIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.IsIso g]
:
When g is an isomorphism, the cokernel of f ≫ g is isomorphic to the cokernel of f.
Instances For
instance
CategoryTheory.Limits.hasCokernel_epi_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{W : C}
(g : W ⟶ X)
[CategoryTheory.Epi g]
:
@[simp]
theorem
CategoryTheory.Limits.cokernelEpiComp_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi f]
[CategoryTheory.Limits.HasCokernel g]
:
@[simp]
theorem
CategoryTheory.Limits.cokernelEpiComp_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi f]
[CategoryTheory.Limits.HasCokernel g]
:
def
CategoryTheory.Limits.cokernelEpiComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{Z : C}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[CategoryTheory.Epi f]
[CategoryTheory.Limits.HasCokernel g]
:
When f is an epimorphism, the cokernel of f ≫ g is isomorphic to the cokernel of g.
Instances For
def
CategoryTheory.Limits.cokernel.zeroCokernelCofork
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
:
The morphism to the zero object determines a cocone on a cokernel diagram
Instances For
def
CategoryTheory.Limits.cokernel.isColimitCoconeZeroCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Epi f]
:
The morphism to the zero object is a cokernel of an epimorphism
Instances For
def
CategoryTheory.Limits.cokernel.ofEpi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Epi f]
:
The cokernel of an epimorphism is isomorphic to the zero object
Instances For
theorem
CategoryTheory.Limits.cokernel.π_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Epi f]
:
The cokernel morphism of an epimorphism is a zero morphism
@[simp]
theorem
CategoryTheory.Limits.MonoFactorisation.kernel_ι_comp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
{f : X ⟶ Y}
[CategoryTheory.Limits.HasKernel f]
(F : CategoryTheory.Limits.MonoFactorisation f)
:
@[simp]
theorem
CategoryTheory.Limits.cokernelImageι_inv
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)]
:
@[simp]
theorem
CategoryTheory.Limits.cokernelImageι_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)]
:
def
CategoryTheory.Limits.cokernelImageι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage 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.)
Instances For
theorem
CategoryTheory.Limits.cokernel.π_of_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
(X : C)
(Y : C)
:
The cokernel of a zero morphism is an isomorphism
instance
CategoryTheory.Limits.kernel.of_cokernel_of_epi
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.π f)]
[CategoryTheory.Epi f]
:
The kernel of the cokernel of an epimorphism is an isomorphism
instance
CategoryTheory.Limits.cokernel.of_kernel_of_mono
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasZeroObject C]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
[CategoryTheory.Mono f]
:
The cokernel of the kernel of a monomorphism is an isomorphism
def
CategoryTheory.Limits.zeroCokernelOfZeroCancel
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
[CategoryTheory.Limits.HasZeroObject C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(hf : ∀ (Z : C) (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = 0 → g = 0)
:
If f ≫ g = 0 implies g = 0 for all g, then 0 : Y ⟶ 0 is a cokernel of f.
Instances For
def
CategoryTheory.Limits.IsCokernel.ofIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Z ⟶ Y)
(i : X ≅ Z)
(h : CategoryTheory.CategoryStruct.comp i.hom l = f)
{s : CategoryTheory.Limits.CokernelCofork f}
(hs : CategoryTheory.Limits.IsColimit s)
:
If i is an isomorphism such that i.hom ≫ l = f, then any cokernel of f is a cokernel of
l.
Instances For
def
CategoryTheory.Limits.cokernel.ofIsoComp
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{Z : C}
(l : Z ⟶ Y)
(i : X ≅ Z)
(h : CategoryTheory.CategoryStruct.comp 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.
Instances For
def
CategoryTheory.Limits.IsCokernel.cokernelIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{Z : C}
(l : Y ⟶ Z)
{s : CategoryTheory.Limits.CokernelCofork f}
(hs : CategoryTheory.Limits.IsColimit s)
(i : s.pt ≅ Z)
(h : CategoryTheory.CategoryStruct.comp (CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.cokernel.cokernelIso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
{Z : C}
(l : Y ⟶ Z)
(i : CategoryTheory.Limits.cokernel f ≅ Z)
(h : CategoryTheory.CategoryStruct.comp (CategoryTheory.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.
Instances For
def
CategoryTheory.Limits.kernelComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
:
G.obj (CategoryTheory.Limits.kernel f) ⟶ CategoryTheory.Limits.kernel (G.map f)
The comparison morphism for the kernel of f.
This is an isomorphism iff G preserves the kernel of f; see
CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
Instances For
@[simp]
theorem
CategoryTheory.Limits.kernelComparison_comp_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
{Z : D}
(h : G.obj X ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.kernelComparison_comp_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
:
@[simp]
theorem
CategoryTheory.Limits.map_lift_kernelComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
{Z : C}
{h : Z ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h f = 0)
{Z : D}
(h : CategoryTheory.Limits.kernel (G.map f) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.lift f h w))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.kernel.lift (G.map f) (G.map h)
(_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = 0))
h
@[simp]
theorem
CategoryTheory.Limits.map_lift_kernelComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
{Z : C}
{h : Z ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.lift f h w))
(CategoryTheory.Limits.kernelComparison f G) = CategoryTheory.Limits.kernel.lift (G.map f) (G.map h) (_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = 0)
theorem
CategoryTheory.Limits.kernelComparison_comp_kernel_map_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{X' : C}
{Y' : C}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasKernel (G.map g)]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
{Z : D}
(h : CategoryTheory.Limits.kernel (G.map g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q)
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map q) = CategoryTheory.CategoryStruct.comp (G.map p) (G.map g)))
h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison g G) h)
theorem
CategoryTheory.Limits.kernelComparison_comp_kernel_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{X' : C}
{Y' : C}
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasKernel (G.map g)]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelComparison f G)
(CategoryTheory.Limits.kernel.map (G.map f) (G.map g) (G.map p) (G.map q)
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map q) = CategoryTheory.CategoryStruct.comp (G.map p) (G.map g))) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
(CategoryTheory.Limits.kernelComparison g G)
def
CategoryTheory.Limits.cokernelComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
:
CategoryTheory.Limits.cokernel (G.map f) ⟶ G.obj (CategoryTheory.Limits.cokernel f)
The comparison morphism for the cokernel of f.
Instances For
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
{Z : D}
(h : G.obj (CategoryTheory.Limits.cokernel f) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_cokernelComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
:
@[simp]
theorem
CategoryTheory.Limits.cokernelComparison_map_desc_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
{Z : C}
{h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f h = 0)
{Z : D}
(h : G.obj Z ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.desc f h w)) h) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.desc (G.map f) (G.map h)
(_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = 0))
h
@[simp]
theorem
CategoryTheory.Limits.cokernelComparison_map_desc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
{Z : C}
{h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f h = 0)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
(G.map (CategoryTheory.Limits.cokernel.desc f h w)) = CategoryTheory.Limits.cokernel.desc (G.map f) (G.map h)
(_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = 0)
theorem
CategoryTheory.Limits.cokernel_map_comp_cokernelComparison_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{X' : C}
{Y' : C}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel g]
[CategoryTheory.Limits.HasCokernel (G.map g)]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
{Z : D}
(h : G.obj (CategoryTheory.Limits.cokernel g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q)
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map q) = CategoryTheory.CategoryStruct.comp (G.map p) (G.map g)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison g G) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq)) h)
theorem
CategoryTheory.Limits.cokernel_map_comp_cokernelComparison
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X : C}
{Y : C}
(f : X ⟶ Y)
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{X' : C}
{Y' : C}
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel g]
[CategoryTheory.Limits.HasCokernel (G.map g)]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q)
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map q) = CategoryTheory.CategoryStruct.comp (G.map p) (G.map g)))
(CategoryTheory.Limits.cokernelComparison g G) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
(G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
class
CategoryTheory.Limits.HasKernels
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
- has_limit : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasKernel f
HasKernels represents the existence of kernels for every morphism.
Instances
class
CategoryTheory.Limits.HasCokernels
(C : Type u)
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
:
- has_colimit : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.HasCokernel f
HasCokernels represents the existence of cokernels for every morphism.