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}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C) :
f ≫ g = 0 → (category_theory.limits.image f ⟶ category_theory.limits.kernel g)
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}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_kernels V]
{A B C : V}
(g : B ⟶ C)
[category_theory.limits.has_zero_object V]
{w : 0 ≫ g = 0} :
category_theory.image_to_kernel_map 0 g w = 0
theorem
category_theory.image_to_kernel_map_zero_right
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
{w : f ≫ 0 = 0} :
theorem
category_theory.image_to_kernel_map_epi_of_zero_of_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_kernels V]
{A B C : V}
(g : B ⟶ C)
[category_theory.mono g]
[category_theory.limits.has_zero_object V]
{w : 0 ≫ g = 0} :
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}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_images V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
[category_theory.epi f]
{w : f ≫ 0 = 0} :
image_to_kernel_map for A --f--> B --0--> C, where [epi g] is an epi
(i.e. the sequence is exact at B).