homologySequence_exact₂ — Mathlib

English

There is an equivalence between epi-ness of (F.shift n0).map T.mor1 and δ = 0.

Русский

Существуют эквивалентности между эпиморфизмом (F.shift n0).map T.mor1 и δ = 0.

LaTeX

$$$\operatorname{Epi}((F.shift n_0).map T.mor_1) \iff F.homologySequenceδ T n_0 n_1 h = 0$$$

Lean4

theorem homologySequence_exact₂ : (ShortComplex.mk _ _ (F.homologySequence_comp T hT n₀)).Exact :=
  by
  refine ShortComplex.exact_of_iso ?_ (F.map_distinguished_exact _ (Triangle.shift_distinguished _ hT n₀))
  exact
    ShortComplex.isoMk ((F.isoShift n₀).app _) (n₀.negOnePow • ((F.isoShift n₀).app _)) ((F.isoShift n₀).app _)
      (by simp) (by simp)

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