forget_createsLimitsOfSize — Mathlib

English

The forgetful functor forget_CommGrpCat creates all limits (of all sizes).

Русский

Функтор забывания forget_CommGrpCat порождает все пределы (любой размерности).

LaTeX

$$$\\text{forget}_{CommGrpCat}\\;\\text{CreatesLimitsOfSize}$$$

Lean4

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

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