quasiIsoAt_unopFunctor_map_iff — Mathlib

English

Dual statement to the op-case: For φ: K → L, quasi-isomorphism status at i for unopFunctor map φ.op is equivalent to quasi-isomorphism status for φ at i.

Русский

Двойственное утверждение к случаю op: для φ: K → L эквивалентно, что k(z) в i-й степени — квазиизоморфизм.

LaTeX

$$$\\text{QuasiIsoAt}((\\mathrm{unopFunctor} \\; V \\; c).map φ.op) i \\iff \\text{QuasiIsoAt}(φ, i)$$$

Lean4

@[simp]
theorem quasiIsoAt_unopFunctor_map_iff {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) (i : ι) [K.HasHomology i]
    [L.HasHomology i] : QuasiIsoAt ((unopFunctor _ _).map φ.op) i ↔ QuasiIsoAt φ i :=
  by
  rw [← quasiIsoAt_opFunctor_map_iff]
  rfl

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