[Merged by Bors] - chore(Algebra/Algebra/Defs): add an algebraMap field to Algebra instead of extending RingHom

[edegeltje]

as proposed on zulip

---

[github-actions]

PR summary 118b2fe326

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

-+-+ algebra'
-+-+-+ algebra

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

Decrease in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
4816	-1	porting notes

Current commit 118b2fe326
Reference commit 7466910ec3

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[kbuzzard]

!bench

[leanprover-bot]

Here are the benchmark results for commit 2890b28.
The entire run failed.
Found no significant differences.

[kbuzzard]

!bench

[leanprover-bot]

Here are the benchmark results for commit e85e968.
The entire run failed.
Found no significant differences.

[kbuzzard]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6fb5948.
The entire run failed.
Found no significant differences.

[kbuzzard]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6fb5948.
The entire run failed.
Found no significant differences.

[kbuzzard]

I should say that I have no particular suspicion that mathlib will compile more quickly or more slowly, but I thought it was worth benchmarking giving that we're changing such a fundamental definition and that typeclass inference can sometimes be very delicate. I hadn't realised that there were problems with the benchmarking bot.

[kbuzzard]

!bench

[leanprover-bot]

Here are the benchmark results for commit 02cc50f.
There were no significant changes against commit 7466910.

[github-actions]

File	Instructions	%
build	-4.214⬝10⁹	(+0.00%)
Mathlib.RingTheory.Kaehler.CotangentComplex	+1.883⬝10⁹	(+0.67%)
Mathlib.RingTheory.Kaehler.JacobiZariski	-2.397⬝10⁹	(-0.28%)
CI run

[kbuzzard]

maintainer delegate

I am not an expert in the finer parts of typeclass inference so I'd like another maintainer to sign off on this, but it's great to see that this change decreases build time a little and the diff looks fine to me (github is making much more of a meal of it than it could do).

[kbuzzard]

Is the Module.compHom thing on line 66 still necessary?

[erdOne]

I believe it is. There's Algebra.compHom that can replace the whole def now but this is probably not in scope of the PR.

[edegeltje]

PR at #20708

[github-actions]

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

[Vierkantor]

bors d+

[mathlib-bors]

✌️ edegeltje can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[edegeltje]

bors r+

[edegeltje]

bors r+

[mathlib-bors]

Already running a review

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style