Algebraic geometry

StructurePrime spectrum#

The prime spectrum of a commutative (semi)ring R is the type of all prime ideals of R.

It is naturally endowed with a topology (the Zariski topology), and a sheaf of commutative rings (see Mathlib/AlgebraicGeometry/StructureSheaf.lean). It is a fundamental building block in algebraic geometry.

PrimeSpectrum.{u_1} (R : Type u_1) [CommSemiring R] : Type u_1
Sources
MathlibPrimeSpectrum
Uses 2 · Used by 2
Statement usesNatural number · Prime ideal
Used byZariski topology · Krull's principal ideal theorem

InstanceZariski topology#

The Zariski topology on the prime spectrum of a commutative (semi)ring is defined via the closed sets of the topology: they are exactly those sets that are the zero locus of a subset of the ring.

PrimeSpectrum.zariskiTopology.{u} {R : Type u} [CommSemiring R] : TopologicalSpace (PrimeSpectrum R)
Sources
MathlibPrimeSpectrum.zariskiTopology
Uses 3 · Used by 2
Statement usesModule · Prime spectrum · Topological space
Used byScheme · Going-up and going-down theorems

StructureLocally ringed space#

A LocallyRingedSpace is a topological space equipped with a sheaf of commutative rings such that all the stalks are local rings.

A morphism of locally ringed spaces is a morphism of ringed spaces such that the morphisms induced on stalks are local ring homomorphisms.

AlgebraicGeometry.LocallyRingedSpace.{u} : Type (u + 1)
Sources
MathlibAlgebraicGeometry.LocallyRingedSpace
Uses 6 · Used by 1
Statement usesLocal ring · Natural number · Ring morphism · Sheafed space · Small category · The category of topological spaces
Used byScheme

StructureScheme#

We define Scheme as an X : LocallyRingedSpace, along with a proof that every point has an open neighbourhood U so that the restriction of X to U is isomorphic, as a locally ringed space, to Spec.toLocallyRingedSpace.obj (op R) for some R : CommRingCat.

AlgebraicGeometry.Scheme.{u_1} : Type (u_1 + 1)
Sources
MathlibAlgebraicGeometry.Scheme
Uses 9
Statement usesAlgebra of endomorphisms of a vector space · Grothendieck topology · Induced topology · Integer · Isomorphism · Locally ringed space · Open map · Yoneda embedding · Zariski topology

TheoremNullstellensatz#

Main statement of the Nullstellensatz

MvPolynomial.vanishingIdeal_zeroLocus_eq_radical.{u_1, u_2, u_3} {k : Type u_1} {K : Type u_2}
  [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ]
  (I : Ideal (MvPolynomial σ k)) :
  MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I) = I.radical
Sources
MathlibMvPolynomial.vanishingIdeal_zeroLocus_eq_radical
Uses 12
Statement usesAlgebraically closed field · Associative algebra over a commutative ring · Ideal of a commutative ring · Polynomial in several indeterminates
Proof usesAlgebraic extension · Field of fractions of an integral domain · Finite-dimensionality · Local ring · Localization · Prime ideal · Quotient space (Fundamentals) · Sum of subspaces

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.