[Merged by Bors] - chore: unify LocalizedModule and OreLocalization#31862
[Merged by Bors] - chore: unify LocalizedModule and OreLocalization#31862erdOne wants to merge 20 commits intoleanprover-community:masterfrom
LocalizedModule and OreLocalization#31862Conversation
PR summary 88c480406bImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 1499 | -8 | backwards compatibility flags |
| 1471 | -8 | privateInPublic flags |
| 50 | -1 | adaptation notes |
Current commit cb5af88568
Reference commit 88c480406b
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
!bench |
|
Benchmark results for 34b2fa7 against b7543c7 are in! @chrisflav Major changes (6)
Minor changes (11)
|
|
Here are the benchmark results for commit 34b2fa7. Benchmark Metric Change
================================================================
- ~Mathlib.AlgebraicGeometry.AffineSpace instructions 84.2%
- ~Mathlib.AlgebraicGeometry.Modules.Tilde instructions 21.7%
+ ~Mathlib.AlgebraicGeometry.Restrict instructions -33.0%
- ~Mathlib.GroupTheory.DivisibleHull instructions 25.7%
- ~Mathlib.RingTheory.NormalClosure instructions 9.5% |
2 files, Instructions +7.0⬝10⁹
3 files, Instructions +6.0⬝10⁹
3 files, Instructions +5.0⬝10⁹
5 files, Instructions +3.0⬝10⁹
8 files, Instructions +2.0⬝10⁹
15 files, Instructions +1.0⬝10⁹
3 files, Instructions -2.0⬝10⁹
|
| /-- The ring homomorphism from `R` to `R[S⁻¹]`, mapping `r : R` to the fraction `r /ₒ 1`. -/ | ||
| @[simps!] | ||
| def numeratorRingHom : R →+* R[S⁻¹] where | ||
| abbrev numeratorRingHom : R →+* R[S⁻¹] where |
There was a problem hiding this comment.
Why is this now an abbrev? And also in the other places?
There was a problem hiding this comment.
Because this is in the algebra instance and it needs to be reducibly equal.
| {U : (Opens (PrimeSpectrum.Top R))ᵒᵖ} (x : U.unop) | ||
| (r : (Spec.structureSheaf R).val.obj U) | ||
| (m : Localizations M ↑x) : | ||
| r • m = (by exact r.1 x : Localization.AtPrime _) • m := rfl |
There was a problem hiding this comment.
This looks bad, what is going on here?
There was a problem hiding this comment.
Some bad defeq abuse. We are getting rid of this file anyways.
| private def smul' (r₁ : R) (s₁ : S) (r₂ : X) (s₂ : S) : X[S⁻¹] := | ||
| private abbrev smul' (r₁ : R) (s₁ : S) (r₂ : X) (s₂ : S) : X[S⁻¹] := | ||
| oreNum r₁ s₂ • r₂ /ₒ (oreDenom r₁ s₂ * s₁) |
There was a problem hiding this comment.
My experiments confirm that the abbrevs in this file are the cause of the massive slowdown in AffineSpace (which makes sense, because this affects the construction of Spec).
I understand that these changes are required to make the checks work at reducible transparency, but I am not sure this is worth it.
There was a problem hiding this comment.
I think things should be solved by making the operations on structure sheaf irreducible, which I will try after the refactor of it.
There was a problem hiding this comment.
But having these declarations be globally reducibly, will also have other undesired performance effects. These should never be unfolded outside of the basic API files. Maybe we can use the module system to our advantage here?
There was a problem hiding this comment.
But to remember the fact that the two instances are defeq we always need to unfold them.
There was a problem hiding this comment.
So we would have to unify the definitions itself.
There was a problem hiding this comment.
Do you mean to unify the instances? As I said I don't think there is an easy way to do so. I could experiment on some generalization of OreSet but I don't think this is a necessity of this PR. To be precise, I expect that generality also comes with its own performance hit and I am not sure if it is worth it or not and we would only know if it gives a net improvement with this PR merged already. OTOH this PR is needed to progress and I would argue we would want to merge it even if there are significant performance regressions.
|
!bench |
|
Benchmark results for 0239558 against b7543c7 are in! @erdOne Major changes (6)
Minor changes (11)
|
|
Here are the benchmark results for commit 0239558. Benchmark Metric Change
================================================================
- ~Mathlib.AlgebraicGeometry.AffineSpace instructions 84.2%
- ~Mathlib.AlgebraicGeometry.Modules.Tilde instructions 21.7%
+ ~Mathlib.AlgebraicGeometry.Restrict instructions -32.9%
- ~Mathlib.GroupTheory.DivisibleHull instructions 25.7%
- ~Mathlib.RingTheory.NormalClosure instructions 9.6% |
2 files, Instructions +7.0⬝10⁹
3 files, Instructions +6.0⬝10⁹
3 files, Instructions +5.0⬝10⁹
2 files, Instructions +4.0⬝10⁹
4 files, Instructions +3.0⬝10⁹
8 files, Instructions +2.0⬝10⁹
15 files, Instructions +1.0⬝10⁹
|
|
This PR causes quite a performance regression. The reason is that some of the components that go into the construction of the ring structure on The reason why these components need to be All in all, I think this PR is a major improvement over the status quo and we should be able to recover from this performance regression when the refactor is complete. So, thanks! |
|
Why |
|
I didn't know there was a difference. Should I be using |
|
I don't know if |
|
Cursory look says it's just for the compile but I probably shouldn't be trusted given the constraints I'm working under |
mattrobball
left a comment
There was a problem hiding this comment.
The whole dependence on Algebra for localization seems strange.
Ideally we can seal OreLocalization after things are designed correctly. But I am not sure if this possible.
| abbrev _root_.LocalizedModule : Type max u v := | ||
| OreLocalization S M | ||
|
|
||
| example {R} [CommSemiring R] (S : Submonoid R) : Localization S = LocalizedModule S R := by |
There was a problem hiding this comment.
Let's move this to a test.
There was a problem hiding this comment.
I have added a test file. But these example are not tests but to showcase to the reader of this file that this defeq is holds by design, and that there are potential defeq diamonds so if one wants to find lemmas about the operations they should also look into the results about Localization. Hence I have kept them in this file as well.
There was a problem hiding this comment.
It should be a comment if in the file itself. Unless the behavior is independent of the import choices (almost nothing), it needs to succeed with full imports if you care about it.
Please remove these.
There was a problem hiding this comment.
I understand your point of having a test file so I added it, but I don't understand the reason of removing the examples. They are illustrative examples to have. Comments are strictly worse as people cannot easily inspect the type of the mentioned declarations nor can they jump to the definition. Comments are also more prone to be out of sync with the actual declaration names.
There was a problem hiding this comment.
Unless the behavior is independent of the import choices (almost nothing), it needs to succeed with full imports if you care about it.
Does this mean that I should switch to import Mathlib in the test file?
There was a problem hiding this comment.
example's create extra burden for linter authors for example. When there is nothing in the environment to look for, how do I make sure the example conforms or at least doesn't mess things up.
Would you mind expanding on this? I am failing to understand this, probably because I don't have a clue how linters work. What does linter look for in the environment? To what should the example conform? How are examples different from regular lemmas in this regard?
I don't see the value of them intramodule in any dimension to be honest.
To me they are just type-checked comments with infoview and they serve the same purposes as comments.
When do you want the defeq to hold? If for all users, then import Mathlib
Yes. I'll change this later.
There was a problem hiding this comment.
Can you sell me on the value for your workflow?
There was a problem hiding this comment.
Are you advocating for removing the example keyword from Lean? Or should it only be used in test files? No burden for linter authors if they're in test files?
There was a problem hiding this comment.
Can you sell me on the value for your workflow?
So when I see a comment like "The multiplication on the localized module.
Note that this gives a diamond with the instance on R[S⁻¹] (which does not require commutativity),
but is defeq to it under with_reducible_and_instances.", I don't have an algorithm to find where the other instance on R[S⁻¹] is, and I have no info what the other instance requires as inputs etc. But if it is included in an example below, I can just inspect the type of it in the info view and find the definition of it very easily.
There was a problem hiding this comment.
I think it's valuable for certain purposes like demonstration or unit tests. In production code, it is less valuable. I don't think it should be removed.
| def r (a b : M × S) : Prop := | ||
| ∃ u : S, u • b.2 • a.1 = u • a.2 • b.1 | ||
|
|
||
| lemma oreEqv_eq_r : (OreLocalization.oreEqv S M).r = r S M := by |
There was a problem hiding this comment.
Why not make this the setoid?
There was a problem hiding this comment.
OreLocalization is indeed defined as the quotient of the setoid of OreLocalization.oreEqv.
There was a problem hiding this comment.
Remind me why r exists again. On mobile so can't explore
There was a problem hiding this comment.
r used to be the relation defining LocalizedModule but we are switching to OreLocalization.oreEqv in this PR.
| simp only [one_mul, smul_smul, ← mul_assoc] } | ||
| simp only [one_mul, smul_smul, ← mul_assoc, mul_right_comm] } | ||
|
|
||
| example : OreLocalization.instMonoid = LocalizedModule.instMonoid (A := R) (S := S) := by |
There was a problem hiding this comment.
Let's put this in a test.
| See https://github.com/leanprover-community/mathlib4/pull/25671 for an approach to generalize this | ||
| but it requires right `R` actions on `R`-algebras. | ||
| -/ | ||
| protected def mul {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} |
There was a problem hiding this comment.
I find it strange we ever talk about Mul in something named module.
There was a problem hiding this comment.
This is probably just unfortunate naming of LocalizedModule but when the module is an algebra then the LocalizedModule is also an algebra.
| mk a₁ s₁ * mk a₂ s₂ = mk (a₁ * a₂) (s₁ * s₂) := by rw [mk_mul_mk', mul_comm s₁ s₂] | ||
|
|
||
| instance {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} : | ||
| instance (priority := 900) {A : Type*} [Semiring A] [Algebra R A] {S : Submonoid R} : |
There was a problem hiding this comment.
We prefer the OreLocalization.instSemiring instance on Localization S. I have added a comment explaining this.
| change _ • mk _ _ = mk _ _ * mk _ _ | ||
| rw [mk_mul_mk, smul'_mk, Algebra.smul_def, one_mul] | ||
|
|
||
| example : (algebra' : Algebra R (LocalizedModule S R)) = OreLocalization.instAlgebra := by |
There was a problem hiding this comment.
Again it should be a test.
| lemma smul_section_apply (r : R) (U : Opens (PrimeSpectrum.Top R)) | ||
| (s : (tildeInModuleCat M).obj (op U)) (x : U) : | ||
| (r • s).1 x = r • (s.1 x) := rfl | ||
| (r • s).1 x = r • (s.1 x) := |
There was a problem hiding this comment.
Can this be salvaged later?
There was a problem hiding this comment.
I'm not sure. Probably yes. But this isn't a really useful defeq to have.
|
This pull request has conflicts, please merge |
|
Please turn the bors d+ |
|
✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with |
…lib4 into erd1/ore-module4
|
bors merge |
We redefine `LocalizedModule` to be an abbrev of `OreLocalization S M` so that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particular `ModuleCat.tilde` and `Spec.structureSheaf`. Some of the declarations are switched to reducible to avoid diamonds. This causes a significant performance regression, most notabaly in `Mathlib/AlgebraicGeometry/AffineSpace.lean`. We shall investigate if there are ways to improve performances. For example by introducing typeclasses to unify the two constructions on this and `LocalizedModule`, or by marking some downstream constructions (e.g. `Spec.structureSheaf`) as irreducible.
|
Pull request successfully merged into master. Build succeeded: |
LocalizedModule and OreLocalizationLocalizedModule and OreLocalization
…unity#31862) We redefine `LocalizedModule` to be an abbrev of `OreLocalization S M` so that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particular `ModuleCat.tilde` and `Spec.structureSheaf`. Some of the declarations are switched to reducible to avoid diamonds. This causes a significant performance regression, most notabaly in `Mathlib/AlgebraicGeometry/AffineSpace.lean`. We shall investigate if there are ways to improve performances. For example by introducing typeclasses to unify the two constructions on this and `LocalizedModule`, or by marking some downstream constructions (e.g. `Spec.structureSheaf`) as irreducible.
…unity#31862) We redefine `LocalizedModule` to be an abbrev of `OreLocalization S M` so that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particular `ModuleCat.tilde` and `Spec.structureSheaf`. Some of the declarations are switched to reducible to avoid diamonds. This causes a significant performance regression, most notabaly in `Mathlib/AlgebraicGeometry/AffineSpace.lean`. We shall investigate if there are ways to improve performances. For example by introducing typeclasses to unify the two constructions on this and `LocalizedModule`, or by marking some downstream constructions (e.g. `Spec.structureSheaf`) as irreducible.
We redefine
LocalizedModuleto be an abbrev ofOreLocalization S Mso that localization of a ring and localization of a module is now defeq. This is very useful to unify downstream constructions, in particularModuleCat.tildeandSpec.structureSheaf.Some of the declarations are switched to reducible to avoid diamonds.
This causes a significant performance regression, most notabaly in
Mathlib/AlgebraicGeometry/AffineSpace.lean.We shall investigate if there are ways to improve performances. For example by introducing
typeclasses to unify the two constructions on this and
LocalizedModule, or by marking somedownstream constructions (e.g.
Spec.structureSheaf) as irreducible.