contravariantSequence — Mathlib

English

Alternative covariant exactness statement for the second index; the ladder argument yields exactness.

Русский

Альтернативная формулировка точности для второго индекса ковариантной последовательности; лестничный аргумент даёт точность.

LaTeX

$$$\\text{covariantSequence\\_₂} = \\text{Exact}$$$

Lean4

/-- Given a short exact short complex `S` in an abelian category `C` and an object `Y : C`,
this is the long exact sequence
`Ext S.X₃ Y n₀ → Ext S.X₂ Y n₀ → Ext S.X₁ Y n₀ → Ext S.X₃ Y n₁ → Ext S.X₂ Y n₁ → Ext S.X₁ Y n₁`
when `1 + n₀ = n₁`. -/
noncomputable def contravariantSequence : ComposableArrows AddCommGrpCat.{w} 5 :=
  mk₅ (AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y (zero_add n₀)))
    (AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y (zero_add n₀))) (AddCommGrpCat.ofHom (hS.extClass.precomp Y h))
    (AddCommGrpCat.ofHom ((mk₀ S.g).precomp Y (zero_add n₁))) (AddCommGrpCat.ofHom ((mk₀ S.f).precomp Y (zero_add n₁)))

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