instIsTriangulatedInverse

Mathlib.CategoryTheory.Triangulated.Adjunction

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.IsTriangulated.instIsTriangulatedInverse

English

If the equivalence E is triangulated, then its inverse functor E.inverse is triangulated.

Русский

Если эквивалентность E триангулирована, то её обратный функтор E.inverse является триангулированным.

LaTeX

$$$\mathrm{IsTriangulated}(E) \Rightarrow \mathrm{IsTriangulated}(E.{\text{inverse}}).$$$

Lean4

instance [E.IsTriangulated] : E.inverse.IsTriangulated :=
  inferInstance

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

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

Разделы

Аффилиация

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