English
If first two arrows form an exact sequence and tail δ₀ is exact, then the whole S is exact.
Русский
Если первые две стрелки образуют точную последовательность, и хвост δ₀ точен, тогда вся S точна.
LaTeX
$$$\text{If } (mk_2( S.map' 0 1, S.map' 1 2 )).\mathrm{Exact} \text{ and } S.\delta_0.\mathrm{Exact}, \text{ then } S.\mathrm{Exact}$$$
Lean4
/-- If `S : ComposableArrows C (n + 2)` is such that the first two arrows form
an exact sequence and that the tail `S.δ₀` is exact, then `S` is also exact.
See `ShortComplex.SnakeInput.snake_lemma` in `Algebra.Homology.ShortComplex.SnakeLemma`
for a use of this lemma. -/
theorem exact_of_δ₀ {S : ComposableArrows C (n + 2)} (h : (mk₂ (S.map' 0 1) (S.map' 1 2)).Exact) (h₀ : S.δ₀.Exact) :
S.Exact := by
rw [exact_iff_δ₀]
constructor <;> assumption
