mathlib documentation


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 #

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.

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

theorem category_theory.preadditive.exact_of_iso_of_exact' {V : Type u} [category_theory.category V] [category_theory.limits.has_images V] [category_theory.limits.has_zero_object V] [category_theory.preadditive V] [category_theory.limits.has_kernels V] [category_theory.limits.has_cokernels V] {A₁ B₁ C₁ A₂ B₂ C₂ : V} (f₁ : A₁ B₁) (g₁ : B₁ C₁) (f₂ : A₂ B₂) (g₂ : B₂ C₂) (α : A₁ A₂) (β : B₁ B₂) (γ : C₁ C₂) (hsq₁ : α.hom f₂ = f₁ β.hom) (hsq₂ : β.hom g₂ = g₁ γ.hom) (h : category_theory.exact f₁ g₁) :

A reformulation of preadditive.exact_of_iso_of_exact that does not involve the arrow category.

The dual of this lemma is only true when V is abelian, see abelian.exact_epi_comp_iff.

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] (h : category_theory.exact f g) {X Y : V} {ι : X B} (hι : ι g = 0) {π : B Y} (hπ : f π = 0) :
ι π = 0

A functor reflects exact sequences if any composable pair of morphisms that is mapped to an exact pair is itself exact.

Instances of this typeclass
Instances of other typeclasses for category_theory.functor.reflects_exact_sequences
  • category_theory.functor.reflects_exact_sequences.has_sizeof_inst