composeAndSheafify

Mathlib.CategoryTheory.Sites.PreservesSheafification

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.composeAndSheafify

Lean4

/-- This is the functor sending a sheaf `X : Sheaf J A` to the sheafification
of `X.val ⋙ F`. -/
noncomputable abbrev composeAndSheafify : Sheaf J A ⥤ Sheaf J B :=
  sheafToPresheaf J A ⋙ (whiskeringRight _ _ _).obj F ⋙ presheafToSheaf J B

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

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

Разделы

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

Аффилиация

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