corepresentable_preservesLimits — Mathlib

English

If a functor F: C → Type is corepresentable, then F preserves limits of all small diagrams (i.e., F is limit-preserving on shapes of a chosen size).

Русский

Если функтор F: C → Type является ко-представимым, то F сохраняет пределы всех малых диаграмм (то есть F сохраняет пределы по формам заданного размера).

LaTeX

$$$\\bigl(\\exists X\\in \\mathrm{Obj}(C)\\, F \\cong \\mathrm{Hom}_C(X,-)\\bigr) \\Rightarrow \\operatorname{PreservesLimitsOfSize}(F).$$$

Lean4

instance corepresentable_preservesLimits : PreservesLimitsOfSize.{t, w} F where

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