homologySequence_exact₃ — Mathlib

English

Equivalent reformulation of the previous criterion for morphism mor1 in the shifted triangle.

Русский

Эквивалентная формулировка критерия для морфизма mor1 в сдвинутом треугольнике.

LaTeX

$$$\text{same as 82137}$$$

Lean4

theorem homologySequence_exact₃ : (ShortComplex.mk _ _ (F.comp_homologySequenceδ T hT _ _ h)).Exact :=
  by
  refine ShortComplex.exact_of_iso ?_ (F.homologySequence_exact₂ _ (rot_of_distTriang _ hT) n₀)
  exact
    ShortComplex.isoMk (Iso.refl _) (Iso.refl _) ((F.shiftIso 1 n₀ n₁ (by cutsat)).app _) (by simp)
      (by simp [homologySequenceδ, shiftMap])

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