AffineZariskiSite

Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.AffineZariskiSite

Lean4

/-- `X.AffineZariskiSite` is the small affine Zariski site of `X`, whose elements are affine open
sets of `X`, and whose arrows are basic open sets `D(f) ⟶ U` for any `f : Γ(X, U)`.

Note that this differs from the definition on stacks project where the arrows in the small affine
Zariski site are arbitrary inclusions.
-/
def AffineZariskiSite (X : Scheme.{u}) : Type u :=
  { U : X.Opens // IsAffineOpen U }

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

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

Разделы

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

Аффилиация

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