comp

Mathlib.CategoryTheory.Triangulated.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Adjunction.IsTriangulated.comp

← MathLib Explorer

English

Constructor to build a triangulated adjunction from a triangulated left adjoint.

Русский

Конструктор триангулированного сопряжения из левого треугольного вложения.

LaTeX

$$mk'' [G.IsTriangulated] : adj.IsTriangulated$$

Lean4

/-- A composition of triangulated adjunctions is triangulated.
-/
instance comp [adj.IsTriangulated] [adj'.IsTriangulated] : (adj.comp adj').IsTriangulated where

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

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

Разделы

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

Аффилиация

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