mathlib documentation

algebra.homology.exact

Exact sequences #

In a category with zero morphisms, images, and equalizers we say that f : A ⟶ B and g : B ⟶ C are exact if f ≫ g = 0 and the natural map image f ⟶ kernel g is an epimorphism.

In any preadditive category this is equivalent to the homology at B vanishing.

However in general it is weaker than other reasonable definitions of exactness, particularly that

  1. the inclusion map image.ι f is a kernel of g or
  2. image f ⟶ kernel g is an isomorphism or
  3. image_subobject f = kernel_subobject f. However when the category is abelian, these all become equivalent; these results are found in category_theory/abelian/exact.lean.

Main results #

Future work #

@[class]

Two morphisms f : A ⟶ B, g : B ⟶ C are called exact if w : f ≫ g = 0 and the natural map image_to_kernel f g w : image_subobject f ⟶ kernel_subobject g is an epimorphism.

In any preadditive category, this is equivalent to w : f ≫ g = 0 and homology f g w ≅ 0.

In an abelian category, this is equivalent to image_to_kernel f g w being an isomorphism, and hence equivalent to the usual definition, image_subobject f = kernel_subobject g.

Instances
@[simp]

In any preadditive category, composable morphisms f g are exact iff they compose to zero and the homology vanishes.

theorem category_theory.comp_eq_zero_of_exact {V : Type u} [category_theory.category V] [category_theory.limits.has_images V] {A B C : V} (f : A B) (g : B C) [category_theory.limits.has_zero_morphisms V] [category_theory.limits.has_equalizers V] [category_theory.limits.has_cokernels V] [category_theory.exact f g] {X Y : V} {ι : X B} (hι : ι g = 0) {π : B Y} (hπ : f «π» = 0) :
ι «π» = 0