preservesLimits_forget — Mathlib

English

The forgetful functor preserves limits, mediated by a natural isomorphism with the evaluation at the unit object in the action equivalence.

Русский

Функтор забывания сохраняет пределы, посредствам натуральной изоморфности с оценкой по единице действия.

LaTeX

$$preservesLimits_forget (V) (G) : PreservesLimits (forget V G)$$

Lean4

noncomputable instance preservesLimits_forget [HasLimits V] : PreservesLimits (forget V G) :=
  Limits.preservesLimits_of_natIso (Action.functorCategoryEquivalenceCompEvaluation V G)

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