Zulip Chat Archive

Stream: maths

Topic: Pointed monoid


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

view this post on Zulip Jalex Stark (Aug 04 2020 at 18:16):

we have group_with_zero

view this post on Zulip Heather Macbeth (Aug 04 2020 at 18:16):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 18:16):

Yes! Thanks!

view this post on Zulip Adam Topaz (Aug 04 2020 at 18:18):

Oh, but unfortunately docs#monoid_algebra uses monoids :(

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:17):

A monoid with zero is a monoid though

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:17):

(a group with 0 isn't a group)

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

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

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

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

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:30):

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

view this post on Zulip 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] != 0, so you can just use the monoid ring with the monoid-with-zero R.

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

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:34):

Yeah! It's great!

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:36):

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:39):

Why no I?

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:39):

There's no map to a ring.

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:39):

aah!

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:39):

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

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 20:44):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 20:48):

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:35):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:39):

Yeah, I know.

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:41):

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

view this post on Zulip Patrick Massot (Aug 04 2020 at 21:41):

I can feel motivation building up :grinning:

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:45):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:46):

What could go wrong?

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:47):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:47):

True!

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

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

view this post on Zulip Kevin Buzzard (Aug 04 2020 at 21:51):

Yeah this a very cool way to do it

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:53):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:53):

"same" = "mathematician's same"

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:54):

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

view this post on Zulip Reid Barton (Aug 04 2020 at 21:55):

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:56):

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

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

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:56):

Oh I see.

view this post on Zulip Adam Topaz (Aug 04 2020 at 21:57):

Yeah that would be annoying.

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

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

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

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

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

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