toRangeSheafify

Mathlib.CategoryTheory.Sites.Subsheaf

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subpresheaf.toRangeSheafify

Lean4

/-- A morphism factors through the sheafification of the image presheaf. -/
@[simps!]
def toRangeSheafify (f : F' ⟶ F) : F' ⟶ ((Subpresheaf.range f).sheafify J).toPresheaf :=
  toRange f ≫ Subpresheaf.homOfLe ((range f).le_sheafify J)

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

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

Разделы

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

Аффилиация

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