refactor: introduce Ideal.IsTwoSided class for quotients of noncommutative rings
#17930
Conversation
alreadydone
commented
Oct 18, 2024
•
alreadydone
commented
- depends on: [Merged by Bors] - refactor: generalize Mul of Submodule and SMul of Ideal on Submodule to noncommutative setting #17708
…to noncommutative setting
PR summary a180e6862fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type |
|---|---|---|
| 196 | -2 | adaptation notes |
| 199 | -4 | disabled simpNF lints |
Current commit a180e6862f
Reference commit b1178f181d
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).
mathlib4-dependent-issues-bot
added
the
blocked-by-other-PR
alreadydone
changed the title
Ideal.IsTwoSided class for generalization to noncommutative settingIdeal.IsTwoSided class for quotients of noncommutative rings
leanprover-community-bot-assistant
added
the
merge-conflict
|
Here are the benchmark results for commit 49dbf9e. Benchmark Metric Change
=====================================================================
+ ~Mathlib.FieldTheory.SeparableDegree instructions -5.3%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.1%
- ~Mathlib.RingTheory.AdjoinRoot instructions 15.8%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.3%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 17.4%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 20.0% |
|
!bench |
|
Here are the benchmark results for commit 53313de. Benchmark Metric Change
=====================================================================
+ ~Mathlib.FieldTheory.SeparableDegree instructions -5.3%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.1%
- ~Mathlib.RingTheory.AdjoinRoot instructions 15.8%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.3%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 17.4%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 20.0% |
…ng one" This reverts commit a3ff84c.
|
!bench |
|
Here are the benchmark results for commit 08e995d. Benchmark Metric Change
=====================================================================
+ ~Mathlib.FieldTheory.SeparableDegree instructions -5.3%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.1%
- ~Mathlib.RingTheory.AdjoinRoot instructions 18.4%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.6%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 21.2%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 21.3% |
…e CommRing one"" This reverts commit 08e995d.
|
!bench |
|
Here are the benchmark results for commit 00e44e4. |
|
!bench |
|
Here are the benchmark results for commit 0f6f5ef. Benchmark Metric Change
=====================================================================
- ~Mathlib.FieldTheory.LinearDisjoint instructions 7.5%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.1%
- ~Mathlib.RingTheory.AdjoinRoot instructions 15.8%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.3%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 17.4%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 20.1% |
leanprover-community-bot-assistant
added
the
merge-conflict
|
@alreadydone How about this for a proposal to move this PR forwards.
I've just opened |
|
Thanks for the proposal!
The diff isn't that intimidating if you look at the declarations diff: the only instance removed is the |
There was a problem hiding this comment.
Once the merge conflicts are fixed we can benchmark this PR and have an actual look at the slowdowns. It seems to me that they are actually not too bad, and perhaps just the price we have to pay for doing algebra properly rather than the way we're currently doing it.
However I would like to raise the possibility that instead of (I : Ideal R) [IsTwoSided I] we could just do (I : TwoSidedIdeal R). (which already exists). Why are we not doing down the TwoSidedIdeal route? Sorry if this has all been covered before, I'm just getting up to speed with it all.
| #adaptation_note | ||
| /-- | ||
| On nightly-2024-11-12, we had to add `nolint simpNF` to the following lemma, | ||
| as otherwise we get a deterministic timeout in typeclass inference. | ||
| This should be investigated. | ||
| -/ | ||
| @[simp, nolint simpNF] |
There was a problem hiding this comment.
| #adaptation_note | |
| /-- | |
| On nightly-2024-11-12, we had to add `nolint simpNF` to the following lemma, | |
| as otherwise we get a deterministic timeout in typeclass inference. | |
| This should be investigated. | |
| -/ | |
| @[simp, nolint simpNF] | |
| @[simp] |
Is this comment still true? I don't seem to get any error or lint failure in the file itself (with #lint) if I remove the nolint. Same for the adaptation note just below.
There was a problem hiding this comment.
I tested the effect around here and it seems negligible. Let me do another test after merging master.
There was a problem hiding this comment.
After removing nolint simpNF, build went down from 0.19% to 0.18%, but lint went up from 0.13% to 0.15%. Is this worth it? Linting tends to cost more time due to lack of parallelization, I heard.
| @@ -223,14 +231,14 @@ lemma quotientInfToPiQuotient_surj [Finite ι] {I : ι → Ideal R} | |||
|
|
|||
| /-- **Chinese Remainder Theorem**. Eisenbud Ex.2.6. | |||
| Similar to Atiyah-Macdonald 1.10 and Stacks 00DT -/ | |||
| noncomputable def quotientInfRingEquivPiQuotient [Finite ι] (f : ι → Ideal R) | |||
| noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R) | |||
There was a problem hiding this comment.
Is it still similar to Stacks 00DT? If so then maybe add a @[stacks] tag?
There was a problem hiding this comment.
Yes, but it's only the isomorphism, not the equality between infimum and product of ideals. The closest thing to the equality in mathlib is probably Ideal.iInf_span_singleton, which should probably be generalized ...
| noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R) | |
| @[stacks 00DT "isomorphism in (1)"] | |
| noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R) |
There was a problem hiding this comment.
However I would like to raise the possibility that instead of
(I : Ideal R) [IsTwoSided I]we could just do(I : TwoSidedIdeal R). (which already exists). Why are we not doing down theTwoSidedIdealroute? Sorry if this has all been covered before, I'm just getting up to speed with it all.
I explained reasons to prefer IsTwoSided here. Here are my latest thoughts: if using TwoSidedIdeal for quotients,
(1) in order to unify the commutative case and noncommutative case, you would like to switch all quotients by Ideals to quotients by TwoSidedIdeals. In the process you need to duplicate a lot of APIs about Ideals to TwoSidedIdeals; it helps to think all that you need for this exact declaration quotientInfRingEquivPiQuotient. Such duplication is mostly meaningless as most operations on Ideal and TwoSidedIdeal agree, and you'd be better served adding instances registering that these operations preserve two-sidedness (which is done in this PR).
(2) Even you are to maintain the two parallel APIs, it's inevitable that you sometimes need to convert between the two types, either by coercion or explicit invocation of .toIdeal/.toTwoSidedIdeal, which is not good news for readability. This is further complicated by the fact TwoSidedIdeal is a RingCon, carrying the data of a binary predicate rather than a unary one, which means that going from TwoSidedIdeal to Ideal and back can't be defeq. This can be alleviated by changing TwoSidedIdeal to be the bundle of Ideal and IsTwoSided, which is arguably the right thing to do, since in a semiring a RingCon and a TwoSidedIdeal aren't the same thing.
(3) When I said "all quotients by Ideals" I actually meant only those where we use the ring structure; since Ideals are in particular Submodules, it's still valid to consider the quotient module. But the ring also has an algebra hence a module structure, and one may needs to compare both at times. If the two quotients are defeq you could treat them as the same (which is a bit of defeq abuse but prevalent when dealing with e.g. CoeSort of Submodule/Subalgebra), but if not (see (2)), you have to use an explicit isomorphism. I think it's better not to create more ways of talking about the same thing.
alreadydone
removed
the
merge-conflict
|
!bench |
|
Here are the benchmark results for commit 80a2ec8. Benchmark Metric Change
=======================================================================
- ~Mathlib.FieldTheory.LinearDisjoint instructions 8.1%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.7%
- ~Mathlib.RingTheory.AdjoinRoot instructions 16.0%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.4%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 17.7%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 20.0%
- ~Mathlib.Topology.Algebra.Valued.LocallyCompact instructions 16.4% |
2 files, Instructions +10.0⬝10⁹
2 files, Instructions +8.0⬝10⁹
3 files, Instructions +7.0⬝10⁹
2 files, Instructions +4.0⬝10⁹
4 files, Instructions +3.0⬝10⁹
6 files, Instructions +2.0⬝10⁹
20 files, Instructions +1.0⬝10⁹
|
|
!bench |
|
Here are the benchmark results for commit a180e68. Benchmark Metric Change
=======================================================================
- ~Mathlib.FieldTheory.LinearDisjoint instructions 8.1%
- ~Mathlib.LinearAlgebra.Semisimple instructions 24.9%
- ~Mathlib.RingTheory.AdjoinRoot instructions 16.0%
- ~Mathlib.RingTheory.Ideal.Quotient.Operations instructions 25.4%
- ~Mathlib.RingTheory.Jacobson.Ring instructions 17.7%
- ~Mathlib.RingTheory.Polynomial.Quotient instructions 20.0%
- ~Mathlib.Topology.Algebra.Valued.LocallyCompact instructions 16.1% |
2 files, Instructions +10.0⬝10⁹
2 files, Instructions +8.0⬝10⁹
3 files, Instructions +7.0⬝10⁹
3 files, Instructions +4.0⬝10⁹
4 files, Instructions +3.0⬝10⁹
6 files, Instructions +2.0⬝10⁹
18 files, Instructions +1.0⬝10⁹
2 files, Instructions -2.0⬝10⁹
|
leanprover-community-bot-assistant
added
the
merge-conflict
|
Gained merge conflicts again from #20518. Should I fix them now? |
