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) :
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) :
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))
theorem PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field {K : Type u_3} {A : Type u_4} {B : Type u_5} [Field K] [CommRing A] [CommRing B] [Algebra K A] [Algebra K B] :
IsOpenMap (comap (algebraMap A (TensorProduct K A B)))