PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain
theorem PrimeSpectrum.exists_primeSpectrum_prod_le_and_ne_bot_of_domain :
∀ {A : Type u} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsNoetherianRing A],
¬IsField A →
∀ {I : Ideal A},
I ≠ ⊥ →
∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I ∧ (Multiset.map PrimeSpectrum.asIdeal Z).prod ≠ ⊥
In a Noetherian integral domain which is not a field, every non-zero ideal contains a non-zero product of prime ideals. More specifically, given any type `A` that is a commutative ring, an integral domain, and a Noetherian ring, and is not a field, for any ideal `I` of `A` that is not the zero ideal, there exists a multiset `Z` of prime spectrums such that the product of ideals associated with the prime spectrums in `Z` is contained within `I` and is not the zero ideal. This theorem is a formalization of Lemma 3 from Samuel's algebraic geometry studies, as stated in section 3.3.
More concisely: In a Noetherian integral domain that is not a field, every non-zero ideal contains a product of non-zero prime ideals.
|
PrimeSpectrum.exists_primeSpectrum_prod_le
theorem PrimeSpectrum.exists_primeSpectrum_prod_le :
∀ (R : Type u) [inst : CommRing R] [inst_1 : IsNoetherianRing R] (I : Ideal R),
∃ Z, (Multiset.map PrimeSpectrum.asIdeal Z).prod ≤ I
This theorem states that in any Noetherian ring, every ideal can be expressed as a subset of the product of a multiset of prime ideals. More specifically, for any commutative ring that is also a Noetherian ring, and for any ideal within that ring, there exists a multiset of prime spectra (which are converted to prime ideals using the `PrimeSpectrum.asIdeal` function) such that the product of this multiset is a subset of or equal to the original ideal. This ties into the fundamental theory of Noetherian rings and the structure of their ideals.
More concisely: In any Noetherian ring, every ideal is contained in the product of a multiset of prime ideals.
|