# mathlibdocumentation

algebra.homology.image_to_kernel

# Image-to-kernel comparison maps #

Whenever f : A ⟶ B and g : B ⟶ C satisfy w : f ≫ g = 0, we have image_le_kernel f g w : image_subobject f ≤ kernel_subobject g (assuming the appropriate images and kernels exist).

image_to_kernel f g w is the corresponding morphism between objects in C.

We define homology f g w of such a pair as the cokernel of image_to_kernel f g w.

theorem image_le_kernel {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
@[instance]
def image_to_kernel.mono {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
def image_to_kernel {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :

The canonical morphism image_subobject f ⟶ kernel_subobject g when f ≫ g = 0.

Equations
@[simp]
theorem subobject_of_le_as_image_to_kernel {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0)  :

Prefer image_to_kernel.

@[simp]
theorem image_to_kernel_arrow_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) {X' : V} (f' : B X') :
@[simp]
theorem image_to_kernel_arrow {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
theorem factor_thru_image_subobject_comp_image_to_kernel {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
@[simp]
theorem image_to_kernel_zero_left {V : Type u} {A B C : V} (g : B C) {w : 0 g = 0} :
w = 0
theorem image_to_kernel_zero_right {V : Type u} {A B C : V} (f : A B) {w : f 0 = 0} :
theorem image_to_kernel_comp_right {V : Type u} {A B C : V} (f : A B) (g : B C) {D : V} (h : C D) (w : f g = 0) :
(g h) _ =
theorem image_to_kernel_comp_left {V : Type u} {A B C : V} (f : A B) (g : B C) {Z : V} (h : Z A) (w : f g = 0) :
image_to_kernel (h f) g _ =
@[simp]
theorem image_to_kernel_comp_mono {V : Type u} {A B C : V} (f : A B) (g : B C) {D : V} (h : C D) (w : f g h = 0) :
(g h) w =
@[simp]
theorem image_to_kernel_epi_comp {V : Type u} {A B C : V} (f : A B) (g : B C) {Z : V} (h : Z A) (w : (h f) g = 0) :
image_to_kernel (h f) g w =
@[simp]
theorem image_to_kernel_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) :
image_to_kernel (f i.hom) (i.inv g) w =
@[instance]
def image_to_kernel_epi_of_zero_of_mono {V : Type u} {A B C : V} (g : B C)  :

image_to_kernel for A --0--> B --g--> C, where g is a mono is itself an epi (i.e. the sequence is exact at B).

@[instance]
def image_to_kernel_epi_of_epi_of_zero {V : Type u} {A B C : V} (f : A B)  :

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

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

The homology of a pair of morphisms f : A ⟶ B and g : B ⟶ C satisfying f ≫ g = 0 is the cokernel of the image_to_kernel morphism for f and g.

Equations
• g w =
def homology.π {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0)  :

The morphism from cycles to homology.

Equations
• g w =
@[simp]
theorem homology.condition {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0)  :
w g w = 0
def homology.desc {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) {D : V} (p : w k = 0) :
g w D

To construct a map out of homology, it suffices to construct a map out of the cycles which vanishes on boundaries.

Equations
• w k p =
@[simp]
theorem homology.π_desc {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) {D : V} (p : w k = 0) :
g w w k p = k
@[simp]
theorem homology.π_desc_assoc {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) {D : V} (p : w k = 0) {X' : V} (f' : D X') :
g w w k p f' = k f'
@[ext]
theorem homology.ext {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) {D : V} {k k' : g w D} (p : g w k = g w k') :
k = k'

To check two morphisms out of homology f g w are equal, it suffices to check on cycles.

@[simp]
theorem homology_zero_zero_inv {V : Type u} {A B C : V} [category_theory.limits.has_cokernel 0 homology_zero_zero._proof_3)] :
homology_zero_zero.inv = 0 homology_zero_zero._proof_15
def homology_zero_zero {V : Type u} {A B C : V} [category_theory.limits.has_cokernel 0 homology_zero_zero._proof_3)] :
0 homology_zero_zero._proof_5 B

homology 0 0 _ is just the middle object.

Equations
@[simp]
theorem homology_zero_zero_hom {V : Type u} {A B C : V} [category_theory.limits.has_cokernel 0 homology_zero_zero._proof_3)] :
homology_zero_zero.hom = homology_zero_zero._proof_12 homology_zero_zero._proof_13
theorem image_subobject_map_comp_image_to_kernel {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) (p : α.right = β.left) :

Given compatible commutative squares between a pair f g and a pair f' g' satisfying f ≫ g = 0 and f' ≫ g' = 0, the image_to_kernel morphisms intertwine the induced map on kernels and the induced map on images.

theorem image_subobject_map_comp_image_to_kernel_assoc {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) (p : α.right = β.left) {X' : V} (f'_1 : X') :
= g' w' f'_1
def homology.map {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) [category_theory.limits.has_cokernel g' w')] (p : α.right = β.left) :
g w homology f' g' w'

Given compatible commutative squares between a pair f g and a pair f' g' satisfying f ≫ g = 0 and f' ≫ g' = 0, we get a morphism on homology.

Equations
• w' α β p =
@[simp]
theorem homology.π_map_assoc {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) [category_theory.limits.has_cokernel g' w')] (p : α.right = β.left) {X' : V} (f'_1 : homology f' g' w' X') :
g w w' α β p f'_1 = g' w' f'_1
@[simp]
theorem homology.π_map {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) [category_theory.limits.has_cokernel g' w')] (p : α.right = β.left) :
g w w' α β p =
@[simp]
theorem homology.map_desc_assoc {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) [category_theory.limits.has_cokernel g' w')] (p : α.right = β.left) {D : V} (k : D) (z : g' w' k = 0) {X' : V} (f'_1 : D X') :
w' α β p g' w' k z f'_1 = _ f'_1
@[simp]
theorem homology.map_desc {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {A' B' C' : V} {f' : A' B'} {g' : B' C'} (w' : f' g' = 0) [category_theory.limits.has_cokernel g' w')] (p : α.right = β.left) {D : V} (k : D) (z : g' w' k = 0) :
w' α β p g' w' k z = _
@[simp]
theorem homology.congr_hom {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {f' : A B} {g' : B C} (w' : f' g' = 0) (pf : f = f') (pg : g = g') :
w' pf pg).hom = w' {left := , right := , w' := _} {left := , right := , w' := _} _
@[simp]
theorem homology.congr_inv {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {f' : A B} {g' : B C} (w' : f' g' = 0) (pf : f = f') (pg : g = g') :
w' pf pg).inv = w {left := , right := , w' := _} {left := , right := , w' := _} _
def homology.congr {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0) {f' : A B} {g' : B C} (w' : f' g' = 0) (pf : f = f') (pg : g = g') :
g w homology f' g' w'

homology f g w ≅ homology f' g' w' if f = f' and g = g'. (Note the objects are not changing here.)

Equations