corepresentable_preservesLimit

Mathlib.CategoryTheory.Limits.Yoneda

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

English

If F is corepresentable, then PreservesLimit G F holds for any G.

Русский

Если F ко-представимо, то для любого G выполняется сохранение предела F.

LaTeX

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

Lean4

instance corepresentable_preservesLimit (G : J ⥤ C) : PreservesLimit G F :=
  preservesLimit_of_natIso _ F.coreprW

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

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

Разделы

Аффилиация

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