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.
Main results
- Suppose that cokernels exist and that
fandgare exact. Ifsis any kernel fork overgandtis any cokernel cofork overf, thenfork.ι s ≫ cofork.π t = 0.
See also category_theory/abelian/exact.lean for results that only hold in abelian categories.
Future work
- Short exact sequences, split exact sequences, the splitting lemma (maybe only for abelian categories?)
- Two adjacent maps in a chain complex are exact iff the homology vanishes
- Composing with isomorphisms retains exactness, and similar constructions
@[class]
structure
category_theory.exact
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
{A B C : V} :
- w : f ≫ g = 0
- epi : category_theory.epi (category_theory.image_to_kernel_map f g category_theory.exact.w)
Two morphisms f : A ⟶ B, g : B ⟶ C are called exact if f ≫ g = 0 and the natural map
image f ⟶ kernel g is an epimorphism.
@[simp]
theorem
category_theory.kernel_comp_cokernel_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.exact f g]
{X' : V}
(f' : category_theory.limits.cokernel f ⟶ X') :
category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f ≫ f' = 0 ≫ f'
@[simp]
theorem
category_theory.kernel_comp_cokernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.exact f g] :
theorem
category_theory.comp_eq_zero_of_exact
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.exact f g]
{X Y : V}
{ι : X ⟶ B}
(hι : ι ≫ g = 0)
{π : B ⟶ Y} :
@[simp]
theorem
category_theory.fork_ι_comp_cofork_π
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.exact f g]
(s : category_theory.limits.kernel_fork g)
(t : category_theory.limits.cokernel_cofork f) :
@[simp]
theorem
category_theory.fork_ι_comp_cofork_π_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.exact f g]
(s : category_theory.limits.kernel_fork g)
(t : category_theory.limits.cokernel_cofork f)
{X' : V}
(f' : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj t.X).obj category_theory.limits.walking_parallel_pair.one ⟶ X') :
category_theory.limits.fork.ι s ≫ category_theory.limits.cofork.π t ≫ f' = 0 ≫ f'