sheaf

Mathlib.Geometry.RingedSpace.SheafedSpace

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.SheafedSpace.sheaf

Lean4

/-- Extract the `sheaf C (X : Top)` from a `SheafedSpace C`. -/
def sheaf (X : SheafedSpace C) : Sheaf C (X : TopCat) :=
  ⟨X.presheaf, X.IsSheaf⟩

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

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

Разделы

Аффилиация

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