Zulip Chat Archive

Stream: maths

Topic: Bimodules


view this post on Zulip Reid Barton (Aug 06 2020 at 13:07):

Does this really work?

view this post on Zulip Reid Barton (Aug 06 2020 at 13:07):

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

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:09):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:20):

Is that the same character as left multiplication?

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:20):

Yeah, is that a problem?

view this post on Zulip Reid Barton (Aug 06 2020 at 13:21):

Would this work for bimodules?

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:21):

Not sure yet. I'll have to try.

view this post on Zulip Reid Barton (Aug 06 2020 at 13:21):

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

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:22):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:23):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:27):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:27):

oh wait I can't any more

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:32):

I'll just make a new topic.

view this post on Zulip Reid Barton (Aug 06 2020 at 13:32):

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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:32):

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

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:33):

I don't have a move option.

view this post on Zulip Reid Barton (Aug 06 2020 at 13:34):

edit message and then change the topic

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:34):

That worked!

view this post on Zulip 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_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 } }

view this post on Zulip 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?

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:37):

Yeah, there's the issue.

view this post on Zulip Utensil Song (Aug 06 2020 at 13:38):

Ping @Eric Wieser

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:39):

Okay, how do you write that right triangle thing?

view this post on Zulip Reid Barton (Aug 06 2020 at 13:40):

\tb but in emacs

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:40):

Works in vscode too.

view this post on Zulip Eric Wieser (Aug 06 2020 at 13:41):

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

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:42):

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

view this post on Zulip Eric Wieser (Aug 06 2020 at 13:43):

Could always have \bur as a shorhand

view this post on Zulip Eric Wieser (Aug 06 2020 at 13:43):

Or \rbullet etc

view this post on Zulip 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?

view this post on Zulip Reid Barton (Aug 06 2020 at 13:52):

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

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:52):

Yeah, just figured that out too :)

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:52):

That's annoying though.

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:53):

I guess it's some precedence issue with equality?

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 06 2020 at 13:54):

73 is the right one apparently

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 06 2020 at 13:57):

Oh ok.

view this post on Zulip 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_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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 06 2020 at 14:21):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Aug 06 2020 at 16:44):

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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Aug 06 2020 at 17:21):

Is this the example you have in mind?

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:29):

my work so far is at branch#bimodule

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:40):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Aaron Anderson (Dec 22 2020 at 22:58):

Hrmm, we are climbing up the import tree quickly

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 22:59):

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

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 23:00):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Aaron Anderson (Dec 22 2020 at 23:03):

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

view this post on Zulip Aaron Anderson (Dec 22 2020 at 23:09):

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

view this post on Zulip Aaron Anderson (Dec 22 2020 at 23:10):

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

view this post on Zulip 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).

view this post on Zulip Aaron Anderson (Dec 22 2020 at 23:50):

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

view this post on Zulip 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

view this post on Zulip Aaron Anderson (Dec 23 2020 at 00:08):

Unless you mean implementing sub_bi_mul_action

view this post on Zulip 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