quotientCompQhIso — Mathlib

English

There is a natural isomorphism between the composition HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh and Q.

Русский

Существует естественный изоморфизм между композициями: HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh и Q.

LaTeX

$$$\\text{quotientCompQhIso} :\\; HomotopyCategory.quotient C (ComplexShape.up ℤ) \\;\\!\\!\\!⊗\\; Qh \\cong Q.$$$

Lean4

/-- The natural isomorphism `HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q`. -/
def quotientCompQhIso : HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh ≅ Q :=
  HomologicalComplexUpToQuasiIso.quotientCompQhIso C (ComplexShape.up ℤ)

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