yoneda_preservesLimits — Mathlib

English

The Yoneda embedding yoneda.obj X preserves limits of any diagram, i.e., it takes limits in Cᵒᵖ to limits in Type.

Русский

Отображение Yoneda сохраняет пределы любых диаграмм, переводя пределы в Cᵒᵖ к пределам в Type.

LaTeX

$$$\\forall X:\\, C,\\; \\mathrm{PreservesLimits}(\\mathrm{yoneda.obj} X)$$$

Lean4

/-- The yoneda embedding `yoneda.obj X : Cᵒᵖ ⥤ Type v` for `X : C` preserves limits. -/
instance yoneda_preservesLimits (X : C) : PreservesLimitsOfSize.{t, w} (yoneda.obj X) where

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