English
Coherence properties of the projection maps of the limit cone to each component hold as usual for ring homomorphisms.
Русский
Свойства согласованности проекционных отображений ограниченного конуса к каждому компоненту выполняются как обычно для гомоморфизмов колец.
LaTeX
$$$((\text{MonCat}.limitπMonoidHom)(F))$ respects composition with each component.$$
Lean4
/-- Construction of a limit cone in `SemiRingCat`.
(Internal use only; use the limits API.)
-/
def limitCone : Cone F where
pt := SemiRingCat.of (Types.Small.limitCone (F ⋙ forget _)).pt
π :=
{ app := fun j ↦ SemiRingCat.ofHom <| limitπRingHom.{v, u} F j
naturality := fun {_ _} f ↦ hom_ext <| RingHom.coe_inj ((Types.Small.limitCone (F ⋙ forget _)).π.naturality f) }
