functor

Mathlib.CategoryTheory.Shift.Opposite

URI: https://scilib.ai/kg/mathlib#CategoryTheory.OppositeShift.functor

Lean4

/-- The functor `F.op`, seen as a functor from `OppositeShift C A` to `OppositeShift D A`.
(We will use this to carry a `CommShift` instance for the naive shifts on the opposite category.
Then, in the pretriangulated case, we will be able to put a `CommShift` instance on `F.op`
for the modified shifts and not deal with instance clashes.
-/
def functor : OppositeShift C A ⥤ OppositeShift D A :=
  F.op

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

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

Разделы

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

Аффилиация

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