unitary submonoid

Stream: maths

[Frédéric Dupuis]

unitary_submonoid is currently defined as the elements A of a unital star algebra that satisfy star A * A = 1. However, every source I've seen require both star A * A = 1 and A * star A = 1 (see e.g. Wikipedia, or these notes). Any objections if I change the definition? (Also, I'd like to change the name to just unitary, it looks much nicer!)

[Eric Wieser]

I was thinking about this the other day

[Eric Wieser]

If we had @Alex J. Best's work on Dedekind finite monoids, then we'd be able to talk about the cases where the definitions are equivalent

[Eric Wieser]

In particular, we could redefine circle as unitary ℂ

[Eric Wieser]

But if the usual definition has both conditions anyway, that's even easier

[Alex J. Best]

I worked on refreshing the branch a bit this week, its almost PRable now I believe

[Alex J. Best]

So hopefully not too many more years till its done :wink:

[Eric Wieser]

After this change, we can now show that circle = unitary complex. Is it sensible to make this definitionally true, or is that just annoying because being definitionally equal to sphere 0 1 is more useful?

[Eric Wieser]

I had a go at this, but there seems to be a bunch of topology stuff defined on sphere that isn't all that easy to transfer onto unitary