instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits

Mathlib.Topology.Sheaves.Skyscraper

URI: https://scilib.ai/kg/mathlib#instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits

English

There is a right adjoint to skyscraperSheafFunctor when HasColimits holds in C.

Русский

Существет правый адъюнкт к skyscraperSheafFunctor при условии HasColimits в C.

LaTeX

$$$(skyscraperSheafFunctor p_0).IsRightAdjoint$$$

Lean4

instance [HasColimits C] : (skyscraperSheafFunctor p₀ : C ⥤ Sheaf C X).IsRightAdjoint :=
  (stalkSkyscraperSheafAdjunction _).isRightAdjoint

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

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

Разделы

Аффилиация

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