instFullPresheafOfModulesValRingCatForget

Mathlib.Algebra.Category.ModuleCat.Sheaf

URI: https://scilib.ai/kg/mathlib#SheafOfModules.instFullPresheafOfModulesValRingCatForget

English

The forget R functor is full, i.e., every morphism in the base category lifts to the module category.

Русский

Функтор forget R полноты: каждый морфизм поднимается до модуля.

LaTeX

$$$\mathrm{forget}\;R\text{ is full}$$$

Lean4

instance : (forget.{v} R).Full :=
  (fullyFaithfulForget R).full

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

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

Разделы

Аффилиация

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