chore: refactor Algebra.TensorProduct.rightAlgebra

[kbuzzard]

(was #25481 ; now re-opened from a fork).

The declaration Algebra.TensorProduct.rightAlgebra makes A ⊗[R] B into a B-algebra (here R is a CommSemiring, A is a Semiring and an R-algebra, and B is a CommSemiring and an R-algebra). It is not an instance because if A = B it causes a diamond. However in the many cases where A isn't B, it can occasionally be useful.

However one could imagine that in the many cases where an R-module M also isn't B, it might occasionally be useful to make M ⊗[R] B into a B-module (and indeed I am finding this in FLT). With the current definition of Algebra.TensorProduct.rightAlgebra this is difficult to do without causing diamonds in the case when M happens to be an R-algebra.

One fix for this is just to redefine Algebra.TensorProduct.rightAlgebra so that the smul field is

smul b ab := TensorProduct.comm _ _ _ (b • (TensorProduct.comm _ _ _ ab))

i.e. literally "swap the product around, use mathlib's instance making B ⊗[R] A into a B-algebra, and then swap back". Then the same definition can be used to make M ⊗[R] B into a B-module and on the odd occasion where this point of view is useful, there is no diamond. This is what we do in this PR. After adding one simp lemma there is no breakage at all in mathlib. Furthermore, for those who have observed that we want to build on this algebra instance sometimes and, for example, add instances of the form "if M is finite over R then M ⊗[R] B is finite over B" -- these instances are really easy to add now with this new definition, because you simply pull back the analogous finite left module instance along the isomorphism M ⊗[R] B = B ⊗[R] M. Examples (from FLT, where the right action is put in a scope):

scoped instance [Module.Finite R M] : Module.Finite A (M ⊗[R] A) :=
  Module.Finite.equiv (Module.TensorProduct.comm R A M)

scoped instance [Module.Free R M] : Module.Free A (M ⊗[R] A) :=
  Module.Free.of_equiv (Module.TensorProduct.comm R A M)

---

---

[github-actions]

PR summary cd84f88c8e

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit cd84f88c8e
Reference commit b8219087d9

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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]

Comments from #25481 :

Me: The reason all the changes are there is that I define smul at the same time as defining the Algebra instance. The smul isn't an instance so I avoided making it. Another approach is to define rightAlgebra_smul : SMul A (A ⊗[R] B), make it locally an instance, make some API for it (some simp lemmas e.g. smul_def), and then tidy the proofs up a bit. But I was a bit concerned about making simp lemmas which only fired for a scalar multiplication which wasn't an instance so I decided to mess with simp as little as possible. I did add one simp lemma for rightAlgebra though; this was to make a proof which was added in #22933 compile again. I could remove the simp lemma and fix the #22933 proof in a different way (probably with another change) or I could alternatively add more simp lemmas about these not-usually-instances. I wasn't sure which way to go so we now have some kind of half-way house.

Me (after the old PR was delegated to me -- but I didn't merge): @eric-wieser this has been delegated to me but I am reluctant to merge because IIRC we had a discussion about this on Zulip and you were not enthusiastic about the change: your specific comment is here #mathlib4 > Right actions on tensor products (again) @ 💬 and I don't want to be the intentional causer of trouble. I do not understand the issues well enough to understand your comment properly.

[kbuzzard]

I've just reread the long thread #mathlib4 > Right actions on tensor products (again) @ 💬 again and what it seems to be is a lot of stuff which is irrelevant to this PR, and then Andrew suggesting this approach, and then Eric saying "I think pulling through comm is going to cause trouble in an eventual bimodule world, where you can't commute without also moving to MulOpposite".