limitModule — Mathlib

English

For a diagram F: J → Module_R, the limit vertex is a module over R.

Русский

Для диаграммы F: J → Module_R вершина предела является модулем над кольцом R.

LaTeX

$${$\operatorname{Module}\!$ }\left( \mathrm{Types.Small.limitCone}(F \to \mathrm{forget}(\mathrm{ModuleCat}\,R))\right).pt$$

Lean4

instance limitModule : Module R (Types.Small.limitCone.{v, w} (F ⋙ forget (ModuleCat.{w} R))).pt :=
  inferInstanceAs <| Module R (Shrink (sectionsSubmodule F))

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