quasiIso_unopFunctor_map_iff — Mathlib

English

Dually to the op-case, for unopFunctor, quasi-isomorphism status is equivalent: QuasiIso((unopFunctor V c).map φ.op) ⇔ QuasiIso φ.

Русский

Дуально к случаю противоложного функторa, для unopFunctor статус квазиизоморфизма эквивалентен: QuasiIso((unopFunctor V c).map φ.op) ⇔ QuasiIso φ.

LaTeX

$$$\\text{QuasiIso}((\\mathrm{unopFunctor} V c).map φ.op) \\iff \\text{QuasiIso} φ$$$

Lean4

@[simp]
theorem quasiIso_unopFunctor_map_iff {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L) [∀ i, K.HasHomology i]
    [∀ i, L.HasHomology i] : QuasiIso ((unopFunctor _ _).map φ.op) ↔ QuasiIso φ := by
  simp only [quasiIso_iff, quasiIsoAt_unopFunctor_map_iff]

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