covariant_sequence_exact₃ — Mathlib

English

Alternative formulation of covariant_sequence_exact₃: the constructed five-term short exact diagram is exact.

Русский

Альтернативная формулировка covariant_sequence_exact₃: построенная пятиэлементная точная диаграмма точна.

LaTeX

$$$(\\mathrm{covariantSequence\\_₃'}\\;X\\;hS\\;n_0\\;n_1\\;h).\\mathrm{Exact}$$$

Lean4

theorem covariant_sequence_exact₃ {n₀ : ℕ} (x₃ : Ext X S.X₃ n₀) {n₁ : ℕ} (hn₁ : n₀ + 1 = n₁)
    (hx₃ : x₃.comp hS.extClass hn₁ = 0) : ∃ (x₂ : Ext X S.X₂ n₀), x₂.comp (mk₀ S.g) (add_zero n₀) = x₃ :=
  by
  have := covariant_sequence_exact₃' X hS n₀ n₁ hn₁
  rw [ShortComplex.ab_exact_iff] at this
  exact this x₃ hx₃

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