instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences

Mathlib.Algebra.Homology.Localization

URI: https://scilib.ai/kg/mathlib#instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences

Lean4

instance :
    (HomotopyCategory.quotient C (ComplexShape.down ι)).IsLocalization (HomologicalComplex.homotopyEquivalences _ _) :=
  (ComplexShape.down ι).quotient_isLocalization (fun _ => ⟨_, rfl⟩) C

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

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

Разделы

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

Аффилиация

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