English
Let F be a diagram of monoids indexed by J. The limit of F in the category of monoids comes with canonical projection maps to each F(j). Each projection is a monoid homomorphism, and the family of projections forms a cone.
Русский
Пусть F — диаграмма моноидов по индексному множеству J. Лимит этой диаграммы в категории моноидов снабжается каноническими отображениями на каждый F(j). Каждое такое проекционное отображение является гомоморфизмом моноидов, и множество таких проекций образует конус.
LaTeX
$$$\forall j,\; limitπMonoidHom(F,j):\; (Types.Small.limitCone(F\, forget MonCat)).pt \to_* (F\, forget MonCat).obj j$$$
Lean4
/-- `limit.π (F ⋙ forget MonCat) j` as a `MonoidHom`. -/
@[to_additive /-- `limit.π (F ⋙ forget AddMonCat) j` as an `AddMonoidHom`. -/
]
noncomputable def limitπMonoidHom (j : J) :
(Types.Small.limitCone.{v, u} (F ⋙ forget MonCat.{u})).pt →* ((F ⋙ forget MonCat.{u}).obj j)
where
toFun := (Types.Small.limitCone.{v, u} (F ⋙ forget MonCat.{u})).π.app j
map_one' := by
simp only [Types.Small.limitCone_pt, Types.Small.limitCone_π_app, equivShrink_symm_one]
rfl
map_mul' _
_ := by
simp only [Types.Small.limitCone_pt, Types.Small.limitCone_π_app, equivShrink_symm_mul]
rfl
