representable_preservesLimits

Mathlib.CategoryTheory.Limits.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.representable_preservesLimits

English

If F is representable and G is a functor with domain J, then G preserves limits with respect to F.

Русский

Если F представимо и G — функтор, то G сохраняет пределы относительно F.

LaTeX

$$$\\mathrm{PreservesLimit}\\; G\\; F$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru