English
If J is a small filtered category and F : J ⥤ CommSemiRingCat, then forgetting the commutative semiring structure preserves filtered colimits; i.e., the colimit computed in CommSemiRingCat, after forgetful functor, agrees with the colimit computed in SemiRingCat.
Русский
Если J — маленькая фильтрованная категория и F : J ⥤ CommSemiRingCat, то при забывании структуры коммутативного полугリングa колимит сохраняется; т. е. колимит в CommSemiRingCat, после забывания, эквивалентен колимиту в SemiRingCat.
LaTeX
$$$ \\mathrm{forget}_{CommSemiRingCat\\to SemiRingCat}\\big( \\operatorname{Colim}_J F \\big) \\cong \\operatorname{Colim}_J \\big( \\, F \\big) \\circ \\mathrm{forget}$$$
Lean4
instance forget₂SemiRing_preservesFilteredColimits : PreservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat.{u})
where
preserves_filtered_colimits
{J hJ1 _} :=
letI : Category J := hJ1
{
preservesColimit := fun {F} =>
preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
(SemiRingCat.FilteredColimits.colimitCoconeIsColimit (F ⋙ forget₂ CommSemiRingCat SemiRingCat.{u})) }
