# mathlibdocumentation

algebra.homology.image_to_kernel_map

# The morphism from image f to kernel g when f ≫ g = 0#

We define the map, as the lift of image.ι f to kernel g, and check some basic properties:

• this map is a monomorphism
• given A --0--> B --g--> C, where [mono g], this map is an epimorphism
• given A --f--> B --0--> C, where [epi f], this map is an epimorphism

In later files, we define the homology of complex as the cokernel of this map, and say a complex is exact at a point if this map is an epimorphism.

At this point we assume that we have all images, and all equalizers. We need to assume all equalizers, not just kernels, so that factor_thru_image is an epimorphism.

def category_theory.image_to_kernel_map {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :

The morphism from image f to kernel g when f ≫ g = 0.

@[simp]
theorem category_theory.image_to_kernel_map_zero_left {V : Type u} {A B C : V} (g : B C) {w : 0 g = 0} :
theorem category_theory.image_to_kernel_map_zero_right {V : Type u} {A B C : V} (f : A B) {w : f 0 = 0} :
theorem category_theory.image_to_kernel_map_comp_right {V : Type u} {A B C : V} (f : A B) (g : B C) {D : V} (h : C D) (w : f g = 0) :
theorem category_theory.image_to_kernel_map_comp_left {V : Type u} {A B C : V} (f : A B) (g : B C) {Z : V} (h : Z A) (w : f g = 0) :
@[simp]
theorem category_theory.image_to_kernel_map_comp_iso {V : Type u} {A B C : V} (f : A B) (g : B C) {D : V} (h : C D) (w : f g h = 0) :
@[simp]
theorem category_theory.image_to_kernel_map_iso_comp {V : Type u} {A B C : V} (f : A B) (g : B C) {Z : V} (h : Z A) (w : (h f) g = 0) :
@[simp]
theorem category_theory.image_to_kernel_map_comp_hom_inv_comp {V : Type u} {A B C : V} (f : A B) (g : B C) {Z : V} {i : B Z} (w : (f i.hom) i.inv g = 0) :
(i.inv g) w =

image_to_kernel_map for A --0--> B --g--> C, where [mono g] is an epi (i.e. the sequence is exact at B).

theorem category_theory.image_to_kernel_map_epi_of_epi_of_zero {V : Type u} {A B C : V} (f : A B)  :

image_to_kernel_map for A --f--> B --0--> C, where [epi g] is an epi (i.e. the sequence is exact at B).