Qh

Mathlib.Algebra.Homology.Localization

URI: https://scilib.ai/kg/mathlib#HomologicalComplexUpToQuasiIso.Qh

Lean4

/-- The functor `HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c` from the homotopy
category to the localized category with respect to quasi-isomorphisms. -/
def Qh : HomotopyCategory C c ⥤ HomologicalComplexUpToQuasiIso C c :=
  CategoryTheory.Quotient.lift _ HomologicalComplexUpToQuasiIso.Q
    (by
      intro K L f g ⟨h⟩
      exact Q_map_eq_of_homotopy h)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru