[Merged by Bors] - feat(algebra/star/self_adjoint): define normal elements of a star monoid

[dupuisf]

In this PR, we define the normal elements of a star monoid, i.e. those elements x
that commute with star x. This is defined as the prop type class is_star_normal.

This was formalized as part of the semilinear maps paper.

---

[dupuisf]

What do people think of making this a type class?

[j-loreaux]

What do you want the instances to be? I guess selfadjoints, unitaries and in more specialized settings, diagonal operators and multiplication operators? Would the point be that if you had an instance [is_star_normal x] you could, for example, automatically conclude that the star subring generated by x is commutative? If so, that could be useful, but at the moment I'm not clear about the utility of making it a type class.

[dupuisf]

Yeah, for now the obvious ones are self-adjoints, unitaries, one, zero, and anything with [has_trivial_star R]. And yes, that was indeed one of the applications I had in mind; another one would be that we could get a diagonalization of an operator without constantly having to pass this as an explicit parameter.

[dupuisf]

I just changed it to a type class in the end. I think it will be very useful when we defining the functional calculus to have it as a type class, so we don't have to pass this around all the time as a parameter; the same goes for the spectral theorem. I can't really picture it causing serious type class inference problems, since it's anyway a prop and we probably won't be adding too many more instances than the few I just added here.

[ocfnash]

What do people think of making this a type class?

I'm dubious about making this a class. I confess that my doubts stem mostly from the fact that it is not very Mathlib-idiomatic rather than a specific worry.

How about we make this a def and if / when the day comes that the manual parameter-passing becomes a pain we consider upgrading then?

[j-loreaux]

I have thought more about this, and I think making it a type class is the way to go. Unlike some other important classes of operators like selfadjoints or unitaries, star normal elements don't have a nice "substructure" (addition or multiplication of normal elements is not normal in general, really it is only closed under the star involution). Thus, while you could bundle star normal elements into a subtype, doing so only really buys you headaches. However, for many applications, we will be passing this condition around a lot, and it would be nice to package it by making it into a type class.

[eric-wieser]

Is there a typeclass in another part of the library that you're using as a template here?

I'd argue you should not make it a typeclass in this PR, and then ask for typeclass opinions in a follow-up PR from the authors of filter.ne_bot (a typeclass) vs is_unit (not a typeclass) vs ...

[dupuisf]

I think we might as well just have this discussion on Zulip right now, instead of possibly having to rewrite a lot of code. I just started a thread there.

[jcommelin]

The Zulip discussion seems to have converged on a typeclass approach. Let's try it out!

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Build failed (retrying...):

• Build mathlib

[eric-wieser]

bors r-

Can you merge master?

bors d+

[bors]

✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[bors]

Canceled.

[dupuisf]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests