Chevalley's theorem

In this file we provide the usual (algebraic) version of Chevalley's theorem. For the proof see Mathlib/RingTheory/Spectrum/Prime/ChevalleyComplexity.lean.

theorem PrimeSpectrum.isConstructible_comap_C {R : Type u_1} [CommRing R] {s : Set (PrimeSpectrum (Polynomial R))} (hs : Topology.IsConstructible s) : Topology.IsConstructible (⇑(comap Polynomial.C) '' s)

theorem PrimeSpectrum.isConstructible_comap_image {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FinitePresentation) {s : Set (PrimeSpectrum S)} (hs : Topology.IsConstructible s) : Topology.IsConstructible (⇑(comap f) '' s)

Chevalley's theorem: If f is of finite presentation, then the image of a constructible set under Spec(f) is constructible.

theorem PrimeSpectrum.isConstructible_range_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : f.FinitePresentation) : Topology.IsConstructible (Set.range ⇑(comap f))

theorem PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] [Algebra.FinitePresentation R S] : IsOpenMap ⇑(comap (algebraMap R S))

Stacks Tag 00I1