instIsHomologicalCompOfIsTriangulated

Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instIsHomologicalCompOfIsTriangulated

← MathLib Explorer

English

If L is triangulated and F is homological, then the composition L ⋅ F is homological.

Русский

Если L трангулирован и F гомологичен, то композиция L ⋅ F гомологична.

LaTeX

$$$(L \\cdot F).IsHomological$$$

Lean4

instance (L : C ⥤ D) (F : D ⥤ A) [L.CommShift ℤ] [L.IsTriangulated] [F.IsHomological] : (L ⋙ F).IsHomological where
  exact T hT := F.map_distinguished_exact _ (L.map_distinguished T hT)

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

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

Разделы

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

Аффилиация

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