Isolating a minimal prime among finitely many

Let I be an ideal in a commutative semiring with finitely many minimal primes over it. For a minimal prime P over I, the intersection of the other minimal primes is not contained in P, so it has an element g ∉ P. Every prime q over I not containing g contains some minimal prime over I, which must be P. Geometrically, when I = ⊥, the basic open set D(g) of Spec A is a nonempty open subset of the irreducible component V(P) meeting no other irreducible component. This reduces statements about a single irreducible component to statements about a localization A[1/g].

Main results

• Ideal.exists_notMem_forall_le_of_mem_minimalPrimes: for a minimal prime P over an ideal with finitely many minimal primes, there is g ∉ P such that every prime over that ideal not containing g contains P.

theorem Ideal.exists_notMem_forall_le_of_mem_minimalPrimes {A : Type u_1} [CommSemiring A] (I : Ideal A) (hfin : I.minimalPrimes.Finite) {P : Ideal A} (hP : P ∈ I.minimalPrimes) : ∃ g ∉ P, ∀ (q : Ideal A), q.IsPrime → I ≤ q → g ∉ q → P ≤ q

Let P be a minimal prime over an ideal I with finitely many minimal primes. Then there is an element g ∉ P such that every prime q over I with g ∉ q contains P.