covariant_sequence_exact₂ — Mathlib

English

The standard covariant exact sequence for Ext is exact for all n, given a short exact S.

Русский

Стандартная ковариантная точная последовательность для Ext точна для всех n при заданной короткой точной последовательности S.

LaTeX

$$$\\mathrm{covariantSequence}\\;X\\;hS\\;n\\;\\text{is exact}$$$

Lean4

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

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