instModuleCarrierObjOppositeRingCatCarrierAbPresheaf

Mathlib.Algebra.Category.ModuleCat.Presheaf

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.instModuleCarrierObjOppositeRingCatCarrierAbPresheaf

English

For every X, the fibre M.obj X carries the structure of a module over the ring R.obj X.

Русский

Для каждого X фибра M.obj X имеет структуру модуля над кольцом R.obj X.

LaTeX

$$$\forall X,\text{Module}(R.obj X, M.obj X).$$$

Lean4

instance (M : PresheafOfModules R) (X : Cᵒᵖ) : Module (R.obj X) (M.presheaf.obj X) :=
  inferInstanceAs (Module (R.obj X) (M.obj X))

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

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

Разделы

Аффилиация

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