Minimal primes under going down

If an R-algebra S satisfies going down, then the contraction of a minimal prime of S is a minimal prime of R: a strictly smaller prime of R would lift, by going down, to a strictly smaller prime of S. Flat algebras satisfy going down (Algebra.HasGoingDown.of_flat), so geometrically a flat morphism of affine schemes sends generic points of irreducible components to generic points of irreducible components.

Main results

• Ideal.under_mem_minimalPrimes: under going down, minimal primes contract to minimal primes.

theorem Ideal.under_mem_minimalPrimes {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.HasGoingDown R S] {Q : Ideal S} (hQ : Q ∈ minimalPrimes S) : under R Q ∈ minimalPrimes R

If S satisfies going down over R, then the contraction of a minimal prime of S is a minimal prime of R.