limitAddCommMonoid — Mathlib

English

For a diagram F: J → Module_R, the limit cone's vertex, viewed as a type, inherits an AddCommMonoid structure.

Русский

Для диаграммы F: J → Mod_R, вершина ограничивающего конуса, как множество, наследует структуру добавочно-коммутативного моноида.

LaTeX

$$$\operatorname{AddCommMonoid} \big( \mathrm{Types.Small.limitCone}(F \to \mathrm{forget}(\mathrm{ModuleCat}\,R)).pt \big)$$$

Lean4

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

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