perf: improve instances in AdjoinRoot#7435
Conversation
|
!bench |
|
Here are the benchmark results for commit 6b14acb. Benchmark Metric Change
===================================================
+ ~Mathlib.FieldTheory.Normal instructions -7.1% |
mattrobball
left a comment
There was a problem hiding this comment.
These seem to be upstream issues. Fixing those would probably improve things more broadly.
| instance [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f) := | ||
| Ideal.Quotient.algebra S | ||
| --TODO: add reference to library note in PR #7432 | ||
| { Ideal.Quotient.algebra S with |
There was a problem hiding this comment.
The underlying problem seems to be that Ideal.Quotient.algebra buries SMul under RingHom.comp which (I'm guessing) is more expensive to unify if you just want the smul.
There was a problem hiding this comment.
This statement is not correct. The two signatures are
@Algebra.mk S (AdjoinRoot f) inst_1 CommSemiring.toSemiring (Submodule.Quotient.instSMul' (span {f})) Algebra.toRingHom _ _ : Algebra S (AdjoinRoot f)and, previously,
@Quotient.algebra S R[X] inst_1 commRing algebraOfAlgebra (span {f}) : Algebra S (R[X] ⧸ span {f})You have to unfold algebraOfAlgebra to get access SMul previously and no longer have to do that.
But Algebra.toRingHom buries RingHom under another layer with change. It might be good to include
toRingHom := RingHom.comp _ _ which avoids this.
There was a problem hiding this comment.
I don't see why this would help because Algebra is the only class that has a toRingHom field. It may help, I guess if people are really exploiting this def-eq everywhere, but that would be bad style anyway.
| instance [DistribSMul S R] [IsScalarTower S R R] : DistribSMul S (AdjoinRoot f) := | ||
| Submodule.Quotient.distribSMul' _ | ||
| --TODO: add reference to library note in PR #7432 | ||
| { Submodule.Quotient.distribSMul' _ with |
There was a problem hiding this comment.
distribSMul' uses Function.Surjective which is probably the underlying problem
There was a problem hiding this comment.
I don't think so. For example, the change in #6803 to the group instance made a difference even though the underlying instance on Con was defined nicely. Maybe defining them nicely all the way back also makes a difference.
mattrobball
left a comment
There was a problem hiding this comment.
See if #7459 helps with the DistribMul instance.
| instance [CommSemiring S] [Algebra S R] : Algebra S (AdjoinRoot f) := | ||
| Ideal.Quotient.algebra S | ||
| --TODO: add reference to library note in PR #7432 | ||
| { Ideal.Quotient.algebra S with |
There was a problem hiding this comment.
This statement is not correct. The two signatures are
@Algebra.mk S (AdjoinRoot f) inst_1 CommSemiring.toSemiring (Submodule.Quotient.instSMul' (span {f})) Algebra.toRingHom _ _ : Algebra S (AdjoinRoot f)and, previously,
@Quotient.algebra S R[X] inst_1 commRing algebraOfAlgebra (span {f}) : Algebra S (R[X] ⧸ span {f})You have to unfold algebraOfAlgebra to get access SMul previously and no longer have to do that.
But Algebra.toRingHom buries RingHom under another layer with change. It might be good to include
toRingHom := RingHom.comp _ _ which avoids this.
|
!bench |
|
Here are the benchmark results for commit 907cc35. |
|
|
Uh oh!
There was an error while loading. Please reload this page.