# mathlib3documentation

algebra.homology.image_to_kernel

# Image-to-kernel comparison maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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) :
@[protected, instance]
def image_to_kernel.mono {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
noncomputable 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
Instances for image_to_kernel
@[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_apply {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0)  :
( g w) x) =
@[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 =
@[protected, 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).

@[protected, 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).

noncomputable 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 =
noncomputable 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
noncomputable 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'
@[simp]
theorem homology.π_desc_apply {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 k p) ( g w) x) = k x
@[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.

The cokernel of the map Im f ⟶ Ker 0 is isomorphic to the cokernel of f.

Equations

The kernel of the map Im 0 ⟶ Ker f is isomorphic to the kernel of f.

Equations
@[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
noncomputable 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
noncomputable 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_apply {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)  :
w' α β p) ( g w) x) = (homology.π f' g' w')
@[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_apply {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 : (homology f g w)) :
g' w' k z) ( w' α β p) x) = _) x
@[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.map_id {V : Type u} {A B C : V} {f : A B} {g : B C} (w : f g = 0)  :
w rfl = 𝟙 (homology f g w)
theorem homology.comp_right_eq_comp_left {V : Type u_1} {A₁ B₁ C₁ A₂ B₂ C₂ A₃ B₃ C₃ : V} {f₁ : A₁ B₁} {g₁ : B₁ C₁} {f₂ : A₂ B₂} {g₂ : B₂ C₂} {f₃ : A₃ B₃} {g₃ : B₃ C₃} (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
(α₁ α₂).right = (β₁ β₂).left

Auxiliary lemma for homology computations.

theorem homology.map_comp_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) {A₃ B₃ C₃ : V} {f₃ : A₃ B₃} {g₃ : B₃ C₃} (w₃ : f₃ g₃ = 0) [category_theory.limits.has_cokernel g₁ w₁)] [category_theory.limits.has_cokernel g₂ w₂)] [category_theory.limits.has_cokernel g₃ w₃)] (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) {X' : V} (f' : homology f₃ g₃ w₃ X') :
w₂ α₁ β₁ p₁ w₃ α₂ β₂ p₂ f' = w₃ (α₁ α₂) (β₁ β₂) _ f'
theorem homology.map_comp {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) {A₃ B₃ C₃ : V} {f₃ : A₃ B₃} {g₃ : B₃ C₃} (w₃ : f₃ g₃ = 0) [category_theory.limits.has_cokernel g₁ w₁)] [category_theory.limits.has_cokernel g₂ w₂)] [category_theory.limits.has_cokernel g₃ w₃)] (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
w₂ α₁ β₁ p₁ w₃ α₂ β₂ p₂ = w₃ (α₁ α₂) (β₁ β₂) _
noncomputable def homology.map_iso {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₁)] [category_theory.limits.has_cokernel g₂ w₂)] (p : α.hom.right = β.hom.left) :
homology f₁ g₁ w₁ homology f₂ g₂ w₂

An isomorphism between two three-term complexes induces an isomorphism on homology.

Equations
@[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' := _} _
noncomputable 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

We provide a variant image_to_kernel' : image f ⟶ kernel g, and use this to give alternative formulas for homology f g w.

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

While image_to_kernel f g w provides a morphism image_subobject f ⟶ kernel_subobject g in terms of the subobject API, this variant provides a morphism image f ⟶ kernel g, which is sometimes more convenient.

Equations
@[simp]
theorem image_subobject_iso_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'_kernel_subobject_iso {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
noncomputable def homology_iso_cokernel_image_to_kernel' {V : Type u} {A B C : V} (f : A B) (g : B C) (w : f g = 0) :
g w

homology f g w can be computed as the cokernel of image_to_kernel' f g w.

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

homology f g w can be computed as the cokernel of kernel.lift g f w.

Equations