Exact sequences #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
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
However in general it is weaker than other reasonable definitions of exactness,
- the inclusion map
image.ι f is a kernel of
image f ⟶ kernel g is an isomorphism or
image_subobject f = kernel_subobject f.
However when the category is abelian, these all become equivalent;
these results are found in
Main results #
- Suppose that cokernels exist and that
g are exact.
s is any kernel fork over
t is any cokernel cofork over
fork.ι s ≫ cofork.π t = 0.
- Precomposing the first morphism with an epimorphism retains exactness.
Postcomposing the second morphism with a monomorphism retains exactness.
g are exact and
i is an isomorphism,
f ≫ i.hom and
i.inv ≫ g are also exact.
Future work #
- Short exact sequences, split exact sequences, the splitting lemma (maybe only for abelian
- Two adjacent maps in a chain complex are exact iff the homology vanishes
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,
f g are exact iff they compose to zero and the homology vanishes.
A reformulation of
preadditive.exact_of_iso_of_exact that does not involve the arrow
The dual of this lemma is only true when
V is abelian, see
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