Scott Morrison (Oct 03 2020 at 03:58):
Do you think I should try to change it? At the moment it seems to me that it's just going to be cumbersome to restrict the ordering to the self-adjoint elements, and somehow we don't lose anything by just having a partial order on everything.
Kevin Buzzard (Oct 03 2020 at 08:19):
Do you need an order on the complexes to talk about complex conjugation in this setting?
Scott Morrison (Oct 03 2020 at 10:48):
Yes, you do. The order you want is just the one that makes each horizontal line in the complex plane incomparable with each other line. Would that be unpleasant/wrong to have as an instance? If so, that suggests we should investigate only asking for an order on the self adjoint elements.
Frédéric Dupuis (Oct 05 2020 at 22:55):
Are you really using the order on elements where the imaginary part is nonzero?
Frédéric Dupuis (Oct 05 2020 at 22:57):
If having this as an instance doesn't cause problems elsewhere, that might make a lot of things simpler, like stating inequalities involving complex numbers that we know are always real.
Scott Morrison (Oct 05 2020 at 23:19):
No, I'm not using the order on non-self-adjoint elements at all.
Scott Morrison (Oct 05 2020 at 23:21):
It's a question of whether it's worth the encumbrance of having to define the subtype of self-adjoint elements, and put an order just on that, and then describe how the star interacts with that order.
Or to go with the current alternative, where it's much quicker to say how the order and the star structure should interact.
Scott Morrison (Oct 05 2020 at 23:22):
I guess I better try out making
complex a star-ordered ring, and see if anything complains.
Scott Morrison (Oct 06 2020 at 10:15):
It seems making
complex a star-ordered ring works fine.
Frédéric Dupuis (Oct 06 2020 at 19:34):
Reid Barton (Oct 06 2020 at 19:37):
This means if is a nonnegative real number?
Scott Morrison (Oct 06 2020 at 21:52):
Frédéric Dupuis (Oct 09 2020 at 15:03):
I just had a look at the
bell branch -- looks good to me! Just one suggestion: what about changing
class has_star (R S : Type u) := (star : R → S)
This way we could also use it for the adjoint of an operator of type
E →L[𝕜] F.
Scott Morrison (Oct 12 2020 at 03:45):
Unfortunately I don't think that typeclass resolution is going to enjoy this problem of having to work out
S every time. I will try it, but I'm pretty confident that this is a no-go.
Frédéric Dupuis (Oct 14 2020 at 15:58):
So even putting
[has_star R R] instead of
[has_star R] would cause problems...?
Frédéric Dupuis (Oct 14 2020 at 16:39):
Yeah, I guess having to define notation for every space to avoid this would just defeat the purpose. Never mind!
Last updated: May 14 2021 at 20:13 UTC