Minimal primes of tensor products

Minimal primes behave well under extension of scalars along a flat algebra. If L is flat over a commutative semiring K, a minimal prime of L ⊗[K] A contracts to a minimal prime of the commutative ring A, because the tensor product is flat over A and satisfies going down.

For an ideal I of a commutative ring A, a minimal prime Q over the extension of I to E ⊗[K] A is the extension of its contraction P whenever E ⊗[K] (A ⧸ P) is a domain. The extension of P is then prime and lies between the extension of I and Q, so minimality forces equality. This applies to components of arbitrary closed subsets as well as to minimal primes of the whole tensor product.

Main results

• Ideal.eq_map_comap_includeRight_of_isDomain: a minimal prime over an extended ideal is extended from its contraction when the tensor product of the contracted quotient is a domain.
• Ideal.comap_includeRight_mem_minimalPrimes: under flat scalar extension, minimal primes of a tensor product contract to minimal primes of the right factor.

theorem Ideal.eq_map_comap_includeRight_of_isDomain {K : Type u_1} [CommRing K] {A : Type u_2} [CommRing A] [Algebra K A] {E : Type u_3} [CommRing E] [Algebra K E] (Q : Ideal (TensorProduct K E A)) {I : Ideal A} (hQ : Q ∈ (map Algebra.TensorProduct.includeRight I).minimalPrimes) (hdom : IsDomain (TensorProduct K E (A ⧸ comap Algebra.TensorProduct.includeRight Q))) : Q = map Algebra.TensorProduct.includeRight (comap Algebra.TensorProduct.includeRight Q)

A minimal prime Q over the extension of an ideal of A to E ⊗[K] A is the extension of its contraction P from A to E ⊗[K] A, provided E ⊗[K] (A ⧸ P) is a domain.

theorem Ideal.comap_includeRight_mem_minimalPrimes {K : Type u_1} [CommSemiring K] {A : Type u_2} [CommRing A] [Algebra K A] {L : Type u_3} [CommRing L] [Algebra K L] [Module.Flat K L] (Q : Ideal (TensorProduct K L A)) (hQ : Q ∈ minimalPrimes (TensorProduct K L A)) : comap Algebra.TensorProduct.includeRight Q ∈ minimalPrimes A

A minimal prime of L ⊗[K] A contracts to a minimal prime of A when L is flat over K: then L ⊗[K] A is flat over A and satisfies going down.