Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq

∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (hV : AlgebraicGeometry.IsAffineOpen V) (x : ↥X) (hxU : x ∈ U) (hxV : x ∈ V),
  hU.fromSpecStalk hxU = hV.fromSpecStalk hxV

The morphism from Spec(O_x) to X given by IsAffineOpen.fromSpec does not depend on the affine open neighborhood of x we choose.

Defined in

Mathlib.AlgebraicGeometry.Stalk

Cited by

1 results in Mathlib

Foundations

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