Commit 2023-08-07 04:16 472450d0
View on Github →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
, andassoc
to take an extra algebra, such that theA
s in the two different places can separately be replaced withR
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 A
s 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.