forget_createsLimitsOfSize — Mathlib

English

The forgetful functor forget MonCat preserves/creates limits of all sizes; i.e., limits can be computed in the underlying category of sets with the induced monoid structure.

Русский

Забывающий функтор forget MonCat сохраняет/создаёт пределы любого размера; пределы можно вычислять в базовой категории множеств с индуцированной моноидной структурой.

LaTeX

$$$\text{CreatesLimitsOfSize}\ (\mathrm{forget}\ \mathrm{MonCat})$$$

Lean4

/-- The forgetful functor from commutative monoids to types preserves all limits. -/
@[to_additive /-- The forgetful functor from commutative additive monoids to types preserves all limits. -/
    ]
noncomputable instance forget_createsLimitsOfSize : CreatesLimitsOfSize.{w, v} (forget MonCat.{u}) where
  CreatesLimitsOfShape := inferInstance

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