limitAlgebra — Mathlib

English

Given a diagram of R-algebras, the limit in the category of algebras carries a natural R-algebra structure on its carrier (i.e., the limit object is an R-algebra).

Русский

Дано диаграмма алгебр над R; предел в категории алгебр имеет естественную структуру R-алгебры на носителе (т. е. предел является R-алгеброй).

LaTeX

$$$$ \text{limitAlgebra}: \text{Algebra } R (\text{Types.Small.limitCone} (F \,\text{⋙ forget (AlgCat R)})).pt $$$$

Lean4

instance limitAlgebra : Algebra R (Types.Small.limitCone (F ⋙ forget (AlgCat.{w} R))).pt :=
  inferInstanceAs <| Algebra R (Shrink (sectionsSubalgebra F))

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