mathlib3 documentation

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.

@[protected, instance]

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]

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).

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

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

Equations
@[ext]

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

homology 0 0 _ is just the middle object.

Equations

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.

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
theorem homology.comp_right_eq_comp_left {V : Type u_1} [category_theory.category V] {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₃} {α₁ : category_theory.arrow.mk f₁ category_theory.arrow.mk f₂} {β₁ : category_theory.arrow.mk g₁ category_theory.arrow.mk g₂} {α₂ : category_theory.arrow.mk f₂ category_theory.arrow.mk f₃} {β₂ : category_theory.arrow.mk g₂ category_theory.arrow.mk g₃} (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
(α₁ α₂).right = (β₁ β₂).left

Auxiliary lemma for homology computations.

theorem homology.map_comp_assoc {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {A₁ B₁ C₁ : V} {f₁ : A₁ B₁} [category_theory.limits.has_image f₁] {g₁ : B₁ C₁} [category_theory.limits.has_kernel g₁] (w₁ : f₁ g₁ = 0) {A₂ B₂ C₂ : V} {f₂ : A₂ B₂} [category_theory.limits.has_image f₂] {g₂ : B₂ C₂} [category_theory.limits.has_kernel g₂] (w₂ : f₂ g₂ = 0) {A₃ B₃ C₃ : V} {f₃ : A₃ B₃} [category_theory.limits.has_image f₃] {g₃ : B₃ C₃} [category_theory.limits.has_kernel g₃] (w₃ : f₃ g₃ = 0) (α₁ : category_theory.arrow.mk f₁ category_theory.arrow.mk f₂) [category_theory.limits.has_image_map α₁] (β₁ : category_theory.arrow.mk g₁ category_theory.arrow.mk g₂) (α₂ : category_theory.arrow.mk f₂ category_theory.arrow.mk f₃) [category_theory.limits.has_image_map α₂] (β₂ : category_theory.arrow.mk g₂ category_theory.arrow.mk g₃) [category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)] [category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)] [category_theory.limits.has_cokernel (image_to_kernel f₃ g₃ w₃)] (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) {X' : V} (f' : homology f₃ g₃ w₃ X') :
homology.map w₁ w₂ α₁ β₁ p₁ homology.map w₂ w₃ α₂ β₂ p₂ f' = homology.map w₁ w₃ (α₁ α₂) (β₁ β₂) _ f'
theorem homology.map_comp {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {A₁ B₁ C₁ : V} {f₁ : A₁ B₁} [category_theory.limits.has_image f₁] {g₁ : B₁ C₁} [category_theory.limits.has_kernel g₁] (w₁ : f₁ g₁ = 0) {A₂ B₂ C₂ : V} {f₂ : A₂ B₂} [category_theory.limits.has_image f₂] {g₂ : B₂ C₂} [category_theory.limits.has_kernel g₂] (w₂ : f₂ g₂ = 0) {A₃ B₃ C₃ : V} {f₃ : A₃ B₃} [category_theory.limits.has_image f₃] {g₃ : B₃ C₃} [category_theory.limits.has_kernel g₃] (w₃ : f₃ g₃ = 0) (α₁ : category_theory.arrow.mk f₁ category_theory.arrow.mk f₂) [category_theory.limits.has_image_map α₁] (β₁ : category_theory.arrow.mk g₁ category_theory.arrow.mk g₂) (α₂ : category_theory.arrow.mk f₂ category_theory.arrow.mk f₃) [category_theory.limits.has_image_map α₂] (β₂ : category_theory.arrow.mk g₂ category_theory.arrow.mk g₃) [category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)] [category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)] [category_theory.limits.has_cokernel (image_to_kernel f₃ g₃ w₃)] (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
homology.map w₁ w₂ α₁ β₁ p₁ homology.map w₂ w₃ α₂ β₂ p₂ = homology.map w₁ w₃ (α₁ α₂) (β₁ β₂) _
noncomputable def homology.map_iso {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {A₁ B₁ C₁ : V} {f₁ : A₁ B₁} [category_theory.limits.has_image f₁] {g₁ : B₁ C₁} [category_theory.limits.has_kernel g₁] (w₁ : f₁ g₁ = 0) {A₂ B₂ C₂ : V} {f₂ : A₂ B₂} [category_theory.limits.has_image f₂] {g₂ : B₂ C₂} [category_theory.limits.has_kernel g₂] (w₂ : f₂ g₂ = 0) [category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)] [category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)] (α : category_theory.arrow.mk f₁ category_theory.arrow.mk f₂) (β : category_theory.arrow.mk g₁ category_theory.arrow.mk g₂) (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
noncomputable def homology.congr {V : Type u} [category_theory.category V] [category_theory.limits.has_zero_morphisms V] {A B C : V} {f : A B} {g : B C} (w : f g = 0) {f' : A B} {g' : B C} (w' : f' g' = 0) [category_theory.limits.has_kernels V] [category_theory.limits.has_cokernels V] [category_theory.limits.has_images V] [category_theory.limits.has_image_maps V] (pf : f = f') (pg : g = g') :
homology f 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.

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