Tensor product over noncommutative ring

Stream: Is there code for X?

[Gareth Ma]

Is there tensor product over noncommutative rings? TensorProduct requires [CommRing R] and so does ModuleCat.monoidalCategory

[Kevin Buzzard]

Can you be more precise? What are you tensoring and what isn't commutative? There are three types involved here

[Gareth Ma]

I want $M \otimes_R N$ where $M$ is a left $R$-module and $N$ is a right $R$-module, and $R$ isn't necessarily commutative, which should be an abelian group

[Gareth Ma]

I don't know how "right $R$-module" works in Lean either, I'm not familiar with the algebra side of Mathlib at all, hence the question :0

[Kevin Buzzard]

My understanding is that if R isn't commutative then to make a right R-module you just make it a left R^op module. If you import mathlib and open TensorProduct does it Just Work? Sorry, not at a computer right now

[Gareth Ma]

I see, but then R still isn't commutative so the TensorProduct doesn't work

[Gareth Ma]

#docs4 TensorProduct

[Gareth Ma]

how do you use this again

[Gareth Ma]

docs4#TensorProduct

[Gareth Ma]

It requires

noncomputable def TensorProduct (R : Type u_1) [CommSemiring R] (M : Type u_4) (N : Type u_5) [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] :
Type (max u_4 u_5)

[Kevin Buzzard]

docs#TensorProduct

[Kevin Buzzard]

Huh, do we really not have this?

[Gareth Ma]

:sad: i want to tensor over $k[G]$ for non-commutative $G$

[Gareth Ma]

seems like a massive task to work on as well...

[Gareth Ma]

Oh there is a draft PR #8638. @Junyan Xu hello :eyes:

[Kevin Buzzard]

Oh I disagree -- sounds like a nice project! Just copy the commutative case and do 150 lines and then stop. You'll make the world a better place!

[Kevin Buzzard]

You can just start by making NonCommTensorProduct and then do the refactor of TensorProduct later

[Gareth Ma]

That's true, I guess the work is just copying the commutative case and mess around with stuff. But since there's a draft PR I'll wait for the (co)author and see if they're working on it :eyes:

[Joël Riou]

Gareth Ma said:

:sad: i want to tensor over $k[G]$ for non-commutative $G$

Just to be sure, do you want to take the tensor product over k[G] (which is going to be a k-vector space), or take the tensor product over k and define a linear action of G? (These two are not the same. A certain formulation of the latter is in the file Mathlib.RepresentationTheory.Action.Monoidal.)

[Gareth Ma]

It's the former, for e.g. induced representations

[Kevin Buzzard]

If all you want is induced representations then you can just make them as something like functions from G to V (an H-rep) satisfying f(hg)=h.f(g) or whatever.

[Gareth Ma]

Oh yeah, I don't think defining induced rep with this tensor product is "natural" anyways, but you want it as a theorem

[Gareth Ma]

that the (Rep.induced something something).\rho.asModule is isomorphic to the tensor product construction

[Junyan Xu]

The nice thing about defining induced rep as a tensor product is that you get Frobenius reciprocity as a special case of docs#ModuleCat.extendRestrictScalarsAdj, which is immediate from uncurryEquiv here. This adjunction has been a major motivation of my draft PR.

Currently, TensorProduct uses R-action on both factors and require them be Modules, but the left factor should really be a R^mop-Module by mathematical convention. For a commutative ring R, R^mop and R are isomorphic rings by the identity map, and a R^mop-Module is the same as an R-Module. But for a noncommutative ring R, a R^mop-MulAction will not give rise to a R-MulAction.

In #8638 I changed TensorProduct to require R^mop-Module on left factor and generalized results when possible, and I plan to define the "commutative tensor product" that takes two R-Modules in another file, by making the left R-Module a R^mop-Module using commutativity. Note that this can't be a global instance, because there are existing R- and R^mop-Module instances on R itself defined for [Semiring R], which are propositionally but not definitionally equal for commutative R, because one is left multiplication and the other is right multiplication.

The current state of #8638 is mostly my experiment to see which results generalize to the noncommutative setting and in which ways they generalize. The type of many declarations are changed (e.g. R-LinearMap is changed to R^mop-LinearMap), which will be disruptive downstream in Mathlib. I think a better approach is to create a new file TensorProduct.General, and put the generalized declarations under the TensorProduct.General namespace. In the current file TensorProduct.Basic, we don't add or remove declarations, but change the constructions / proofs to use the generalized declarations when possible. I might try to implement this this weekend.

(Remark: If we relax [Module] to [SMul] in TensorProduct, we could avoid changing one of the R to R^mop, because a R^mop-SMul does give rise to a R-SMul, and if you make this a local/temporary instance, you can "define the general/noncommutative tensor product in terms of the existing/commutative tensor product", but I think this approach is mathematically dubious.)

[Eric Wieser]

There was a very long thread about this in the past, which culminated in a refactor of Algebra to imply actions on both sides (so that we don't need separate types for tensor products of noncommutative algebras). The PR was mostly lost to the porting tide.

[Yuyang Zhao]

(See #maths > left vs right modules in tensor products and #mathlib4 > Noncommutative ring things )

[Junyan Xu]

Here's a new idea: similar to semilinear maps, we can generalize TensorProduct to take a R-module M and a S-module N together with a RingHom σ from S to R^dma (defeq to R^mop with same ring structure). In this setting, the tensor-Hom adjunction becomes the correspondence between M ⊗[σ] N →+ P and N →ₛₗ[σ] M →+ P. One can take σ to be RingEquiv.toOpposite if R=S is commutative, or RingEquiv.opOp if R is S^mop. This generalized TensorProduct isn't quite symmetric in the two factors, and RingHomInvPair can be used to express the necessary condition for TensorProduct.comm ...

[Eric Wieser]

Is there any precedent for doing this with σ = star?

[Johan Commelin]

I think there is precedent when \sigma = Frob.