English
The limit (in Types.Small) of a diagram F ⋙ forget CommSemiRingCat carries a commutative semiring structure, i.e., the limit object inherits the CommSemiring structure.
Русский
Предел диаграммы F ⋙ forget CommSemiRingCat в Types.Small обладает структурой CommSemiring, т.е. предел наделен структурой коммутативного полуприн.
LaTeX
$$$CommSemiring\big(\mathrm{Types.Small}.limitCone(F\!\!\to forget CommSemiRingCat)\big).pt$$$
Lean4
instance limitCommSemiring : CommSemiring (Types.Small.limitCone.{v, u} (F ⋙ forget CommSemiRingCat.{u})).pt :=
let _ : CommSemiring (F ⋙ forget CommSemiRingCat.{u}).sections :=
@Subsemiring.toCommSemiring (∀ j, F.obj j) _
(SemiRingCat.sectionsSubsemiring.{v, u} (F ⋙ forget₂ CommSemiRingCat.{u} SemiRingCat.{u}))
inferInstanceAs <| CommSemiring (Shrink (F ⋙ forget CommSemiRingCat.{u}).sections)
