instIsTriangulatedDerivedCategoryMapDerivedCategory

Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor

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

English

The derived-category map functor is triangulated.

Русский

Функтор отображения из производной категории треугольный.

LaTeX

$$$F.mapDerivedCategory\;IsTriangulated$$$

Lean4

instance : F.mapDerivedCategory.IsTriangulated :=
  Functor.isTriangulated_of_precomp_iso F.mapDerivedCategoryFactorsh

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

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

Разделы

Аффилиация

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