theorem dense_constructible_contains_basicOpen {R : Type u_1} [CommRing R] [IsDomain R] {s : Set (PrimeSpectrum R)} (hs : Topology.IsConstructible s) (hd : Dense s) : ∃ (b : R), b ≠ 0 ∧ ↑(PrimeSpectrum.basicOpen b) ⊆ s

A dense constructible subset of the spectrum of an integral domain contains a nonempty basic open subset D(b).

theorem denseRange_comap_of_injective {B : Type u_1} {A : Type u_2} [CommRing B] [CommRing A] [IsDomain B] [Algebra B A] (hf : Function.Injective ⇑(algebraMap B A)) : DenseRange (PrimeSpectrum.comap (algebraMap B A))

If the algebra map B → A is injective and B is a domain, then the induced map of spectra has dense image.

theorem chevalley_algebraic_core (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (b : B), b ≠ 0 ∧ ↑(PrimeSpectrum.basicOpen b) ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A))

Algebraic core of Chevalley's theorem: for a dominant morphism of finite type between integral Noetherian rings, the image of Spec A → Spec B contains a nonempty basic open.

theorem chevalley_algebraic_core_primes (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (b : B), b ≠ 0 ∧ ∀ (𝔮 : Ideal B) [𝔮.IsPrime], b ∉ 𝔮 → ∃ (𝔭 : Ideal A), 𝔭.IsPrime ∧ Ideal.comap (algebraMap B A) 𝔭 = 𝔮

Reformulation of chevalley_algebraic_core in terms of prime ideals: every prime not containing some fixed nonzero b ∈ B is the contraction of a prime of A.

theorem chevalley_image_contains_dense_open (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsDomain B] [IsDomain A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] (hf : Function.Injective ⇑(algebraMap B A)) : ∃ (U : TopologicalSpace.Opens (PrimeSpectrum B)), (↑U).Nonempty ∧ Dense ↑U ∧ ↑U ⊆ Set.range (PrimeSpectrum.comap (algebraMap B A))

Topological repackaging: the image of a dominant finite-type morphism contains a nonempty dense open subset (part of Chevalley's theorem).

theorem chevalley_constructible (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] : Topology.IsConstructible (Set.range (PrimeSpectrum.comap (algebraMap B A)))

Chevalley's theorem: the image of a morphism of finite type between Noetherian schemes is constructible.

theorem chevalley_open_map_of_flat (B : Type u_1) (A : Type u_2) [CommRing B] [CommRing A] [IsNoetherianRing B] [Algebra B A] [Algebra.FiniteType B A] [Module.Flat B A] : IsOpenMap (PrimeSpectrum.comap (algebraMap B A))

A flat morphism of finite type between Noetherian schemes is an open map (consequence of going-down and finite presentation).