instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits

Mathlib.Topology.Sheaves.Skyscraper

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

English

There exists a right adjoint to skyscraperPresheafFunctor when HasColimits hold in C.

Русский

Существуют правый адъюнкт к skyscraperPresheafFunctor при условии наличия колимитов в C.

LaTeX

$$$(skyscraperPresheafFunctor p_0).IsRightAdjoint$$$

Lean4

instance [HasColimits C] : (skyscraperPresheafFunctor p₀ : C ⥤ Presheaf C X).IsRightAdjoint :=
  (skyscraperPresheafStalkAdjunction _).isRightAdjoint

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

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

Разделы

Аффилиация

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