mapHomotopyCategory

Mathlib.Algebra.Homology.HomotopyCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.NatTrans.mapHomotopyCategory

Lean4

/-- A natural transformation induces a natural transformation between
  the induced functors on the homotopy category. -/
@[simps]
def mapHomotopyCategory {F G : V ⥤ W} [F.Additive] [G.Additive] (α : F ⟶ G) (c : ComplexShape ι) :
    F.mapHomotopyCategory c ⟶ G.mapHomotopyCategory c
    where
  app C := (HomotopyCategory.quotient W c).map ((NatTrans.mapHomologicalComplex α c).app C.as)
  naturality := by
    rintro ⟨C⟩ ⟨D⟩ ⟨f : C ⟶ D⟩
    simp only [HomotopyCategory.quot_mk_eq_quotient_map, Functor.mapHomotopyCategory_map, ← Functor.map_comp,
      NatTrans.naturality]

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

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

Разделы

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

Аффилиация

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