Bimodules

Stream: maths

[Reid Barton]

Does this really work?

[Reid Barton]

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

[Adam Topaz]

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]

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

[Reid Barton]

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

[Adam Topaz]

I'm thinking something along these lines:

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

[Reid Barton]

Is that the same character as left multiplication?

[Adam Topaz]

Yeah, is that a problem?

[Reid Barton]

Would this work for bimodules?

[Adam Topaz]

Not sure yet. I'll have to try.

[Reid Barton]

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

[Adam Topaz]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

oh wait I can't any more

[Adam Topaz]

I'll just make a new topic.

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

I don't have a move option.

[Reid Barton]

edit message and then change the topic

[Adam Topaz]

That worked!

[Adam Topaz]

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_add := by simp [add_mul],
  smul_zero := by simp,
  add_smul := by simp [mul_add],
  zero_smul := by simp }

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

[Reid Barton]

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

[Adam Topaz]

Yeah, there's the issue.

[Utensil Song]

Ping @Eric Wieser

[Adam Topaz]

Okay, how do you write that right triangle thing?

[Reid Barton]

\tb but in emacs

[Adam Topaz]

Works in vscode too.

[Eric Wieser]

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

[Adam Topaz]

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

[Eric Wieser]

Could always have \bur as a shorhand

[Eric Wieser]

Or \rbullet etc

[Adam Topaz]

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]

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

[Adam Topaz]

Yeah, just figured that out too :)

[Adam Topaz]

That's annoying though.

[Adam Topaz]

I guess it's some precedence issue with equality?

[Reid Barton]

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]

73 is the right one apparently

[Adam Topaz]

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]

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

[Adam Topaz]

Oh ok.

[Adam Topaz]

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_add := by simp [add_mul],
  smul_zero := by simp,
  add_smul := by simp [mul_add],
  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]

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]

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

[Eric Wieser]

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]

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

[Yury G. Kudryashov]

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]

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]

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

[Adam Topaz]

Is this the example you have in mind?

[Aaron Anderson]

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]

my work so far is at branch#bimodule

[Yury G. Kudryashov]

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

[Aaron Anderson]

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]

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

[Yury G. Kudryashov]

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]

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]

Hrmm, we are climbing up the import tree quickly

[Yury G. Kudryashov]

@Adam Topaz It's because I made a stupid mistake.

[Yury G. Kudryashov]

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

[Aaron Anderson]

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]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Reid Barton]

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]

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

[Aaron Anderson]

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]

Unless you mean implementing sub_bi_mul_action

[Aaron Anderson]

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