contravariant_sequence_exact₂ — Mathlib

English

Alternative contravariant exactness: given x2 with zero composition from mk₀ S.f, there exists x1 with the corresponding composition to x2.

Русский

Альтернативная точность контравариантной последовательности: при заданном x2 с нулевой композицией от mk₀ S.f существует x1 с соответствующей композицией к x2.

LaTeX

$$$\\exists x_1, x_1 \\text{ satisfies } x_1 \\circ (mk_0 S.f) = x_2$$$

Lean4

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

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