Commit 2023-08-07 04:16 472450d0

feat: heterogenize TensorProduct.congr and friends (#6035) The summary is that this PR:

• generalizes a handful of results to non-commutative algebras (simply by moving them to an earlier section)
• adds heterogenous versions of map, congr, mapBilinear, homTensorHom, leftComm, tensorTensorTensorComm
• generalizes lcurry, uncurry, and assoc to take an extra algebra, such that the As in the two different places can separately be replaced with R The punchline here is really:

def tensorTensorTensorComm :
  (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) :=

which is valuable for a base change / tensor product of bilinear forms when instantiated as

(M ⊗[R] N) ⊗[A] (Dual A M ⊗[R] Dual R N)
  ≃ₗ[A]
(M ⊗[A] Dual A M) ⊗[R] (N ⊗[R] Dual R N)

It would not surprise me if it's possible to introduce a third ring into tensorTensorTensorComm, but for now I'd prefer to assume that for that particular definition, two rings is enough for anybody! Unfortunately, this was not the case for lcurry, uncurry, and assoc, which really do need to work over three rings so that the As in the two different places can separately be replaced with R; both permutations are needed in the construction of tensorTensorTensorComm, and it seemed preferable to not have a plethora of primed variants. I make no claim that the pile of IsScalarTower and SMulCommClass arguments here are in any sense optimal, besides the fact they specifically enable the use-case I have for the base change of bilinear forms.