singleTriangle

Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.ShortExact.singleTriangle

Lean4

/-- The (distinguished) triangle in the derived category of `C` given by a
short exact short complex in `C`. -/
@[simps!]
noncomputable def singleTriangle : Triangle (DerivedCategory C) :=
  Triangle.mk ((singleFunctor C 0).map S.f) ((singleFunctor C 0).map S.g) hS.singleδ

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

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

Разделы

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

Аффилиация

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