# Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

# 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₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) {Z : D} (h : G.obj Y Z) :
@[simp]
theorem CategoryTheory.Limits.KernelFork.map_condition {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :
CategoryTheory.CategoryStruct.comp (G.map ()) (G.map f) = 0
def CategoryTheory.Limits.KernelFork.map {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :

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₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :
def CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (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₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (hc : ) (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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {h : Z X} (w : ) :

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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {h : Z X} (w : ) :

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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) :

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
def CategoryTheory.Limits.PreservesKernel.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasKernel (G.map f)] :

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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasKernel (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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasKernel (G.map f)] :
theorem CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasKernel (G.map f)] {X' : C} {Y' : C} (g : X' Y') [CategoryTheory.Limits.HasKernel (G.map g)] (p : X X') (q : Y Y') {Z : D} (h : G.obj () Z) :
theorem CategoryTheory.Limits.kernel_map_comp_preserves_kernel_iso_inv {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasKernel (G.map f)] {X' : C} {Y' : C} (g : X' Y') [CategoryTheory.Limits.HasKernel (G.map g)] (p : X X') (q : Y Y') :
@[simp]
theorem CategoryTheory.Limits.CokernelCofork.map_condition_assoc {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) {Z : D} (h : G.obj () Z) :
@[simp]
theorem CategoryTheory.Limits.CokernelCofork.map_condition {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :
CategoryTheory.CategoryStruct.comp (G.map f) (G.map ()) = 0
def CategoryTheory.Limits.CokernelCofork.map {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :

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₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (G : ) :
def CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (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₁} [] {D : Type u₂} [] {X : C} {Y : C} {f : X Y} (hc : ) (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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {h : Y Z} (w : ) :

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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} {Z : C} {f : X Y} {h : Y Z} (w : ) :

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

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
def CategoryTheory.Limits.PreservesCokernel.ofIsoComparison {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasCokernel (G.map f)] :

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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasCokernel (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₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasCokernel (G.map f)] :
theorem CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map_assoc {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasCokernel (G.map f)] {X' : C} {Y' : C} (g : X' Y') [CategoryTheory.Limits.HasCokernel (G.map g)] (p : X X') (q : Y Y') {Z : D} (h : CategoryTheory.Limits.cokernel (G.map g) Z) :
theorem CategoryTheory.Limits.preserves_cokernel_iso_comp_cokernel_map {C : Type u₁} [] {D : Type u₂} [] (G : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.Limits.HasCokernel (G.map f)] {X' : C} {Y' : C} (g : X' Y') [CategoryTheory.Limits.HasCokernel (G.map g)] (p : X X') (q : Y Y') :
noncomputable instance CategoryTheory.Limits.preservesKernelZero {C : Type u₁} [] {D : Type u₂} [] (X : C) (Y : C) (G : ) :
noncomputable instance CategoryTheory.Limits.preservesCokernelZero {C : Type u₁} [] {D : Type u₂} [] (X : C) (Y : C) (G : ) :
noncomputable def CategoryTheory.Limits.preservesKernelZero' {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (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₁} [] {D : Type u₂} [] {X : C} {Y : C} (G : ) (f : X Y) (hf : f = 0) :

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

Instances For