exact_of_δlast — Mathlib

English

Let S be a Composable Arrows diagram of length n+2. If the last δ is exact and the two-entry map mk₂ is exact, then S is exact.

Русский

Пусть диаграмма ComposableArrows длины n+2 имеет δ_last точную последовательность; если также точна пара входов mk₂, то вся диаграмма S точна.

LaTeX

$$$ S.\\delta_{last} \\text{ is exact } \\land \\bigl( \\mathrm{mk}_2\\bigl(S.map'(n,n+1) , S.map'(n+1,n+2)\\bigr) \\bigr).Exact \\Rightarrow S.Exact $$$

Lean4

theorem exact_of_δlast {n : ℕ} (S : ComposableArrows C (n + 2)) (h₁ : S.δlast.Exact)
    (h₂ : (mk₂ (S.map' n (n + 1)) (S.map' (n + 1) (n + 2))).Exact) : S.Exact :=
  by
  rw [exact_iff_δlast]
  constructor <;> assumption

Похожие утверждения