constantSheaf

Mathlib.CategoryTheory.Sites.ConstantSheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.constantSheaf

Lean4

/-- The functor which maps an object of `D` to the constant sheaf at that object, i.e. the
sheafification of the constant presheaf.
-/
noncomputable def constantSheaf : D ⥤ Sheaf J D :=
  Functor.const Cᵒᵖ ⋙ (presheafToSheaf J D)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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