Conflicting `≤` and `<`

Stream: mathlib4

[Alex Meiburg]

In working on QuantumInfo we've run into a funny problem. The Loewner_order is pretty common throughout quantum information, and defines two operators ≤ and < on matrices (or more generally, linear operators): A ≤ B means (B - A).PosSemidef, and A < B means (B - A).PosDef. Each of these is generally well-behaved with regards to addition and scalar multiplication ... they turn matrices into a OrderedCancelAddCommMonoid, for instance.

We would like to have these both available to work with.

But the silly thing is that these two definitions conflict: it is not true that a ≤ b ↔ a = b ∨ a < b. They generally "agree" in the sense that a = b → a ≤ b, a < b → a ≤ b, and a < b → a ≠ b. Unfortunately, already at the most basic level(!) of Preorder, Mathlib assumes that LE and LT should be related this way. This means we can't make one instance accessible without automatically making another, garbage notation available.

If we make a ≤ b available, then we get a < b which ends up meaning "B - A is positive semi-definite but not zero". We can make a < b available instead, and (uniquely) complete it to a preorder by defining a ≤ b appropriately, but then that ends up meaning "B - A is either 0 or positive definite". Both of these are pretty undesirable.

We can of course use a custom notation like ≺ and ≼, or ⩽, but then we're losing out on Preorder and the entire class hierarchy and all the useful theorems.

[Alex Meiburg]

Is there any way to, for instance, say "I have this Preorder instance, but please only ever use it to for the LE instances and not an LT instance"? And then likewise for another one, where I only want the LT instance?

Of course if I start with h : a ≤ b and then do h.lt I'll have ended up with the "bad" instance, but I don't expect Lean (or Mathlib) could offer me any better solution.

[Edward van de Meent]

you could have a type alias where you endow the structure with the reflexivisation of <, then have notation ≺ which means "move to the type alias, then <"

[Edward van de Meent]

at least, i think that works

[Edward van de Meent]

so basically, you can have two Preorder instances, and have notation tell lean which to use by making them a macro for type aliases

[Eric Wieser]

This is probably a bad idea, because the lemmas / tactics will likely match the wrong one and complain whoops, I missed the type alias part.

[Jireh Loreaux]

I don't think type aliases are the way to go here.

[Eric Wieser]

@Jireh Loreaux, is the proposed ≤ order also the one that satisfies StarOrderedRing?

[Jireh Loreaux]

Yes, I think we already have this order on matrices over RCLike in Mathlib.

[Jireh Loreaux]

At least, I definitely wrote it at one point, and I think I remember PR'ing it, but possibly not.

[Alex Meiburg]

It exists and we're using it. :) (Thanks!)

[Eric Wieser]

Loogle finds nothing for StarOrderedRing (Matrix _ _ _)

[Jireh Loreaux]

Oh, then I guess I didn't PR it.

[Eric Wieser]

@Alex Meiburg, what are you referring to then?

[Alex Meiburg]

Oh, I got it mixed up. We're not using one from Mathlib, we've got our own instance. It was a while ago and we went through a few iterations so my memory got confused

[Jireh Loreaux]

(deleted)

[Yaël Dillies]

Alex Meiburg said:

We can of course use a custom notation like ≺ and ≼, or ⩽, but then we're losing out on Preorder and the entire class hierarchy and all the useful theorems.

How many "useful theorems" do you expect apply to your case (apart from the fact that a < b ↔ a ≤ b ∧ ¬ b ≤ a doesn't hold)?

[Edward van de Meent]

I guess at worst we could generalize Preorder to PrePreorder/SemiPreorder/etc

[Alex Meiburg]

Oh, there's docs#ContinuousLinearMap.instLoewnerPartialOrder, that's what I was thinking of

[Eric Wieser]

I think if forced to choose the ≤ ordering is most justified as a global instance

[Jireh Loreaux]

No, I think the answer here is that we want something akin to (but different from) docs#StrongLT. We're going to need the same kind of thing for C⋆-algebras, as this is exactly the concept of a strictly positive element in that context.

[Jireh Loreaux]

And probably (scoped) notation like ≪ is appropriate for it.

[Alex Meiburg]

Yaël Dillies said:

How many "useful theorems" do you expect apply to your case (apart from the fact that a < b ↔ a ≤ b ∧ ¬ b ≤ a doesn't hold)?

All the theorems that OrderedAddCommMonoid obeys, like sub_le_sub_iff for instance

[Alex Meiburg]

(and then also sub_lt_sub_iff ... both of which hold, they're just talking about different orderings)

[Eric Wieser]

Eric Wieser said:

I think if forced to choose the ≤ ordering is most justified as a global instance

I would also be happy to see this PR :)!

[Yaël Dillies]

I am pressed to remind the community that last time someone claimed to have an interesting order for which a < b ↔ a ≤ b ∧ ¬ b ≤ a doesn't hold, it turned out the order was wrong: #maths > Surreal numbers @ 💬

[Jireh Loreaux]

Yaël, this is absolutely standard in operator algebras.

[Eric Wieser]

StrongLT is a trivial example of where that doesn't hold, right?

[Yaël Dillies]

Just making sure... :smile:

[Jireh Loreaux]

Preferably, it will be some sort of class that you can hook into and extends PartialOrder. Note that it needs to be a class like this to cover both the case of matrices and abstract C⋆-algebras. (In the non-unital C⋆-algebra setting, being strictly positive means that the hereditary C⋆-subalgebra generated by that element is the whole algebra, so it's quite a different beast; in the unital setting this is equivalent to being nonnegative with zero not in the spectrum.)

[Alex Meiburg]

Indeed the Loewner order is exactly the same as theStrongLT issue, if you treat each matrix M as a function fun v => v * M * (star v); then the standard ordering on functions gives the A ≤ B ordering, and the StrongLT ordering on functions gives the A < B ordering.

[Alex Meiburg]

In the non-unital C⋆-algebra setting, being strictly positive means that the hereditary C⋆-subalgebra generated by that element is the whole algebra, so it's quite a different beast

woah, I didn't know that

[Alex Meiburg]

Eric Wieser said:

I think if forced to choose the ≤ ordering is most justified as a global instance

Just wanted to echo I totally agree with this. This is what's been going on in our repo so far. We'd written 0 < B a couple of places to mean B.PosDef, and when trying (and failing) to fill in the sorries we realized what was happening... :)

[Eric Wieser]

Jireh Loreaux said:

And probably (scoped) notation like ≪ is appropriate for it.

What do we call the version of Set.Ioo for the strong order?

[Jireh Loreaux]

Set.Ioooooooo :laughter_tears:

[Jireh Loreaux]

I think we likely don't have a name for it.

[Eric Wieser]

I can see that being quite handy, because on product types Set.Ioo is pretty useless (give me the whole cube except its top and bottom point)

[Edward van de Meent]

i mean... is there even a notion of strongly open sets, for that matter?

[Edward van de Meent]

since that's what the o refers to

[Alex Meiburg]

infix:max "💪<" => StrongLT

[Alex Meiburg]

So (besides just making do with (B-A).PosDef), what would be the best way to try to move forward with this?
Try to figure out a "generalized StrongLT", that has some facts about it being compatible with a PartialOrder, so it can be a kind of mixin - across different objects that would have a notion like this?

[Alex Meiburg]

I'm picturing something like

class Strong_LT (α : Type*) [Preorder α] where
  rel : α → α → Prop
  so : IsStrictOrder α rel
  lt_of_stronglt : ∀ x y, rel x y → x < y

infix:50 " ≺ "  => Strong_LT.rel

[Alex Meiburg]

I think by connecting it to a preorder like that, then some other theorems can be proved by ≺ in appropriate cases. Like with IsOrderedAddMonoid you can already establish that a ≺ b → ∀ (c : α), ¬(c + b ≺ c + a), for instance

[Alex Meiburg]

I don't know if it would make sense to require more connections between the two. Saying that ≺ should also respect any StrictMono functions seems reasonable (and, I think, holds for both these cases) and then a lot more could be proved in general about linking it back and forth to the 'main' preorder

[Junyan Xu]

Why is α implicit in Strong_LT?

∀< is apparently a valid notation too.

[Alex Meiburg]

Junyan Xu said:

Why is α implicit in Strong_LT?

Because I was silly :) Fixed haha

∀< is apparently a valid notation too.

Oh, that's nice