coyonedaFunctor_preservesLimits — Mathlib

English

The coyoneda functor preserves limits: coyoneda_preservesLimits asserts that the functor coyoneda preserves limits.

Русский

Функтор койонеда сохраняет пределы: coyoneda_preservesLimits утверждает сохранение пределов функтором койонеда.

LaTeX

$$$\\mathrm{PreservesLimits}\\, (\\mathrm{coyoneda})$$$

Lean4

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

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