Bimodules

Stream: Is there code for X?

[Edison Xie]

Do we have a notation of bimodules? I'm aware that we could use [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] but do we need a def for this? Moreover do we have a category of bimodule? Again I found Bimod in mathlib but this doesn't look quite right because it requires two monoid objects in the category of rings (ℤ-algebras)? Or is it the one I want?

[Yaël Dillies]

No two typeclasses in [AddCommGroup M] [Module R M] [Module S M] [SMulCommClass R S M] talk about the same set of free variables, so there is no way to make it shorter except for some elaboration magic like class abbrev

[Edison Xie]

are you suggesting that we use this way and never have a definition of the category of bimodules? Because I want a way to describe BimoduleHom as a type :-(

[Yaël Dillies]

You asked about a typeclass of the form Bimodule R S M. I am saying this typeclass is SMulCommClass R S M. I haven't said anything about the category of bimodules

[Edison Xie]

Yaël Dillies said:

You asked about a typeclass of the form Bimodule R S M. I am saying this typeclass is SMulCommClass R S M. I haven't said anything about the category of bimodules

Are you suggesting this?

structure BiModuleCat (R S : Type*) [Ring S] [Ring R] where
  carrier : Type*
  [isAddCommGroup : AddCommGroup carrier]
  [isModuleR : Module R carrier]
  [isModuleS : Module S carrier]
  [isCompatible : SMulCommClass R S carrier]

[Eric Wieser]

I don't think Yael was suggesting anything about the category of bimodules

[Eric Wieser]

But that looks reasonable to me

[Eric Wieser]

What are you going to use for the morphisms?

[Edison Xie]

Eric Wieser said:

What are you going to use for the morphisms?

I’m thinking just map_smul for R and S actions?

[Eric Wieser]

So a linear map plus an extra field?

[Kevin Buzzard]

I am completely confused. Isn't an (R,S)-bimodule usually an abelian group with a left action of R and a commuting right action of S? That's not what the above code says.

[Edison Xie]

Kevin Buzzard said:

I am completely confused. Isn't an (R,S)-bimodule usually an abelian group with a left action of R and a commuting right action of S? That's not what the above code says.

I was just following the instructions given in Mathlib/Algebra/Module/Bimodule :smiling_face_with_tear:

[Kevin Buzzard]

But in the module docstring for that file it says

variable (R S M : Type*) [Ring R] [Ring S]
variable [AddCommGroup M] [Module R M] [Module Sᵐᵒᵖ M] [SMulCommClass R Sᵐᵒᵖ M]

which is (correct and) not what you wrote.

[Edison Xie]

But it also said its “preferable” to set things without opposite? I’m confused too… :smiling_face_with_tear:

[Eric Wieser]

Kevin Buzzard said:

the module docstring for that file

Which file?

[Kevin Buzzard]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Bimodule.html

[Kevin Buzzard]

For implementation of API via the tensor product trick I totally agree that we don't need the ops, but if we're defining the category of bimodules then we surely do, otherwise the definition is just wrong.

[Eric Wieser]

'Wrong" or "more general"?

[Eric Wieser]

You could define

structure BiModuleCat' (R S : Type*) [Ring S] [Ring R] where
  carrier : Type*
  [isAddCommGroup : AddCommGroup carrier]
  [isModuleR : Module R carrier]
  [isModuleS : Module S carrier]
  [isCompatible : SMulCommClass R S carrier]

abbrev BiModuleCat (R S : Type*) [Ring S] [Ring R] := BiModuleCat' R Sᵐᵒᵖ

[Eric Wieser]

Probably you'd find most if not all of your results hold in the generality of the primed version

[Eric Wieser]

Of course, if the primed version is totally uninteresting that's not a particularly relevant observation

[Edison Xie]

Kevin Buzzard said:

For implementation of API via the tensor product trick I totally agree that we don't need the ops, but if we're defining the category of bimodules then we surely do, otherwise the definition is just wrong.

persumably we also want BiModuleCat R S equivalent to the ModuleCat of their tensorproduct (later) but yeah I agree that we want the right definition

[Aaron Liu]

Is BiModuleCat' R S not just the same as BiModuleCat R Sᵐᵒᵖ since ᵐᵒᵖ is involutive?

[Eric Wieser]

ᵐᵒᵖ is not definitionally involutive, src#MulOpposite is a one-field structure

[Aaron Liu]

what I meant is, its composition with itself is naturally isomorphic to the identity functor in the category of rings

[Kevin Buzzard]

Eric Wieser said:

'Wrong" or "more general"?

Wrong. That's not the category of (R,S)-bimodules, it's the category of (R,S^{op})-bimodules, so it shouldn't be called BiModuleCat R S.

[Kevin Buzzard]

But just to be clear -- I agree with your abbrev BiModuleCat idea above (although maybe BiModuleOpCat or something would be a better name than BiModuleCat', I am worried we'll confuse mathematicians who are just browsing).

[Kevin Buzzard]

The reason one usually works with BimoduleCat is that there's a "tensor product over S" functor BiModuleCat R S -> BiModuleCat S T -> BiModuleCat R T and this looks quite natural (R acts on the left on M and T acts on the right of N, so both act on $M\otimes_S N$ where $S$ acts on $M$ on the right and on $N$ on the left), whereas doing this with tensor products would involve some some kind of contraction (totally doable, but somehow feels a lot less natural). However we also do something which mathematicians would presumably regard as unnatural when we secretly regard bilinear maps as linear maps to linear maps, and maybe this is just the same sort of thing.