uliftFunctorFullyFaithful

Mathlib.Algebra.Category.Grp.Ulift

URI: https://scilib.ai/kg/mathlib#GrpCat.uliftFunctorFullyFaithful

Lean4

/-- The universe lift functor for groups is fully faithful.
-/
@[to_additive /-- The universe lift functor for additive groups is fully faithful. -/
    ]
def uliftFunctorFullyFaithful : uliftFunctor.{u, v}.FullyFaithful
    where
  preimage f := GrpCat.ofHom (MulEquiv.ulift.toMonoidHom.comp (f.hom.comp MulEquiv.ulift.symm.toMonoidHom))
  map_preimage _ := rfl
  preimage_map _ := rfl

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

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

Разделы

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

Аффилиация

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