English
The projection maps from the limit cone to each component are assembled into a ring homomorphism.
Русский
Проекции из предельного конуса в соответствующие компоненты образуют гомоморфизм колец.
LaTeX
$$$\text{limitπRingHom}(F, j) : \mathrm{Types.Small.limitCone}(\dots) \to (F \to \text{forget SemiRingCat}).obj j$$$
Lean4
/-- `limit.π (F ⋙ forget SemiRingCat) j` as a `RingHom`. -/
def limitπRingHom (j) : (Types.Small.limitCone.{v, u} (F ⋙ forget SemiRingCat)).pt →+* (F ⋙ forget SemiRingCat).obj j :=
let f : J ⥤ AddMonCat.{u} := F ⋙ forget₂ SemiRingCat.{u} AddCommMonCat.{u} ⋙ forget₂ AddCommMonCat AddMonCat
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ MonCat) ⋙ forget MonCat)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget SemiRingCat.{u}))
let _ : Small.{u} (Functor.sections (f ⋙ forget AddMonCat)) :=
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget SemiRingCat.{u}))
{ AddMonCat.limitπAddMonoidHom f j, MonCat.limitπMonoidHom (F ⋙ forget₂ SemiRingCat MonCat.{u}) j with
toFun := (Types.Small.limitCone (F ⋙ forget SemiRingCat)).π.app j }
