limitRing — Mathlib

English

The limit of a diagram F : J ⥤ RingCat carries a natural ring structure, obtained by transporting the limit from types via the forgetful functor.

Русский

Предел диаграммы F : J ⥤ RingCat естественным образом образует кольцо, получаемое переносом предела из множеств через забывающий функтор.

LaTeX

$$$ \\text{limitRing } :\\; \\operatorname{Ring}( \\mathrm{Types.Small}.limitCone( F\\,\\mathrm{forget RingCat} ).\\mathrm{pt} )$$$

Lean4

instance limitRing : Ring.{u} (Types.Small.limitCone.{v, u} (F ⋙ forget RingCat.{u})).pt :=
  let _ : Ring (F ⋙ forget RingCat.{u}).sections := (sectionsSubring F).toRing
  inferInstanceAs <| Ring (Shrink _)

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