exact_up_to_refinements — Mathlib

English

For a morphism γ: A → S.homology, there exist A', π, epi, z: A' → S.X2 with hz: z ≫ S.g = 0 such that π ≫ γ = S.liftCycles z hz ≫ S.homologyπ.

Русский

Для отображения γ: A → S.homology существует уточнение A' → A с эпиморфизмом π и з в S.X2 с hz: z ≫ S.g = 0, удовлетворяющее π ≫ γ = S.liftCycles z hz ≫ S.homologyπ.

LaTeX

$$$\\exists A',\\pi:A'\\to A\\; (\\pi\\ epi)\\; (z:A'\\to S.X_2),\\; (hz:z\\,S.g=0),\\; \\pi\\,\\gamma = S.liftCycles\\ z\\ hz\\, S.homology\\pi$$$

Lean4

theorem exact_up_to_refinements (hS : S.Exact) {A : C} (x₂ : A ⟶ S.X₂) (hx₂ : x₂ ≫ S.g = 0) :
    ∃ (A' : C) (π : A' ⟶ A) (_ : Epi π) (x₁ : A' ⟶ S.X₁), π ≫ x₂ = x₁ ≫ S.f :=
  by
  rw [ShortComplex.exact_iff_exact_up_to_refinements] at hS
  exact hS x₂ hx₂

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