# mathlibdocumentation

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

def category_theory.limits.is_limit_map_cone_fork_equiv' {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f : X Y} {h : Z X} (w : h 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 kernel_fork.of_ι with functor.map_cone.

This is a variant of is_limit_map_cone_fork_equiv for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

Equations
def category_theory.limits.is_limit_fork_map_of_is_limit' {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f : X Y} {h : Z X} (w : h f = 0)  :

The property of preserving kernels expressed in terms of kernel forks.

This is a variant of is_limit_fork_map_of_is_limit for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

Equations
noncomputable def category_theory.limits.is_limit_of_has_kernel_of_preserves_limit {C : Type u₁} {D : Type u₂} (G : C D) {X 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.

Equations
@[protected, instance]
def category_theory.limits.category_theory.functor.map.has_kernel {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.preserves_kernel.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :

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

Equations
noncomputable def category_theory.limits.preserves_kernel.iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.preserves_kernel.iso_hom {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :
@[protected, instance]
def category_theory.limits.kernel_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :
def category_theory.limits.is_colimit_map_cocone_cofork_equiv' {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f : X Y} {h : Y Z} (w : f 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 cokernel_cofork.of_π with functor.map_cocone.

This is a variant of is_colimit_map_cocone_cofork_equiv for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

Equations
def category_theory.limits.is_colimit_cofork_map_of_is_colimit' {C : Type u₁} {D : Type u₂} (G : C D) {X Y Z : C} {f : X Y} {h : Y Z} (w : f h = 0)  :

The property of preserving cokernels expressed in terms of cokernel coforks.

This is a variant of is_colimit_cofork_map_of_is_colimit for equalizers, which we can't use directly between G.map 0 = 0 does not hold definitionally.

Equations
noncomputable def category_theory.limits.is_colimit_of_has_cokernel_of_preserves_colimit {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :

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

Equations
@[protected, instance]
def category_theory.limits.category_theory.functor.map.has_cokernel {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :
noncomputable def category_theory.limits.preserves_cokernel.of_iso_comparison {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :

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

Equations
noncomputable def category_theory.limits.preserves_cokernel.iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :

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

Equations
@[simp]
theorem category_theory.limits.preserves_cokernel.iso_inv {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :
@[protected, instance]
def category_theory.limits.cokernel_comparison.category_theory.is_iso {C : Type u₁} {D : Type u₂} (G : C D) {X Y : C} (f : X Y)  :