quasiIsoAt₀_iff — Mathlib

English

For Chain complexes over Nat, QuasiIsoAt f 0 is equivalent to the shortComplexQuasiIso of the corresponding shortComplexFunctor.

Русский

Для цепных комплексoв над Nat QuasiIsoAt f 0 эквивалентно сокращённому комплексному отображению соответствующего shortComplexFunctor.

LaTeX

$$QuasiIsoAt f 0 \iff ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C _ 1 0 0).map f)$$

Lean4

theorem quasiIsoAt₀_iff {K L : ChainComplex C ℕ} (f : K ⟶ L) [K.HasHomology 0] [L.HasHomology 0]
    [(K.sc' 1 0 0).HasHomology] [(L.sc' 1 0 0).HasHomology] :
    QuasiIsoAt f 0 ↔ ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C _ 1 0 0).map f) :=
  quasiIsoAt_iff' _ _ _ _ (by simp) (by simp)

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