Preserving (co)kernels #
Constructions to relate the notions of preserving (co)kernels and reflecting (co)kernels to concrete (co)forks.
In particular, we show that kernel_comparison f g G is an isomorphism iff G preserves
the limit of the parallel pair f,0, as well as the dual result.
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_condition_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{Z : D}
(h : G.obj Y ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Fork.ι c))
(CategoryTheory.CategoryStruct.comp (G.map f) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_condition
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Fork.ι c)) (G.map f) = 0
def
CategoryTheory.Limits.KernelFork.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
CategoryTheory.Limits.KernelFork (G.map f)
A kernel fork for f is mapped to a kernel fork for G.map f if G is a functor
which preserves zero morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Limits.KernelFork.map_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
def
CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
The underlying cone of a kernel fork is mapped to a limit cone if and only if the mapped kernel fork is limit.
Instances For
def
CategoryTheory.Limits.KernelFork.mapIsLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.KernelFork f)
(hc : CategoryTheory.Limits.IsLimit c)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
A limit kernel fork is mapped to a limit kernel fork by a functor G when this functor
preserves the corresponding limit.
Instances For
def
CategoryTheory.Limits.isLimitMapConeForkEquiv'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
{Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h f = 0)
:
CategoryTheory.Limits.IsLimit (G.mapCone (CategoryTheory.Limits.KernelFork.ofι h w)) ≃ CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι (G.map h) (_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = 0))
The map of a kernel fork is a limit iff
the kernel fork consisting of the mapped morphisms is a limit.
This essentially lets us commute KernelFork.ofι with Functor.mapCone.
This is a variant of isLimitMapConeForkEquiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Instances For
def
CategoryTheory.Limits.isLimitForkMapOfIsLimit'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
{Z : C}
{f : X ⟶ Y}
{h : Z ⟶ X}
(w : CategoryTheory.CategoryStruct.comp h f = 0)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
(l : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι h w))
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.KernelFork.ofι (G.map h) (_ : CategoryTheory.CategoryStruct.comp (G.map h) (G.map f) = 0))
The property of preserving kernels expressed in terms of kernel forks.
This is a variant of isLimitForkMapOfIsLimit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Instances For
def
CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
CategoryTheory.Limits.IsLimit
(CategoryTheory.Limits.Fork.ofι (G.map (CategoryTheory.Limits.kernel.ι f))
(_ :
CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.ι f)) (G.map f) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.ι f)) 0))
If G preserves kernels and C has them, then the fork constructed of the mapped morphisms of
a kernel fork is a limit.
Instances For
instance
CategoryTheory.Limits.instHasKernelObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
CategoryTheory.Limits.HasKernel (G.map f)
def
CategoryTheory.Limits.PreservesKernel.ofIsoComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[i : CategoryTheory.IsIso (CategoryTheory.Limits.kernelComparison f G)]
:
If the kernel comparison map for G at f is an isomorphism, then G preserves the
kernel of f.
Instances For
def
CategoryTheory.Limits.PreservesKernel.iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
G.obj (CategoryTheory.Limits.kernel f) ≅ CategoryTheory.Limits.kernel (G.map f)
If G preserves the kernel of f, then the kernel comparison map for G at f is
an isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesKernel.iso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
instance
CategoryTheory.Limits.instIsIsoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorKernelKernelMapKernelComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
:
theorem
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
{X' : C}
{Y' : C}
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasKernel (G.map g)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) 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.kernel g) ⟶ Z)
:
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)))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.map f g p q hpq)) h)
theorem
CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasKernel f]
[CategoryTheory.Limits.HasKernel (G.map f)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G]
{X' : C}
{Y' : C}
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasKernel (G.map g)]
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p 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)))
(CategoryTheory.Limits.PreservesKernel.iso G g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesKernel.iso G f).inv
(G.map (CategoryTheory.Limits.kernel.map f g p q hpq))
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_condition_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
{Z : D}
(h : G.obj
(((CategoryTheory.Functor.const CategoryTheory.Limits.WalkingParallelPair).obj c.pt).obj
CategoryTheory.Limits.WalkingParallelPair.one) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (G.map f)
(CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.Cofork.π c)) h) = CategoryTheory.CategoryStruct.comp 0 h
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_condition
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
CategoryTheory.CategoryStruct.comp (G.map f) (G.map (CategoryTheory.Limits.Cofork.π c)) = 0
def
CategoryTheory.Limits.CokernelCofork.map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
CategoryTheory.Limits.CokernelCofork (G.map f)
A cokernel cofork for f is mapped to a cokernel cofork for G.map f if G is a functor
which preserves zero morphisms.
Instances For
@[simp]
theorem
CategoryTheory.Limits.CokernelCofork.map_π
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
def
CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
The underlying cocone of a cokernel cofork is mapped to a colimit cocone if and only if the mapped cokernel cofork is colimit.
Instances For
def
CategoryTheory.Limits.CokernelCofork.mapIsColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
{f : X ⟶ Y}
(c : CategoryTheory.Limits.CokernelCofork f)
(hc : CategoryTheory.Limits.IsColimit c)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
A colimit cokernel cofork is mapped to a colimit cokernel cofork by a functor G
when this functor preserves the corresponding colimit.
Instances For
def
CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
{Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f h = 0)
:
CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ h w)) ≃ CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.CokernelCofork.ofπ (G.map h)
(_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = 0))
The map of a cokernel cofork is a colimit iff
the cokernel cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute CokernelCofork.ofπ with Functor.mapCocone.
This is a variant of isColimitMapCoconeCoforkEquiv for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Instances For
def
CategoryTheory.Limits.isColimitCoforkMapOfIsColimit'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
{Z : C}
{f : X ⟶ Y}
{h : Y ⟶ Z}
(w : CategoryTheory.CategoryStruct.comp f h = 0)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
(l : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ h w))
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.CokernelCofork.ofπ (G.map h) (_ : CategoryTheory.CategoryStruct.comp (G.map f) (G.map h) = 0))
The property of preserving cokernels expressed in terms of cokernel coforks.
This is a variant of isColimitCoforkMapOfIsColimit for equalizers,
which we can't use directly between G.map 0 = 0 does not hold definitionally.
Instances For
def
CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
CategoryTheory.Limits.IsColimit
(CategoryTheory.Limits.Cofork.ofπ (G.map (CategoryTheory.Limits.cokernel.π f))
(_ :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map (CategoryTheory.Limits.cokernel.π f)) = CategoryTheory.CategoryStruct.comp 0 (G.map (CategoryTheory.Limits.cokernel.π f))))
If G preserves cokernels and C has them, then the cofork constructed of the mapped morphisms of
a cokernel cofork is a colimit.
Instances For
instance
CategoryTheory.Limits.instHasCokernelObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
CategoryTheory.Limits.HasCokernel (G.map f)
def
CategoryTheory.Limits.PreservesCokernel.ofIsoComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[i : CategoryTheory.IsIso (CategoryTheory.Limits.cokernelComparison f G)]
:
If the cokernel comparison map for G at f is an isomorphism, then G preserves the
cokernel of f.
Instances For
def
CategoryTheory.Limits.PreservesCokernel.iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
G.obj (CategoryTheory.Limits.cokernel f) ≅ CategoryTheory.Limits.cokernel (G.map f)
If G preserves the cokernel of f, then the cokernel comparison map for G at f is
an isomorphism.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PreservesCokernel.iso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
instance
CategoryTheory.Limits.instIsIsoCokernelObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMapCokernelCokernelComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
:
theorem
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
{X' : C}
{Y' : C}
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel g]
[CategoryTheory.Limits.HasCokernel (G.map g)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
{Z : D}
(h : CategoryTheory.Limits.cokernel (G.map g) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom
(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)))
h) = CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G g).hom h)
theorem
CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{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}
(f : X ⟶ Y)
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (G.map f)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G]
{X' : C}
{Y' : C}
(g : X' ⟶ Y')
[CategoryTheory.Limits.HasCokernel g]
[CategoryTheory.Limits.HasCokernel (G.map g)]
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair g 0) G]
(p : X ⟶ X')
(q : Y ⟶ Y')
(hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesCokernel.iso G f).hom
(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 (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
(CategoryTheory.Limits.PreservesCokernel.iso G g).hom
noncomputable instance
CategoryTheory.Limits.preservesKernelZero
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(X : C)
(Y : C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
noncomputable instance
CategoryTheory.Limits.preservesCokernelZero
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
(X : C)
(Y : C)
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
:
noncomputable def
CategoryTheory.Limits.preservesKernelZero'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
(f : X ⟶ Y)
(hf : f = 0)
:
The kernel of a zero map is preserved by any functor which preserves zero morphisms.
Instances For
noncomputable def
CategoryTheory.Limits.preservesCokernelZero'
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
[CategoryTheory.Limits.HasZeroMorphisms D]
{X : C}
{Y : C}
(G : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesZeroMorphisms G]
(f : X ⟶ Y)
(hf : f = 0)
:
The cokernel of a zero map is preserved by any functor which preserves zero morphisms.