heads-up: right algebras/modules incoming

Stream: FLT

[Kevin Buzzard]

I find it very frustrating that $A\otimes B$ is not a $B$-algebra. Sometimes you want it to be an $A$-algebra and a $B$-algebra at the same time. Mathlib won't have this instance because of the objection "what if $A=B$?" but my response to that (mimicking Pooh's to Piglet) is "what if $A\not=B$?".

FLT#616 makes a new scope: open scope TensorProduct.RightActions. With this scope open the following miracles occur. Let $R$ be a commutative ring and let $B$ be a commutative $R$-algebra.

1) If $A$ is an $R$-algebra then $A\otimes_RB$ is a $B$-algebra.
2) If $M$ is an $R$-module then $M\otimes_RB$ is a $B$-module.
3) If $M$ is finite, resp. free, then $M\otimes_RB$ is finite, resp. free.
4) More controversially, if $B$ has a topology then $M\otimes_RB$ gets the $B$-module topology. In particular if $A$ is a finite $R$-algebra and $B$ is a topological ring then $A\otimes_RB$ is automatically a topological ring.

So be warned, when you open this scope, that's currently what you get. If (4) turns out to be annoying then we can roll it back later by putting it into another scope.

This broke a lot of code! It's mostly fixed in FLT#616, which I'm currently working on.

I'm really sorry about the very nice-looking PRs piling up; I have some stuff which I want to get done before Monday so I've had to focus on my own work rather than reviewing other people's PRsand definitely I'm not leaving them until Monday just so I can show off how many PRs people are making to the FLT project in my talk. I am (genuinely!) also very busy this weekend; I'm playing dots and boxes at a science festival for 6 hours straight on both Sat and Sun and then going to Cambridge straight afterwards.