Pointed monoid

Stream: maths

[Adam Topaz]

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

[Jalex Stark]

we have group_with_zero

[Heather Macbeth]

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

[Adam Topaz]

Yes! Thanks!

[Adam Topaz]

Oh, but unfortunately docs#monoid_algebra uses monoids :(

[Kevin Buzzard]

A monoid with zero is a monoid though

[Kevin Buzzard]

(a group with 0 isn't a group)

[Adam Topaz]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

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]

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]

(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]

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

[Kevin Buzzard]

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

[Adam Topaz]

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]

Yeah! It's great!

[Adam Topaz]

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}$).

[Kevin Buzzard]

Why no I?

[Adam Topaz]

There's no map to a ring.

[Kevin Buzzard]

aah!

[Adam Topaz]

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

[Kevin Buzzard]

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]

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

[Adam Topaz]

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]

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

[Adam Topaz]

Yeah, I know.

[Adam Topaz]

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

[Patrick Massot]

I can feel motivation building up :grinning:

[Kevin Buzzard]

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]

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

[Adam Topaz]

What could go wrong?

[Kevin Buzzard]

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

[Adam Topaz]

True!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Yeah this a very cool way to do it

[Adam Topaz]

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

[Adam Topaz]

"same" = "mathematician's same"

[Adam Topaz]

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]

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]

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]

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

[Adam Topaz]

Oh I see.

[Adam Topaz]

Yeah that would be annoying.

[Yury G. Kudryashov]

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]

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

[Yury G. Kudryashov]

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

[Adam Topaz]

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