instIsTriangulatedFunctor

Mathlib.CategoryTheory.Triangulated.Adjunction

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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