Zulip Chat Archive

Stream: maths

Topic: Misc semigroup stuff

Cameron Torrance (Sep 13 2022 at 18:11):

A few months ago I was working on implementing the multiplier algebra of a C*-algebra and learnt much of the terminology used in this context comes from a paper about semigroups.

Let $S$ be a semigroup. A function $L: S \to S$ is said to be a left centraliser if :

L(ab) = L(a)b .

A function $R:S \to S$ is said to be a right centraliser if :

R(ab) = a R(b) .

A pair of functions $L, R : S \to S$ is said to be a double centraliser if:

aL(b) = R(a)b .

I was wondering how common this terminology is and if these definitions + minor results involving them, are important enough in more general contexts to warrant living outside my multiplier algebra file.

Additionally I'm wondering want is currently the best way of talking about (left/right) cancelative semigroups.

Johan Commelin (Sep 13 2022 at 18:18):

There is docs#left_cancel_semigroup

Cameron Torrance (Sep 13 2022 at 18:26):

wouldn't this cause issues if I wanted to talk about a semigroup being left and right cancellative?

Johan Commelin (Sep 13 2022 at 18:29):

Doesn't seem to have come up yet... we don't have cancel_semigroup. But docs#cancel_monoid does exist.

Cameron Torrance (Sep 13 2022 at 18:41):

I have results that use left, right and left + right assumptions, and monoids aren't general enough for the specific application I have in mind.

Johan Commelin (Sep 13 2022 at 18:46):

It's certainly possible to add cancel_semigroup to the hierarchy.

Yaël Dillies (Sep 13 2022 at 19:52):

@Christopher Hoskin, didn't you prove some results about left/right centralizers by any chance?

Christopher Hoskin (Sep 13 2022 at 20:09):

@Yaël Dillies Is this what you were thinking of: https://github.com/leanprover-community/mathlib/pull/12746 ? It has been in review for 6 months now.

Christopher Hoskin (Sep 13 2022 at 20:14):

My memory is a bit rusty now (it's decades since I studied maths full time) but I suspect that the centroid of a non-unital C*-algebra coincides with the centre of the unitization of the C*-algebra?

Yaël Dillies (Sep 13 2022 at 20:17):

Oh yes, I wasn't sure whether it was centroid_hom or not anymore

Christopher Hoskin (Sep 13 2022 at 21:31):

Yaël Dillies said:

Oh yes, I wasn't sure whether it was centroid_hom or not anymore

I think that was your terminology, but it seemed consistent with what's elsewhere in mathlib, so we kept it.

Yaël Dillies (Sep 13 2022 at 21:35):

Yeah, I fully came up with the name. Never studied C-algebras at all.

Last updated: Dec 20 2023 at 11:08 UTC