forget_preservesLimitsOfSize — Mathlib

English

The forgetful functor forget GrpCat preserves limits of all sizes.

Русский

Забывающий функтор GrpCat сохраняет пределы всех размерах.

LaTeX

$$$ \mathrm{PreservesLimitsOfSize}(\mathrm{forget GrpCat}) $$$

Lean4

/-- The forgetful functor from groups to types preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of types. -/
@[to_additive (relevant_arg := 100) /-- The forgetful functor from additive groups to types preserves all limits.

    This means the underlying type of a limit can be computed as a limit in the category of types. -/
    ]
instance forget_preservesLimitsOfSize : PreservesLimitsOfSize.{w, v} (forget GrpCat.{u}) :=
  inferInstance

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