-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(ring_theory/noetherian): add two lemmas on products of prime ideals #5013
Conversation
Merge branch 'master' into prime_prod
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Nice results! I extracted a pair of lemmas that can shorten the proofs considerably. I also commented with some tips for how to code slicker proofs, but overall it was already pleasant to read.
src/ring_theory/noetherian.lean
Outdated
obtain ⟨x, y, hx, hy, h_xy⟩ : ∃ (x y : R), x ∉ M ∧ y ∉ M ∧ x * y ∈ M, | ||
{ rw [ideal.is_prime, not_and] at h_not_prM, | ||
specialize h_not_prM h_not_topM, | ||
rw not_forall at h_not_prM, | ||
cases h_not_prM with x hx, | ||
rw not_forall at hx, | ||
cases hx with y hxy, | ||
use [x, y], finish }, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Golfing:
obtain ⟨x, y, hxy, hx, hy⟩ : ∃ (x y : R), x * y ∈ M ∧ x ∉ M ∧ y ∉ M,
{ rw [ideal.is_prime, not_and] at h_not_prM,
specialize h_not_prM h_not_topM,
push_neg at h_not_prM,
assumption },
src/ring_theory/noetherian.lean
Outdated
begin | ||
have hA_nont : nontrivial A, | ||
apply is_integral_domain.to_nontrivial (integral_domain.to_is_integral_domain A), | ||
by_cases h_topI : I < ⊤, |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I prefer to deal with the easy case first:
by_cases h_topI : I = ⊤,
{ rcases h_topI with rfl,
obtain ⟨p_id, h_nzp, h_pp⟩ : ∃ (p : ideal A), p ≠ 0 ∧ p.is_prime,
{ apply ring.not_is_field_iff_exists_prime.mp h_fA },
let p : prime_spectrum A := ⟨p_id, h_pp⟩,
use [({p} : multiset (prime_spectrum A)), le_top],
rwa [multiset.map_singleton, multiset.singleton_eq_singleton, multiset.prod_singleton] },
...
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
I have implemented all requested changes with two minor modifications:
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
With these two small tweaks I'm happy. Let's get an independent reviewer too.
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Great, I have implemented these two changes. |
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Johan Commelin <johan@commelin.net>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
…als (#5013) Add two lemmas saying that in a noetherian ring (resp. _integral domain)_ every (_nonzero_) ideal contains a (_nonzero_) product of prime ideals. Co-authored-by: faenuccio <65080144+faenuccio@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
Add two lemmas saying that in a noetherian ring (resp. integral domain) every (nonzero) ideal contains a (nonzero) product of prime ideals.