toPresheafedSpace

Mathlib.AlgebraicGeometry.Spec

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Spec.toPresheafedSpace

Lean4

/-- Spec, as a contravariant functor from commutative rings to presheafed spaces.
-/
def toPresheafedSpace : CommRingCat.{u}ᵒᵖ ⥤ PresheafedSpace CommRingCat :=
  Spec.toSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace

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

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

Разделы

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

Аффилиация

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