mathlib documentation


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:

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.

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