-
Notifications
You must be signed in to change notification settings - Fork 156
CommAlgebras as CommRingHoms #1145
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Conversation
8a04a53 to
e997ccd
Compare
5abb334 to
72226e5
Compare
|
I did some random benchmarking (this PR is not really about type checking speed, but I made some changes while I rewrote code). In summary, the two modules in CommAlgebra with comparable content have signficantly lower type checking times now, while there is no significant change for the modules in Ring and CommRing I checked. |
e3cae56 to
04adbaf
Compare
e62abab to
bc7a252
Compare
8abc7a4 to
7917b85
Compare
e56d3a6 to
ef5ab32
Compare
416c279 to
7c1e4d1
Compare
|
I explained this PR to Evan, whom I didn't ask to read through all of it. He believes me that it makes sense and I will just merge it now. |
03b784f to
3caf5b5
Compare
This is an experiment to see if algebras work better when they are defined as homomorphisms of rings.
UPDATE: The experiment worked. It is however the case, that it is quite some work to port everything to the new definition of
CommAlgebraand not all of this work is done in this PR. I think it should be merged anyway, since it is already very big and it should already be useful to others.