Theorems · Definition · algebraic geometry

AlgebraicGeometry.IsAffineOpen.fromSpecStalk

{X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} →
    AlgebraicGeometry.IsAffineOpen U → {x : ↥X} → x ∈ U → (AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ X)

A morphism from Spec(O_x) to X, which is defined with the help of an affine open neighborhood U of x.

Defined in

Mathlib.AlgebraicGeometry.Stalk

Cited by

5 results in Mathlib

Foundations

Depth 145 from the axioms · uses propext, Classical.choice, Quot.sound