star_ring

Stream: general

[Scott Morrison]

Do we yet have anything about *-algebras? I'd like some! I know we have src#ring_invo (which I've just tidied up a bit in #4052).

[Scott Morrison]

I was imagining something like:

variables {R : Type} [ring R] [star_ring R]

example (r s : R) : (r * s)† = s† * r† := ...

[Scott Morrison]

It would be fun to, e.g. prove Bell's inequality, or define Banach algebras...

[Frédéric Dupuis]

I think it would be nice to have some sort of has_star typeclass that could be used for this, with instances for complex conjugation, Hermitian adjoints, etc.

[Scott Morrison]

I wonder how much value has_star itself actually has, vs. starting at star_ring. Are the examples of less-than-rings which we will want to talk about star(=linear, antimultiplicative involutions) on? I guess I have no complaint about star_ring only depending on semiring, rather than ring.

[Scott Morrison]

I also feel pretty strongly about not making global notation for this. Depending on which topic of mathematics I'm thinking about today, I might feel strongly that this operation should be written as star, bar, or dagger. :-)

[Johan Commelin]

But the bar will look funny in unicode, no matter what, right?

[Scott Morrison]

feeling strongly about notation rarely leads to being happy in lean (or life, for that matter)

[Alex J. Best]

I was kinda surprised this works to be honest:

variables {K : Type} [field K] (x y : K)
def bar : K → K := sorry
notation `̅` a := bar a
#check ̅x
#check ̅(1 : K)

of course the second one looks silly, but ̅x isn't so bad in vscode.

[Frédéric Dupuis]

Yeah, actually we probably want to be flexible regarding notation on this one!

[Eric Wieser]

I've tried to revive the star parts of @Scott Morrison's PR in #4886

[Frédéric Dupuis]

Were those PRs actually dropped, or did @Scott Morrison just not have time yet?

[Eric Wieser]

I think he's just been busy

[Eric Wieser]

I thought I'd try splitting them up to help speed things along

[Scott Morrison]

I hadn't had time, but definitely come back to them. Happy for any help, however!

[Eric Wieser]

Should I take that as "I don't object to you splitting out that PR and having to deal with merging it back in later"?