limitCommRing — Mathlib

English

The limit (in the category of rings) of a functor F: J ⥤ CommRingCat carries a canonical commutative ring structure.

Русский

Предел (в категории колец) диаграммы F : J ⥤ CommRingCat обладает естественной структурой коммутативного кольца.

LaTeX

$$$\mathrm{CommRingCat}.\text{limitCone } F\; \text{is a limit cone; its vertex carries a commutative ring}. $$$

Lean4

instance limitCommRing : CommRing.{u} (Types.Small.limitCone.{v, u} (F ⋙ forget CommRingCat.{u})).pt :=
  let _ : CommRing (F ⋙ forget CommRingCat).sections :=
    @Subring.toCommRing (∀ j, F.obj j) _ (RingCat.sectionsSubring.{v, u} (F ⋙ forget₂ CommRingCat RingCat.{u}))
  inferInstanceAs <| CommRing (Shrink _)

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