forget_preservesLimits — Mathlib

English

The forgetful functor GrpCat → Type preserves all limits; in particular, the underlying set of a limit is the limit of the underlying sets.

Русский

Функтор забывания GrpCat → Type сохраняет все пределы; в частности, множество предела является пределом множеств.

LaTeX

$$$ \mathrm{PreservesLimits}(\text{forget GrpCat}) $$$

Lean4

@[to_additive]
instance forget_preservesLimits : PreservesLimits (forget GrpCat.{u}) :=
  GrpCat.forget_preservesLimitsOfSize.{u, u}

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