quasiIsoAt_iff' — Mathlib

English

For an isomorphism f, the quasi-isomorphism at i follows; the same as previous but stated in variant form.

Русский

Для изоморфизма f квазиизоморфизм на i следует; формулировка варианта соответствует предыдущей.

LaTeX

$$QuasiIsoAt f i$$

Lean4

theorem quasiIsoAt_iff' (f : K ⟶ L) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) [K.HasHomology j]
    [L.HasHomology j] [(K.sc' i j k).HasHomology] [(L.sc' i j k).HasHomology] :
    QuasiIsoAt f j ↔ ShortComplex.QuasiIso ((shortComplexFunctor' C c i j k).map f) :=
  by
  rw [quasiIsoAt_iff]
  exact ShortComplex.quasiIso_iff_of_arrow_mk_iso _ _ (Arrow.isoOfNatIso (natIsoSc' C c i j k hi hk) (Arrow.mk f))

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