uliftFunctor

Mathlib.Algebra.Category.MonCat.Basic

URI: https://scilib.ai/kg/mathlib#MonCat.uliftFunctor

Lean4

/-- Universe lift functor for monoids. -/
@[to_additive (attr := simps) /-- Universe lift functor for additive monoids. -/
    ]
def uliftFunctor : MonCat.{v} ⥤ MonCat.{max v u}
    where
  obj X := MonCat.of (ULift.{u, v} X)
  map {_ _} f := MonCat.ofHom <| MulEquiv.ulift.symm.toMonoidHom.comp <| f.hom.comp MulEquiv.ulift.toMonoidHom
  map_id X := by rfl
  map_comp {X Y Z} f g := by rfl

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

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

Разделы

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

Аффилиация

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