δlast — Mathlib

English

Let S be a composable chain of length n+2 in a category with zero morphisms. If the chain is exact, then the last delta morphism is exact as well.

Русский

Пусть S — композиционная последовательность длины n+2 в категории с нулевыми морфизмами. Если цепочка точна, то и последний переход δ_last образует точную последовательность.

LaTeX

$$$ S\,.Exact \rightarrow S_{\delta\!\text{last}}.Exact $$$

Lean4

theorem δlast {S : ComposableArrows C (n + 2)} (hS : S.Exact) : S.δlast.Exact :=
  by
  rw [exact_iff_δlast] at hS
  exact hS.1

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