English
For S in ComposableArrows C (n+2), S.Exact is equivalent to S.δlast.Exact and the tail two arrows are exact simultaneously.
Русский
Для S в ComposableArrows C (n+2) точность S эквивалентна δlast.Exact и тому, что хвостовые две стрелки точны одновременно.
LaTeX
$$$S \in \mathrm{ComposableArrows}(C, n+2) \Rightarrow S.\mathrm{Exact} \iff \big( S.\delta_{\mathrm{last}}.\mathrm{Exact} \land (mk_2 (S.map' n (n+1)) (S.map' (n+1) (n+2))).\mathrm{Exact} \big)$$$
Lean4
theorem exact_iff_δlast {n : ℕ} (S : ComposableArrows C (n + 2)) :
S.Exact ↔ S.δlast.Exact ∧ (mk₂ (S.map' n (n + 1)) (S.map' (n + 1) (n + 2))).Exact :=
by
constructor
· intro h
constructor
· exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero i)) (fun i hi => h.exact i)
· rw [exact₂_iff]; swap
· rw [isComplex₂_iff]
exact h.toIsComplex.zero n
exact h.exact n (by cutsat)
· rintro ⟨h, h'⟩
refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
· simp only [Nat.add_le_add_iff_right] at hi
obtain hi | rfl := hi.lt_or_eq
· exact h.toIsComplex.zero i
· exact h'.toIsComplex.zero 0
· simp only [Nat.add_le_add_iff_right] at hi
obtain hi | rfl := hi.lt_or_eq
· exact h.exact i
· exact h'.exact 0
