exactAt_iff_of_quasiIsoAt — Mathlib

English

If f is quasi-iso at i, then K.ExactAt i iff L.ExactAt i.

Русский

Если f ~ является квазиизо на i, то K.ExactAt i эквивалентно L.ExactAt i.

LaTeX

$$K.ExactAt i \iff L.ExactAt i$$

Lean4

theorem exactAt_iff_of_quasiIsoAt (f : K ⟶ L) (i : ι) [K.HasHomology i] [L.HasHomology i] [QuasiIsoAt f i] :
    K.ExactAt i ↔ L.ExactAt i :=
  ⟨fun hK => (quasiIsoAt_iff_exactAt f i hK).1 inferInstance, fun hL =>
    (quasiIsoAt_iff_exactAt' f i hL).1 inferInstance⟩

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