feat: Define the localization of a fractional ideal at a prime ideal#14237
feat: Define the localization of a fractional ideal at a prime ideal#14237
Conversation
…e basic facts about it.
prime, and prove some basic facts about it.
PR summary f5dca2297eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This PR/issue depends on: |
Vierkantor
left a comment
There was a problem hiding this comment.
Thanks! The results look good, nicely stated and a good coverage of the requirements. I'm still thinking a bit about the proofs, some of them feel like a lot of manual work, but perhaps that's unavoidable with the current state of the library.
| variable {A : Type*} [CommRing A] [IsDomain A] (P : Ideal A) [P.IsPrime] | ||
| variable (I : FractionalIdeal A⁰ (FractionRing A)) (J : FractionalIdeal A⁰ (FractionRing A)) | ||
|
|
||
| local notation "Aₚ" => Localization.AtPrime P | ||
| local notation "K" => FractionRing A | ||
| local notation "hf" => nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ <| | ||
| IsLocalization.injective Aₚ P.primeCompl_le_nonZeroDivisors |
There was a problem hiding this comment.
One thing to remark on here is that the library tends to prefer IsLocalization.AtPrime over Localization.AtPrime and IsFractionRing over FractionRing. It does make everything more verbose, but it helps in cases where we know a specific value for the localization. For example, FractionRing ℤ is not the same thing as ℚ. So you would end up inserting a lot of coercions and isomorphisms to identify the different localizations.
I expect in this case it's okay since we're treating localizedAtPrime as a new construction operating on a pair (Ideal, FractionalIdeal), so we don't need to insert so many explicit isomorphisms. What is your experience with using these results in your follow-up work?
There was a problem hiding this comment.
I wanted to define it in greater generality, but I couldn't find an easy way to get it to work. If I recall correctly, the problem was that K needs to be an Aₚ-algebra, which can't (currently) be inferred when they're defined using IsFractionRing and IsLocalization.
There was a problem hiding this comment.
To answer the other question, the only follow-up work I did with this was the proof of isDedekindDomain ↔ isDedekindDomainDvr linked above. In that specific case, being stuck with FractionRing rather than IsFractionRing didn't cause any problems.
There was a problem hiding this comment.
I wanted to define it in greater generality, but I couldn't find an easy way to get it to work. If I recall correctly, the problem was that
Kneeds to be anAₚ-algebra, which can't (currently) be inferred when they're defined usingIsFractionRingandIsLocalization.
Is the issue that we are missing some instances? Can you switch to the Is point of view and add them, or give some idea about problems which you can't solve using the Is approach?
| use s₂ • i₁ + s₁ • i₂, s₁ * s₂ | ||
| simp only [AddSubmonoid.coe_add, coe_toAddSubmonoid, coe_smul_of_tower, smul_add] | ||
| congr 1 | ||
| · rw [Submonoid.mk_smul, algebra_compatible_smul Aₚ (s₂ : A) (i₁ : K), ← mk_one_eq_algebraMap, | ||
| ← smul_assoc, smul_eq_mul, mk_mul, mul_one, ← mk_mul, mk_self, mul_one] | ||
| · rw [Submonoid.mk_smul, algebra_compatible_smul Aₚ (s₁ : A) (i₂ : K), ← mk_one_eq_algebraMap, | ||
| ← smul_assoc, smul_eq_mul, mk_mul, mul_comm, mul_assoc, ← mk_mul, mk_self, one_mul, mul_one] | ||
| · rintro y _ ⟨i, s, rfl⟩ | ||
| refine Localization.induction_on y (fun ⟨a, s₁⟩ ↦ ⟨a • i, s₁ * s, ?_⟩) | ||
| rw [coe_smul_of_tower, ← smul_assoc, smul_comm, ← smul_assoc] | ||
| nth_rewrite 1 [← mul_one a, ← smul_eq_mul, ← smul_mk] | ||
| rw [smul_assoc a, smul_eq_mul, mk_mul, one_mul] |
There was a problem hiding this comment.
More like a note to self: It feels like all these rewriting steps should be doable in a simpler way. Can we figure out a normal form for these expressions that simp can produce reliably?
There was a problem hiding this comment.
I couldn't figure out a good way to do it. Writing the theorem using mk 1 s • i was already my attempt at using something that could be considered a normal form, but it doesn't want to play nice with the simplifier.
It's possible to extract the first six rewrites (which the two congr subgoals have in common) into a separate lemma. I'm not sure whether the lemma is interesting enough to be worthwhile. That might partly depend on whether we decide to redo this whole file in greater generality with IsLocalization and IsFractionRing.
As an aside, the congr 1 doesn't do anything important -- the proof still works without it. I think it's nice to have it in there for now while we're discussing how to simplify the code, but we could remove it later.
| extended_add K hf I J | ||
|
|
||
| theorem localizedAtPrime_mul : | ||
| (I * J).localizedAtPrime P = (I.localizedAtPrime P) * (J.localizedAtPrime P) := |
There was a problem hiding this comment.
| (I * J).localizedAtPrime P = (I.localizedAtPrime P) * (J.localizedAtPrime P) := | |
| (I * J).localizedAtPrime P = I.localizedAtPrime P * J.localizedAtPrime P := |
and everywhere else
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
Define the localization of a fractional ideal at a prime ideal, and prove some basic properties.
This PR is part 3 out of 4 of a proof of
isDedekindDomain_iff_isDedekindDomainDvr.Part 4 is available here: #14242