mathlib documentation

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.

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

@[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]
theorem homology.ext {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) [category_theory.limits.has_cokernel (image_to_kernel f g w)] {D : V} {k k' : homology f g w D} (p : homology.π f g w k = homology.π f g w k') :
k = k'

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