## Stream: maths

### Topic: Bimodules

#### Reid Barton (Aug 06 2020 at 13:07):

Does this really work?

#### Reid Barton (Aug 06 2020 at 13:07):

Anyways, wouldn't it be more natural to write right actions on the right?

#### Adam Topaz (Aug 06 2020 at 13:08):

Yes, but since everything is already done for left modules, wouldn't it be more convenient to define a right action as a left action by M\op?

#### Adam Topaz (Aug 06 2020 at 13:09):

Notation can be introduced for a right action, I guess.

#### Reid Barton (Aug 06 2020 at 13:10):

I'm not sure what is more convenient, but maybe that's just lasting scars from opposite

#### Adam Topaz (Aug 06 2020 at 13:11):

I'm thinking something along these lines:

notation a  • :73 m := has_scalar.smul (opposite.op m) a


#### Reid Barton (Aug 06 2020 at 13:20):

Is that the same character as left multiplication?

#### Adam Topaz (Aug 06 2020 at 13:20):

Yeah, is that a problem?

#### Reid Barton (Aug 06 2020 at 13:21):

Would this work for bimodules?

#### Adam Topaz (Aug 06 2020 at 13:21):

Not sure yet. I'll have to try.

#### Reid Barton (Aug 06 2020 at 13:21):

I was imagining we would use some paired characters, like steal the stupid triangle notation perhaps

#### Adam Topaz (Aug 06 2020 at 13:22):

I'm not sure what you're referring to.

#### Reid Barton (Aug 06 2020 at 13:23):

e.g. change smul to ▸ and use ◂ for right multiplication (muls?)

#### Reid Barton (Aug 06 2020 at 13:24):

but of course there's doubtless a large number of other options

#### Reid Barton (Aug 06 2020 at 13:24):

example :one: of a bimodule is R as an (R, R)-bimodule, so I'm having trouble imagining using the same notation for multiplication on both sides

#### Adam Topaz (Aug 06 2020 at 13:25):

This works:

import algebra

class comm_mul_action M N α
[monoid M] [monoid N]
[mul_action M α] [mul_action N α] :=
(commutes {m : M} {n : N} {a : α} : m • n • a = n • m • a)

class biaction M N α [monoid M] [monoid N]
[mul_action M α] [mul_action Nᵒᵖ α] extends comm_mul_action M Nᵒᵖ α

notation a  • :73 m := has_scalar.smul (opposite.op m) a

class bimodule A B M [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] extends biaction A B M

variables (A B M : Type*) [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] [bimodule A B M]
variables (a : A) (b : B) (m : M)

example : a • m • b = a • (m • b) := by rw comm_mul_action.commutes


#### Reid Barton (Aug 06 2020 at 13:27):

(I'm going to move lots of this discussion to topic "bimodules")

#### Reid Barton (Aug 06 2020 at 13:27):

oh wait I can't any more

#### Adam Topaz (Aug 06 2020 at 13:32):

I'll just make a new topic.

#### Reid Barton (Aug 06 2020 at 13:32):

oh, I would have to do it on my own messages

#### Reid Barton (Aug 06 2020 at 13:32):

I think you can do it on your messages, e.g., starting with this one

#### Adam Topaz (Aug 06 2020 at 13:33):

I don't have a move option.

#### Reid Barton (Aug 06 2020 at 13:34):

edit message and then change the topic

That worked!

#### Adam Topaz (Aug 06 2020 at 13:35):

Here's what I have so far:

import algebra

class comm_mul_action M N α
[monoid M] [monoid N]
[mul_action M α] [mul_action N α] :=
(commutes {m : M} {n : N} {a : α} : m • n • a = n • m • a)

class biaction M N α [monoid M] [monoid N]
[mul_action M α] [mul_action Nᵒᵖ α] extends comm_mul_action M Nᵒᵖ α

notation a  • :73 m := has_scalar.smul (opposite.op m) a

class bimodule A B M [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] extends biaction A B M

variables (A B M : Type*) [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] [bimodule A B M]
variables (a : A) (b : B) (m : M)

example : a • m • b = a • (m • b) := by rw comm_mul_action.commutes

instance foo1 : semimodule Aᵒᵖ A :=
{ smul := λ a b, b * a.unop,
one_smul := by simp,
mul_smul := by simp [mul_assoc],
smul_zero := by simp,
zero_smul := by simp }

instance foo : bimodule A A A :=
{ commutes := λ a b c, by { change _ * (_ * _ ) = _, rw ←mul_assoc, refl } }


#### Reid Barton (Aug 06 2020 at 13:37):

Now if you try to use • on a ring A do you not get some overloaded notation error?

#### Adam Topaz (Aug 06 2020 at 13:37):

Yeah, there's the issue.

#### Utensil Song (Aug 06 2020 at 13:38):

Ping @Eric Wieser

#### Adam Topaz (Aug 06 2020 at 13:39):

Okay, how do you write that right triangle thing?

#### Reid Barton (Aug 06 2020 at 13:40):

\tb but in emacs

#### Adam Topaz (Aug 06 2020 at 13:40):

Works in vscode too.

#### Eric Wieser (Aug 06 2020 at 13:41):

Can we just use an r subscript for the right version?

#### Adam Topaz (Aug 06 2020 at 13:42):

Maybe, but wouldn't it be terrible to write \bu\_r a million times?

#### Eric Wieser (Aug 06 2020 at 13:43):

Could always have \bur as a shorhand

Or \rbullet etc

#### Adam Topaz (Aug 06 2020 at 13:50):

The last line in this gives me errors:

import algebra

class comm_mul_action M N α
[monoid M] [monoid N]
[mul_action M α] [mul_action N α] :=
(commutes {m : M} {n : N} {a : α} : m • n • a = n • m • a)

class biaction M N α [monoid M] [monoid N]
[mul_action M α] [mul_action Nᵒᵖ α] extends comm_mul_action M Nᵒᵖ α

notation m  •ᵣ :73 a := (opposite.op a) • m

class bimodule A B M [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] extends biaction A B M

variables (A B M : Type*) [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] [bimodule A B M]
variables (a : A) (b : B) (m : M)

#check a • m •ᵣ b
#check a • (m •ᵣ b)

example : a • m •ᵣ b = a • (m •ᵣ b) := sorry


Can anyone reproduce and/or explain why?

#### Reid Barton (Aug 06 2020 at 13:52):

example : (a • m •ᵣ b) = a • (m •ᵣ b) := sorry

#### Adam Topaz (Aug 06 2020 at 13:52):

Yeah, just figured that out too :)

#### Adam Topaz (Aug 06 2020 at 13:52):

That's annoying though.

#### Adam Topaz (Aug 06 2020 at 13:53):

I guess it's some precedence issue with equality?

#### Reid Barton (Aug 06 2020 at 13:53):

or notation m  •ᵣ :73 a:73 := (opposite.op a) • m or 72 whichever is the right one, I can never remember how these work

#### Reid Barton (Aug 06 2020 at 13:54):

73 is the right one apparently

#### Adam Topaz (Aug 06 2020 at 13:56):

I think we should make it 72: e.g. with 73 this is true:

variables {x y z : A}

example : x • y •ᵣ z = x • (y •ᵣ z) := rfl


#### Reid Barton (Aug 06 2020 at 13:56):

what I mean is the levels for •ᵣ should be equal because then it will associate properly with itself

Oh ok.

#### Adam Topaz (Aug 06 2020 at 13:59):

Seems okay so far:

import algebra

class comm_mul_action M N α
[monoid M] [monoid N]
[mul_action M α] [mul_action N α] :=
(commutes {m : M} {n : N} {a : α} : m • n • a = n • m • a)

class biaction M N α [monoid M] [monoid N]
[mul_action M α] [mul_action Nᵒᵖ α] extends comm_mul_action M Nᵒᵖ α

notation m  •ᵣ :72 a:72 := (opposite.op a) • m

class bimodule A B M [semiring A] [semiring B] [add_comm_monoid M]
[semimodule A M] [semimodule Bᵒᵖ M] extends biaction A B M

variables (A : Type*) [semiring A]

namespace semiring
instance : semimodule Aᵒᵖ A :=
{ smul := λ a b, b * a.unop,
one_smul := by simp,
mul_smul := by simp [mul_assoc],
smul_zero := by simp,
zero_smul := by simp }

instance : bimodule A A A :=
{ commutes := λ a b c, by { change _ * (_ * _ ) = _, rw ←mul_assoc, refl } }
end semiring

variables {x y z : A}

example : x • y •ᵣ z = x • (y •ᵣ z) :=
by simp_rw comm_mul_action.commutes


#### Eric Wieser (Aug 06 2020 at 14:13):

notation m  •ᵣ :72 a:72 := (opposite.op a) • m - this doesn't strike me as correct - don't you need (opposite.unop (opposite.op a) • (opposite.op m))?

i.e., flip both arguments and the order of multiplication, then flip the result back

#### Adam Topaz (Aug 06 2020 at 14:21):

I'm confused. Why? A right action is just a left action by the opposite ring.

#### Eric Wieser (Aug 06 2020 at 14:25):

My uninformed thinking was that maybe α needs to be made opposite too. Maybe the argument goes that α doesn't define any multiplicative operator so it doesn't matter

#### Yury G. Kudryashov (Aug 06 2020 at 16:44):

α has no multiplication so there is no need to opposite it.

#### Yury G. Kudryashov (Aug 06 2020 at 16:46):

Note that comm_mul_action can be used for something else than bimodules. E.g., a group representation is a mul_action on a vector space that commutes with the action of the field (though this doesn't help us study the set of all representations).

#### Eric Wieser (Aug 06 2020 at 17:09):

Yury G. Kudryashov said:

α has no multiplication so there is no need to opposite it.

There's no has_mul α in that context, but what if there is in a consumer?

#### Adam Topaz (Aug 06 2020 at 17:19):

I'm the case of an algebra, the multiplication from the base ring commutes with everything anyway, so it shouldn't matter.

#### Adam Topaz (Aug 06 2020 at 17:21):

Is this the example you have in mind?

#### Aaron Anderson (Dec 22 2020 at 22:29):

I think we should revisit this. I've been discussing bimodule implementation at https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/4770.20smul_comm_class with @Yury G. Kudryashov

#### Aaron Anderson (Dec 22 2020 at 22:29):

my work so far is at branch#bimodule

#### Yury G. Kudryashov (Dec 22 2020 at 22:31):

Can you define subbimodule R M := submodule (R × opposite R) M and reuse most of the theory about submodules?

#### Aaron Anderson (Dec 22 2020 at 22:39):

I'll try that. Should I also try defining bimodules that way from the beginning, or just provide a module (A × opposite B) M instance givenbimodule A B M?

#### Aaron Anderson (Dec 22 2020 at 22:40):

I guess that last question is about equivalent to "should bimodules be mixins?"

#### Yury G. Kudryashov (Dec 22 2020 at 22:41):

We should have a semimodule (R × S) M instance given semimodule R M, semimodule S M, and smul_comm_class R S M.

#### Adam Topaz (Dec 22 2020 at 22:53):

I don't know if the last few comments use the Cartesian product just because of Unicode input problems with zulip, but it's important to note that a bimodule is a module over the tensor product not the Cartesian product (distributivity won't work correctly with Cartesian product).

#### Aaron Anderson (Dec 22 2020 at 22:58):

Hrmm, we are climbing up the import tree quickly

#### Yury G. Kudryashov (Dec 22 2020 at 23:00):

BTW, should we redefine submodules based on a distrib_mul_action instead of a semimodule?

#### Aaron Anderson (Dec 22 2020 at 23:01):

Yeah, this is getting impractical for basic definitions, in part because our tensor products require commutativity, and a lot of the point of bimodules requires noncommutative scalars

#### Aaron Anderson (Dec 22 2020 at 23:02):

Yury G. Kudryashov said:

BTW, should we redefine submodules based on a distrib_mul_action instead of a semimodule?

I don't see why not. Nothing breaks immediately.

#### Aaron Anderson (Dec 22 2020 at 23:03):

wait, the commutativity requirement might not be necessary, let me check

#### Aaron Anderson (Dec 22 2020 at 23:09):

Yeah, I think commutativity isn't necessary, but subtraction totally is

#### Aaron Anderson (Dec 22 2020 at 23:10):

I'm ok only defining subbimodules for actual bimodules and not bisemimodules

#### Reid Barton (Dec 22 2020 at 23:37):

I hope that whatever ends up happening is built on top of some kind of bi-mul_actions so we don't have to reinvent those later. That probably rules out approaches based on the tensor product (which likely weren't that viable anyways).

#### Aaron Anderson (Dec 22 2020 at 23:50):

I think the tensor product might be viable for defining subbimodules - not really for bimodules themselves.

#### Aaron Anderson (Dec 22 2020 at 23:52):

As to bi-mul_action, I think the implementation would just be to assume two separate mul_actions and then a smul_comm_class, which we already have

#### Aaron Anderson (Dec 23 2020 at 00:08):

Unless you mean implementing sub_bi_mul_action

#### Aaron Anderson (Dec 23 2020 at 00:12):

In which case I think there would be a diamond to deal with

Last updated: May 06 2021 at 18:20 UTC