Zulip Chat Archive

Stream: general

Topic: star_ring

Scott Morrison (Sep 06 2020 at 07:12):

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 (Sep 06 2020 at 07:14):

I was imagining something like:

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

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

Scott Morrison (Sep 06 2020 at 07:15):

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

Frédéric Dupuis (Sep 07 2020 at 00:15):

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 (Sep 07 2020 at 03:11):

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 (Sep 07 2020 at 03:12):

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 (Sep 07 2020 at 04:21):

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

Scott Morrison (Sep 07 2020 at 04:50):

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

Alex J. Best (Sep 07 2020 at 05:00):

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 (Sep 07 2020 at 23:17):

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

Eric Wieser (Nov 03 2020 at 14:09):

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

Frédéric Dupuis (Nov 03 2020 at 16:30):

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

Eric Wieser (Nov 03 2020 at 16:47):

I think he's just been busy

Eric Wieser (Nov 03 2020 at 16:48):

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

Scott Morrison (Nov 04 2020 at 03:47):

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

Eric Wieser (Nov 04 2020 at 10:28):

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"?

Last updated: Aug 03 2023 at 10:10 UTC