isTriangulated_leftAdjoint

Mathlib.CategoryTheory.Triangulated.Adjunction

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

← MathLib Explorer

English

Constructs IsTriangulated for the right adjoint via mk'.

Русский

Конструируется IsTriangulated для правого сопряженного через mk'.

LaTeX

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

Lean4

/-- The left adjoint of a triangulated functor is triangulated.
-/
theorem isTriangulated_leftAdjoint [G.IsTriangulated] : F.IsTriangulated :=
  by
  have := isTriangulated_rightAdjoint adj.op
  exact F.isTriangulated_of_op

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

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

Разделы

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

Аффилиация

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