Products of pairwise non-associated primes: divisibility, minimal primes, radicality

Pure commutative algebra behind the ideal sheaf of a simple normal crossings divisor, on the analytic side (Hironaka/Manifold/Snc/NormalCrossings.lean, Snc/Dictionary.lean, Snc/Bundled.lean) and on the algebraic side (Hironaka/Resolution/Algebraic/Snc/DictionaryBoundary.lean, Hironaka/Resolution/Algebraic/Kol07/UnionIdealInvertible.lean): a germ vanishing on each of finitely many coordinate hyperplanes through a point is divisible by each coordinate, and the coordinates are pairwise non-associated prime elements of the regular local ring 𝒪_{M,a}, so the germ is divisible by their product (prod_dvd_of_prime_of_not_dvd); the minimal primes of the principal ideal of the product are exactly the principal ideals of the factors (minimalPrimes_span_prod, mem_minimalPrimes_span_prod); the ideal is radical (isRadical_span_prod); a product of two ideals of a commutative ring is the unit ideal iff both are (Ideal.mul_ne_top_iff).

This is the algebra of Hironaka's definition of normal crossings — "the ideal of each irreducible component of E is generated by one of the z_i" [Hir64, Definition 2] — iterated over the components; the statements themselves are standard and not in the sources.

theorem Ideal.mul_ne_top_iff {R : Type u_1} [CommRing R] (I J : Ideal R) : I * J ≠ ⊤ ↔ I ≠ ⊤ ∨ J ≠ ⊤

A product of two ideals of a commutative ring is the unit ideal iff both are.

theorem IsLocalRing.prod_dvd_of_prime_of_not_dvd {R : Type u_1} [CommRing R] {ι : Type u_2} (s : Finset ι) (f : ι → R) (hp : ∀ i ∈ s, Prime (f i)) (hnd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ¬f i ∣ f j) {z : R} (hz : ∀ i ∈ s, f i ∣ z) : ∏ i ∈ s, f i ∣ z

In a commutative ring, if finitely many prime elements, none dividing another, each divide z, then their product divides z (the iteration of "each z_i" in [Hir64, Definition 2]).

theorem IsLocalRing.minimalPrimes_span_prod {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {p : ι → R} (hp : ∀ i ∈ s, Prime (p i)) {P : Ideal R} (hP : P ∈ (Ideal.span {∏ i ∈ s, p i}).minimalPrimes) : ∃ i ∈ s, P = Ideal.span {p i}

A minimal prime over the principal ideal generated by a product of prime elements is generated by one of the factors.

theorem IsLocalRing.mem_minimalPrimes_span_prod {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {p : ι → R} (hp : ∀ i ∈ s, Prime (p i)) (hnd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ¬p i ∣ p j) {j : ι} (hj : j ∈ s) : Ideal.span {p j} ∈ (Ideal.span {∏ i ∈ s, p i}).minimalPrimes

Each factor of a product of pairwise non-associated prime elements generates a minimal prime of the principal ideal of the product.

theorem IsLocalRing.isRadical_span_prod {R : Type u_1} [CommRing R] {ι : Type u_2} {s : Finset ι} {p : ι → R} (hp : ∀ i ∈ s, Prime (p i)) (hnd : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → ¬p i ∣ p j) : (Ideal.span {∏ i ∈ s, p i}).IsRadical

The principal ideal generated by a product of pairwise non-associated prime elements is radical.