Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus

∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X] (s : Set ↑(X.presheaf.obj (Opposite.op ⊤))),
  ⇑X.isoSpec.hom '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

If X is affine, the image of the zero locus of global sections of X under X.isoSpec is the zero locus in terms of the prime spectrum of Γ(X, ⊤).

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffine