moduleObj — Mathlib

English

There is a canonical module structure on objects obtained by forgetting to the underlying type in a diagram valued in ModuleCat.

Русский

Для объектов, полученных от диаграммы в ModuleCat, существует каноническая структура модуля на забытом объекте типа.

LaTeX

$$$$ \\text{ModuleCat.moduleObj}(F, j) \\in \\text{Mod}_R $$$$

Lean4

instance moduleObj (j) : Module.{u, w} R ((F ⋙ forget (ModuleCat R)).obj j) :=
  inferInstanceAs <| Module R (F.obj j)

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