singleFunctorsPostcompQhIso — Mathlib

English

There is an isomorphism between the functors singleFunctors C and (HomotopyCategory.singleFunctors C).postcomp Qh, i.e., the singleFunctors structure is compatible with the quotient-to-derived construction.

Русский

Существует изоморфизм между функтором singleFunctors и (HomotopyCategory.singleFunctors).postcomp Qh; структура singleFunctors согласована с переходом к производной через факторизацию.

LaTeX

$$singleFunctorsPostcompQIso : singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh$$

Lean4

/-- The isomorphism
`DerivedCategory.singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh` given
by the definition of `DerivedCategory.singleFunctors`. -/
noncomputable def singleFunctorsPostcompQhIso : singleFunctors C ≅ (HomotopyCategory.singleFunctors C).postcomp Qh :=
  Iso.refl _

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