## Stream: maths

### Topic: Pointed monoid

#### Adam Topaz (Aug 04 2020 at 18:13):

What's the mathlib way to speak about pointed monoids, i.e. multiplicative monoids with an absorbing element called "0"?

#### Jalex Stark (Aug 04 2020 at 18:16):

we have group_with_zero

#### Heather Macbeth (Aug 04 2020 at 18:16):

There is docs#monoid_with_zero, is that the same thing?

Yes! Thanks!

#### Adam Topaz (Aug 04 2020 at 18:18):

Oh, but unfortunately docs#monoid_algebra uses monoids :(

#### Kevin Buzzard (Aug 04 2020 at 20:17):

A monoid with zero is a monoid though

#### Kevin Buzzard (Aug 04 2020 at 20:17):

(a group with 0 isn't a group)

#### Adam Topaz (Aug 04 2020 at 20:20):

But the zero in the monoid_with_zero needs to be identified with the zero in the monoid algebra.

#### Adam Topaz (Aug 04 2020 at 20:22):

If you forget the zero exists in the monoid_with_zero, then I don't think you get the right object.

#### Kevin Buzzard (Aug 04 2020 at 20:27):

oh no you're right, that's not now it works. Why do you need such a construction? The monoid ring is a free module over the ring with basis the monoid.

#### Kevin Buzzard (Aug 04 2020 at 20:28):

Random note: monoids with zero were introduced by Johan as a result of our work formalising valuations, which we needed for adic spaces.

#### Adam Topaz (Aug 04 2020 at 20:29):

There are various reasons for this... One which you might like comes from Theorem 1 in this paper: https://arxiv.org/pdf/1311.2774.pdf

#### Adam Topaz (Aug 04 2020 at 20:30):

(In this case it doesn't matter because the 0 in $R$ maps to $0$ via the map they mention, but I would like to use a similar constructions in other contexts as well.)

#### Kevin Buzzard (Aug 04 2020 at 20:33):

I am confused. The Z[R] in that paper just looks like the standard monoid ring to me; in particular  != 0, so you can just use the monoid ring with the monoid-with-zero R.

#### Kevin Buzzard (Aug 04 2020 at 20:34):

My mind is also a bit blown -- this seems like a much easier construction than the Witt vectors.

#### Adam Topaz (Aug 04 2020 at 20:34):

Yes, it's just the usual monoid algebra, but the reason it works with just the monoid algebra is since they work with this ideal $I$.

#### Adam Topaz (Aug 04 2020 at 20:34):

Yeah! It's great!

#### Adam Topaz (Aug 04 2020 at 20:36):

The thing is, I want to do analogous things where no such $I$ exists (imagine, for example, the monoid algebra of the unit disc in $\mathbb{C}$).

Why no I?

#### Adam Topaz (Aug 04 2020 at 20:39):

There's no map to a ring.

aah!

#### Adam Topaz (Aug 04 2020 at 20:39):

Well, I guess there is (into $\mathbb{C}$), but is that really the correct thing? (my guess is no.)

#### Kevin Buzzard (Aug 04 2020 at 20:43):

You will have things in the kernel like [a]+[b]-[c]-[d] if a+b=c+d has magnitude > 1, so the kernel might be a lot harder to control

#### Kevin Buzzard (Aug 04 2020 at 20:44):

You should use the p-adic unit disc, then all your problems go away ;-)

#### Adam Topaz (Aug 04 2020 at 20:48):

Anyway, the short version is that I would like to think of $\mathbb{Z}[R]$ as a (very bad) approximation of Witt vectors, and try to play around with that.

#### Kevin Buzzard (Aug 04 2020 at 21:35):

You can just quotient out by R of course, and you also have [r] + [-r]...

Yeah, I know.

#### Adam Topaz (Aug 04 2020 at 21:41):

But mathlib doesn't even have two-sided ideals :(

#### Patrick Massot (Aug 04 2020 at 21:41):

I can feel motivation building up :grinning:

#### Kevin Buzzard (Aug 04 2020 at 21:45):

I count myself at least partially to blame for this. I had no idea that noncommutative rings existed so when we were pushing to develop some ring theory I was very much guided by Atiyah--Macdonald

#### Adam Topaz (Aug 04 2020 at 21:45):

I still think it makes sense to define bimodules as $A \otimes B^{op}$-modules.

#### Adam Topaz (Aug 04 2020 at 21:46):

What could go wrong?

#### Kevin Buzzard (Aug 04 2020 at 21:47):

Well you didn't see what went wrong when we first defined modules ;-)

True!

#### Kevin Buzzard (Aug 04 2020 at 21:47):

But I'd like to think that we are older and wiser now, although we are yet to fix subrings

#### Kevin Buzzard (Aug 04 2020 at 21:50):

I think it would be a very pleasant exercise to define two sided ideals of a ring, I'll try and drum up some enthusiasm amongst the troops. Isn't bimodules a different story? Oh -- you make R an R-bimodule and then just consider submodules? Very nice!

#### Kevin Buzzard (Aug 04 2020 at 21:51):

Yeah this a very cool way to do it

#### Adam Topaz (Aug 04 2020 at 21:53):

Yeah, an AB-bimodule is the "same" as a left $A \otimes B^{op}$-module.

#### Adam Topaz (Aug 04 2020 at 21:53):

"same" = "mathematician's same"

#### Adam Topaz (Aug 04 2020 at 21:54):

So we would need to define the obvious $A \otimes A^{op}$-module structure on $A$. A submodule is then a two-sided ideal, and we would get the additive structure of the quotient ring for free.

#### Reid Barton (Aug 04 2020 at 21:55):

If you define an $(A, B)$-bimodule as an $A \otimes B^\mathrm{op}$-module then you wouldn't be able to arrange that left and right multiplication have the expected formulas by definition

#### Adam Topaz (Aug 04 2020 at 21:56):

How so? You can deduce a left action of $A$ as $a \in A$ acting via $a \otimes 1$, and a right action via $1 \otimes b$.

#### Reid Barton (Aug 04 2020 at 21:56):

For example,

• R is an (R, R)-bimodule
• An (R, S)-bimodule is also a left R-module
• R is already a left R-module

There's no way you could make these left R-module structures agree definitionally

Oh I see.

#### Adam Topaz (Aug 04 2020 at 21:57):

Yeah that would be annoying.

#### Yury G. Kudryashov (Aug 06 2020 at 04:02):

About bimodules: I think that we should have a class comm_mul_actions M N \a [mul_action M \a] [mul_action N \a] saying that two actions commute

#### Yury G. Kudryashov (Aug 06 2020 at 04:03):

This can be used to define an action of the product of M and N

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

If M is a commutative monoid, then any action of M commutes with itself

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

Something like this?

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ᵒᵖ α


Last updated: May 10 2021 at 07:15 UTC