Algebra.TensorProduct.[left|right]Algebra

Stream: mathlib4

[Kevin Buzzard]

Our definitions of docs#Algebra.TensorProduct.leftAlgebra and docs#Algebra.TensorProduct.rightAlgebra have significantly diverged (one has three types, the other has 4; one has semirings; one has unnecessary commutativity assumptions). There is a genuine asymmetry here in that both can't be instances (or else the $A$-algebra structure on $A\otimes_RA$ is ambiguous) and it looks like the instance has had more love than the non-instance. Is there a reason not to fix this up? It's handy to have rightAlgebra as a local instance occasionally but I've run into an example in FLT where not everything is a CommRing so rightAlgebra as it stands won't apply. If there are no objections I might take this on as a tube problem.

[Eric Wieser]

I think one cause of friction here is that literature tends to write a base-change by tensoring with the ring on the right, while mathlib does so by tensoring on the left. A lot of the time you can resolve this by just writing things backwards. Of course, it's very plausible that you genuinely need both versions.

[Kevin Buzzard]

My actual problem is indeed that I want to stick to the literature. If I start asking number theorists questions like "what do you think about $\mathbb{A}_F\otimes_FD$ rather than $D\otimes_F\mathbb{A}_F$ then I might get the answer "are you sure your system is fit for purpose if this is an issue?".

[Kevin Buzzard]

What's ridiculous is that the only reason I want this tensor product to be an $\mathbb{A}_F$-module is so that I can use my module topology work to put a topology on the tensor product ($\mathbb{A}_F$ has a topology, $D$ does not) and then get typeclass inference to automatically show that it's a topological ring. I could just do all of this by hand but am currently convinced that what I'm doing is "the right way to do it".

[Kevin Buzzard]

Weakening rightAlgebra so that it didn't assume A was commutative would be enough for me, this would certainly be easier (indeed it's already in FLT) but I was contemplating upstreaming it to mathlib and that was when I realised the asymmetry.

[Eric Wieser]

Given we have rightAlgebra in mathlib anyway it probably does makes sense to generalize it (perhaps not adding the fourth ring), but I suspect you're making work for yourself here that a notation flip would avoid

[Kevin Buzzard]

Yes, it is pretty dismal. I don't think I'm going to be able to flip the notation. You can try it yourself by editing the definition on the Shimura variety Wikipedia page to $Sh_K(G,X)=K\backslash G(\mathbb{A}_f) \times X / G(\mathbb{Q})$ and arguing that this is more convenient.

[Eric Wieser]

I don't even understand the operator precedence in that notation, let alone where the tensor product is hiding!

[Kevin Buzzard]

$G(A):= (D\otimes A)^\times$ in our case. Not that all this matters; my point is that this convention is set in stone :-(

[Eric Wieser]

Oh, your point was not that I'll end up in a mess, but that Wikipedia will say no

[Kevin Buzzard]

Right. Because why go against the literature? Shimura made a random decision in the 60s and now we're stuck with it but it's everywhere.

[Eric Wieser]

I feel like there are plenty of places in mathlib where someone made a decision in the literature but we did something different because it generalized better / used more existing machinery

[Eric Wieser]

Eric Wieser said:

it's very plausible that you genuinely need both versions.

To be clear, this case would arise if you need both one of the actions that comes from $A$ and one of the actions that come from $D$, and the action on $D$ can't factor through any actions you have on $A$.

[Kevin Buzzard]

My D is noncommutative so I'll never need the algebra structure, I'll just need the ring hom, which is unproblematic.

[Antoine Chambert-Loir]

A long time ago, I wrote in detail the derivation of the “natural” action of $\mathrm{GL}(2,\mathbf R)^+$ on the upper half plane, not as the standard formula, but just wondering what acts on what, and getting the resulting formula. This is a mess. If $V$ is a real plane, eg $V=\mathbf C$, then $\mathrm{GL}(2,\mathbf R)$ acts on the set $$\matchcal B$$ of bases of $V$ on the right, etc. At the end, the action of $\left(\begin{smallmatrix}a & b \\ c & d \end{smallmatrix}\right)$ on $\tau\in\mathfrak h$ is given by $\left(\begin{smallmatrix}a & b \\ c & d \end{smallmatrix}\right)\cdot \tau = \frac{c+d\tau}{a+b\tau}$.

[Antoine Chambert-Loir]

To get the standard one, you need to conjugate the given action by $w=\left(\begin{smallmatrix}0 & 1 \\ 1 & 0 \end{smallmatrix}\right)$.

[Antoine Chambert-Loir]

(Regarding the convention for base change, I'm pretty sure most mathematical texts have incoherent conventions, and in any case, most authors are incoherent from one text to another. So mathlib can fix one, I see no harm in that.)

[Oliver Nash]

I might be missing the point above, but it seems to me there is also a "natural" way to get the usual $\frac{az + b}{cz + d}$ formula.

If we start with $\mathbb{CP}^1$ but also endow it with the real structure coming from complex conjugation then its automorphism group $PSL(2, \mathbb{C})$ has a distinguished $PSL(2, \mathbb{R})$ which has three orbits. The boring one, fixed by the real structure, is $\mathbb{RP}^1$, but the other two, interchanged by the real structure, are interesting. If we consider the orbit containing $[i, 1]$ then we get the usual $\frac{az + b}{cz + d}$ formula, right?