limitAddCommGroup — Mathlib

English

For a diagram F: J → Module_R, the limit cone's vertex carries an AddCommGroup structure.

Русский

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

LaTeX

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

Lean4

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

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