L₀'_exact — Mathlib

English

The object at L3 is exact.

Русский

Объект L3 образует точную последовательность.

LaTeX

$$$\\operatorname{Exact}(S.L_3)$$$

Lean4

theorem L₀'_exact : S.L₀'.Exact :=
  by
  rw [ShortComplex.exact_iff_exact_up_to_refinements]
  intro A x₂ hx₂
  dsimp [L₀'] at x₂ hx₂
  obtain ⟨A', π, hπ, x₁, fac⟩ :=
    S.L₁_exact.exact_up_to_refinements (x₂ ≫ pullback.fst _ _)
      (by rw [assoc, pullback.condition, reassoc_of% hx₂, zero_comp])
  exact ⟨A', π, hπ, x₁, pullback.hom_ext (by simpa [L₀'] using fac) (by simp [L₀', hx₂])⟩

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