homologyFunctorFactors

Mathlib.Algebra.Homology.HomotopyCategory

URI: https://scilib.ai/kg/mathlib#HomotopyCategory.homologyFunctorFactors

Lean4

/-- The homology functor on the homotopy category is induced by
the homology functor on homological complexes. -/
noncomputable def homologyFunctorFactors (i : ι) :
    quotient V c ⋙ homologyFunctor V c i ≅ HomologicalComplex.homologyFunctor V c i :=
  Quotient.lift.isLift _ _
    _
      -- this is to prevent any abuse of defeq

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

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

Разделы

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

Аффилиация

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