instFullUlift

Mathlib.Algebra.Category.FGModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#FGModuleCat.instFullUlift

English

The ULift forgetful functor is full: every morphism between ULift-objects comes from FGModuleCat.

Русский

Полнота функторa забывания ULift: каждый морфизм между ULift-объектами исходит из FGModuleCat.

LaTeX

$$$(\\mathrm{ULift}.Full)$$$

Lean4

instance : (ulift R).Full :=
  (fullyFaithfulULift R).full

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

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

Разделы

Аффилиация

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