refactor(algebra/star): replace `star_ring_aut` with `star`

[eric-wieser]

As opposed to star_ring_aut. This is an alternate approach to and partial reversion of #9640 ~~, made as a PR for ease of discussion.~~

---

[hrmacbeth]

Eric, thank you for your work on this experiment. I'm still not in favour of this approach. I think it would be very off-putting to potential users of the complex numbers (many of whom are not mathematically sophisticated, or who are mathematically sophisticated but are analysts rather than algebraists) to have to encounter the word star. For example, in analysis.complex.isometry, in the approach of this PR,

rw [conj.map_sub, conj.map_sub] at this,

becomes

rw [star_sub, star_sub] at this,

(in #9640 it becomes

rw [ring_equiv.map_sub, ring_equiv.map_sub] at this,

which is still a little undesirable, but at least most users will know what a ring_equiv is.)

[hrmacbeth]

Note: an alternative solution would be to rename has_star to has_conj, star_ring to conj_ring, etc etc! Possibly with localized notation star for conj in the cstar_algebra locale. Did we discuss this possibility before?

Edit: I guess this would have the disadvantage of subtly bringing the noncommutative case where it's not wanted. For example, the standard conj_mul lemma would say conj (a * b) = conj b * conj a which would definitely confuse many users.

[eric-wieser]

I think if the name were conj we could justify swapping around the conj_mul and conj_mul' lemmas to make commutativity less surprising

[dupuisf]

I'm still skeptical about the unbundled approach given that there is no "historical" reason for it, but now that there is at least a basic API for it I could probably live with it.

If we do go down this route though, I think I would prefer to get rid of conj entirely and just have star. I think having multiple versions of this for no real reason is more confusing than having to learn once that the complex conjugate is called star -- out of all the things about Lean that might confuse a beginner, I'm not sure this makes even the top 50 :-)

[eric-wieser]

Regarding naming; we could have the function named conj, but still call the typeclass star_monoid etc. @semorrison, independent of whether we go the bundled approach, what's your view on star vs conj as names?

[hrmacbeth]

If we do go down this route though, I think I would prefer to get rid of conj entirely and just have star. I think having multiple versions of this for no real reason is more confusing than having to learn once that the complex conjugate is called star -- out of all the things about Lean that might confuse a beginner, I'm not sure this makes even the top 50 :-)

Hmm, I don't agree, I think this is quite an off-putting thing! If we are going to completely unify, I think we should use the names conj, conj_mul, conj_add, etc. (I don't care whether the objects are called star_ring or conj_ring, I only care about the name of the operation and its lemmas.). The users of C*-algebras will be on average much more sophisticated than the users of the complex numbers, and better able to deal with an unexpected naming choice.

In summary I would prefer, to the current approach of this PR, either (A) the approach of #9640 or (B) a wholesale renaming of star, star_add etc to conj, conj_add etc. I don't have a preference between (A) and (B).

[eric-wieser]

I have a slight preference for B, but also I'd never seen the "star" terminology before this so am not particularly equipped to see the downsides in B.

I don't object to merging A while we decide, but I think we should at least have the discussion about B involving people who do care about the "star" naming.

[dupuisf]

So we really have two decisions to make: (1) whether we go bundled or unbundled, and (2) if we go unbundled, what the naming scheme should be (in the bundled case we'll have a few different versions of star in use, so I think having different names is not so bad). My preferred option is still bundled; in the applications I'm interested in, this would mean having two versions in common use: star_ring_aut denoted as conj for the complex conjugate, and a future star_linear_isometry (with perhaps a shorter name/notation) for C*-algebras.

In the unbundled case, I think a simple and consistent naming scheme should be the main priority. I agree that "star" is a bit off-putting for beginners, but I think it's the sort of thing one gets over very quickly. We had a comparable example in mathlib until recently, with the whole semimodule/module/vector_space thing, which was arguably friendlier to beginners who just want vector spaces, but in the long run I think this was more confusing than just learning that vector space is now spelled "module".