yonedaFunctor_preservesLimits — Mathlib

English

The Yoneda functor universally preserves limits; i.e., the functor yoneda from C to (Cᵒᵖ ⥤ Type) preserves all limits in its target.

Русский

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

LaTeX

$$$\\mathrm{PreservesLimitsOfSize}(\\mathrm{yoneda})$$$

Lean4

instance yonedaFunctor_preservesLimits : PreservesLimitsOfSize.{t, w} (@yoneda C _) :=
  by
  apply preservesLimits_of_evaluation
  intro K
  change PreservesLimitsOfSize (coyoneda.obj K)
  infer_instance

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