English
For ComposableArrows S with length n+2, S.Exact implies S.δ₀.Exact.
Русский
Для композиционных стрелок длины n+2 из S.Exact следует S.δ₀.Exact.
LaTeX
$$$S \in \mathrm{ComposableArrows}(C, n+2) \Rightarrow S.\delta_0 \mathrm{.Exact}$$$
Lean4
theorem exact_iff_δ₀ (S : ComposableArrows C (n + 2)) : S.Exact ↔ (mk₂ (S.map' 0 1) (S.map' 1 2)).Exact ∧ S.δ₀.Exact :=
by
constructor
· intro h
constructor
· rw [exact₂_iff]; swap
· rw [isComplex₂_iff]
exact h.toIsComplex.zero 0
exact h.exact 0 (by cutsat)
· exact Exact.mk (IsComplex.mk (fun i hi => h.toIsComplex.zero (i + 1))) (fun i hi => h.exact (i + 1))
· rintro ⟨h, h₀⟩
refine Exact.mk (IsComplex.mk (fun i hi => ?_)) (fun i hi => ?_)
· obtain _ | i := i
· exact h.toIsComplex.zero 0
· exact h₀.toIsComplex.zero i
· obtain _ | i := i
· exact h.exact 0
· exact h₀.exact i
