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.

Equations

• CategoryTheory.Limits.KernelFork.map c G = CategoryTheory.Limits.KernelFork.ofι (G.map (CategoryTheory.Limits.Fork.ι c)) ⋯

@[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] : CategoryTheory.Limits.Fork.ι (CategoryTheory.Limits.KernelFork.map c G) = G.map (CategoryTheory.Limits.Fork.ι c)

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] : CategoryTheory.Limits.IsLimit (G.mapCone c) ≃ CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.map c G)

The underlying cone of a kernel fork is mapped to a limit cone if and only if the mapped kernel fork is limit.

Equations

• One or more equations did not get rendered due to their size.

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] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.map c G)

A limit kernel fork is mapped to a limit kernel fork by a functor G when this functor preserves the corresponding limit.

Equations

• CategoryTheory.Limits.KernelFork.mapIsLimit c hc G = (CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv c G) (CategoryTheory.Limits.isLimitOfPreserves G hc)

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) ⋯)

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.

Equations

• CategoryTheory.Limits.isLimitMapConeForkEquiv' G w = CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv (CategoryTheory.Limits.KernelFork.ofι h w) G

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) ⋯)

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.

Equations

• CategoryTheory.Limits.isLimitForkMapOfIsLimit' G w l = (CategoryTheory.Limits.isLimitMapConeForkEquiv' G w) (CategoryTheory.Limits.PreservesLimit.preserves l)

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)) ⋯)

If G preserves kernels and C has them, then the fork constructed of the mapped morphisms of a kernel fork is a limit.

Equations

• CategoryTheory.Limits.isLimitOfHasKernelOfPreservesLimit G f = CategoryTheory.Limits.isLimitForkMapOfIsLimit' G ⋯ (CategoryTheory.Limits.kernelIsKernel f)

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)

Equations

• ⋯ = ⋯

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)] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G

If the kernel comparison map for G at f is an isomorphism, then G preserves the kernel of f.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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] : (CategoryTheory.Limits.PreservesKernel.iso G f).hom = CategoryTheory.Limits.kernelComparison f 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] : CategoryTheory.IsIso (CategoryTheory.Limits.kernelComparison f G)

Equations

• ⋯ = ⋯

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 (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.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.

Equations

• CategoryTheory.Limits.CokernelCofork.map c G = CategoryTheory.Limits.CokernelCofork.ofπ (G.map (CategoryTheory.Limits.Cofork.π c)) ⋯

@[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] : CategoryTheory.Limits.Cofork.π (CategoryTheory.Limits.CokernelCofork.map c G) = G.map (CategoryTheory.Limits.Cofork.π c)

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] : CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.map c G)

The underlying cocone of a cokernel cofork is mapped to a colimit cocone if and only if the mapped cokernel cofork is colimit.

Equations

• One or more equations did not get rendered due to their size.

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] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.map c G)

A colimit cokernel cofork is mapped to a colimit cokernel cofork by a functor G when this functor preserves the corresponding colimit.

Equations

• CategoryTheory.Limits.CokernelCofork.mapIsColimit c hc G = (CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv c G) (CategoryTheory.Limits.isColimitOfPreserves G hc)

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) ⋯)

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.

Equations

• CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' G w = CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv (CategoryTheory.Limits.CokernelCofork.ofπ h w) G

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) ⋯)

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.

Equations

• CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' G w l = (CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' G w) (CategoryTheory.Limits.PreservesColimit.preserves l)

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)) ⋯)

If G preserves cokernels and C has them, then the cofork constructed of the mapped morphisms of a cokernel cofork is a colimit.

Equations

• CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit G f = CategoryTheory.Limits.isColimitCoforkMapOfIsColimit' G ⋯ (CategoryTheory.Limits.cokernelIsCokernel f)

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)

Equations

• ⋯ = ⋯

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)] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G

If the cokernel comparison map for G at f is an isomorphism, then G preserves the cokernel of f.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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] : (CategoryTheory.Limits.PreservesCokernel.iso G f).inv = CategoryTheory.Limits.cokernelComparison f 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] : CategoryTheory.IsIso (CategoryTheory.Limits.cokernelComparison f G)

Equations

• ⋯ = ⋯

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) ⋯) 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 (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] : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair 0 0) G

Equations

• One or more equations did not get rendered due to their size.

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] : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair 0 0) G

Equations

• One or more equations did not get rendered due to their size.

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) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G

The kernel of a zero map is preserved by any functor which preserves zero morphisms.

Equations

• CategoryTheory.Limits.preservesKernelZero' G f hf = Eq.mpr ⋯ inferInstance

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) : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G

The cokernel of a zero map is preserved by any functor which preserves zero morphisms.

Equations

• CategoryTheory.Limits.preservesCokernelZero' G f hf = Eq.mpr ⋯ inferInstance