forget₂Mon_preservesFilteredColimits

English

There is a noncomputable instance that forget₂ GrpCat MonCat preserves filtered colimits; i.e., filtered colimits in GrpCat, when viewed as MonCat, are preserved.

Русский

Существует невычислимый экземпляр, что забыть GrpCat до MonCat сохраняет фильтрованные колимиты; то есть фильтрованные колимиты в GrpCat сохраняются при рассмотрении как MonCat.

LaTeX

$$$$ \mathrm{PreservesFilteredColimits}(\mathrm{forget}_{\mathsf{GrpCat},\mathsf{MonCat}}) $$$$

Lean4

@[to_additive forget₂AddMon_preservesFilteredColimits]
noncomputable instance forget₂Mon_preservesFilteredColimits :
    PreservesFilteredColimits.{u} (forget₂ GrpCat.{u} MonCat.{u}) where
  preserves_filtered_colimits x hx1
    _ :=
    letI : Category.{u, u} x := hx1
    ⟨fun {F} =>
      preservesColimit_of_preserves_colimit_cocone (colimitCoconeIsColimit.{u, u} F)
        (MonCat.FilteredColimits.colimitCoconeIsColimit.{u, u} _)⟩

Похожие утверждения