Rank conjugate for IsROrC

Stream: general

[MohanadAhmed]

In PR #6239 I try to prove the following, For a matrix with elements in (IsROrC), the following three relations hold:

• $\text{rank}(A^H) = \text{rank}(A)$
• $\text{rank}(A^HA) = \text{rank}(A)$
• $\text{rank}(AA^H) = \text{rank}(A)$

The closest lemmas in mathlib to this are rank_conjTranspose, rank_self_mul_conjTranspose ... etc. These however do not apply since they require PartialOrder and StarOrderedRing instances on IsROrC. The status of the instances and where to place them seems to be a conversation the community is having and will continue to have for some time.

The lemmas above however apply without resorting to this specific class issue. All they need is dotProduc (star v) v =0 iff v = 0 which clearly applies to the IsROrC type class.

[MohanadAhmed]

Any thoughts welcome

[Eric Wieser]

I think there is a post on zulip somewhere that proves that first result in even greater generality, it would be good to find it

[MohanadAhmed]

Do you mean this one?
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/row.20rank.20equals.20column.20rank

[Eric Wieser]

Yes!

[Eric Wieser]

Though maybe that generalizes in a different direction...

[MohanadAhmed]

I think the fact that there is an IsROrC class is a strong indicator for having these lemmas. I mean is it not a bit odd that I cannot apply dotProduct_star_self_eq_zero to the IsROrC class?

[Eric Wieser]

Well yes, but you should also be able to apply it for \Q

[MohanadAhmed]

If you can make a class that includes Q, R, C alone then I think we can prove the dotProduct_star_self_eq_zero for them. But I don't think that would be a wise step. I think among those three Q is different , it is not like the others!

[Eric Wieser]

We already have one such class, it's StarOrderedRing!

[MohanadAhmed]

That includes things other than Q R C. Does it not include Positive Semi-definite Matrices for example?

[MohanadAhmed]

I mean no order is required to have dotProduct_star_self_eq_zero it is just straight equal or not equal question right?

[MohanadAhmed]

A StarOrderedRing as in mathlib requires a PartialOrder

[MohanadAhmed]

Which is a discussion you have demonstrated has been running on and off for some time

[Eric Wieser]

There's no question about whether we want the partial order: only if we want to make people type open scoped ComplexOrder to get it

[Eric Wieser]

I agree that it's unfortunate that the typeclass is about orders even though the statement does not mention inequalities

[Jireh Loreaux]

I'm not sure why you think needing the order here is unfortunate. This theorem, correctly interpreted, just says that a sum of positive elements is zero if and only if each of them is zero. You need the order to talk about positivity.

And anyway, there are tons of results in C*-algebra theory that require the partial order without ever making explicit reference to it in the statement.

[Eric Wieser]

If many statements don't mention the order, perhaps there should be a Prop-only typeclass that says "such an order could exist"

[Eric Wieser]

Sort of like docs#TopologicalSpace.MetrizableSpace doesn't actually globally induce a metric

[Jireh Loreaux]

I'm not really sure what that will buy us in practice.

[Jireh Loreaux]

And @MohanadAhmed, I realize sometimes things don't move as fast as we want, but please be patient about #6210, we'll get it sorted soon.

[Eric Wieser]

We always have the option of splitting #6210 in two: first add IsROrC.toPartialOrder as a scoped instance (which is uncontroversial), and then make a follow-up PR that makes it global

[MohanadAhmed]

(deleted)

[MohanadAhmed]

Jireh Loreaux said:

And MohanadAhmed, I realize sometimes things don't move as fast as we want, but please be patient about #6210, we'll get it sorted soon.

To be honest when I saw the 21 Feb 2021 date at the top of that poll thread, ................... well I saw a few years flashing by :joy: :joy: :rolling_on_the_floor_laughing:

[Eric Wieser]

It's worth remembering that that thread is only about bike-shedding whether to write open scoped ComplexOrder or not. That should be orthogonal to any mathematical concerns.

[MohanadAhmed]

On the more constructive note:
How about a class that just encodes the following:
conjTranspose v * v = 0 iff v = 0

[MohanadAhmed]

That would include Q R C , positive semidefinite matrices and so on

[MohanadAhmed]

I think it is called something like a Star Normed Field

[Jireh Loreaux]

You mean docs#CstarRing ?

[Eric Wieser]

That's not enough to work for the vector lemma, right? Because we're using dotProduct not *

[MohanadAhmed]

I meant mulitplication by *

[Eric Wieser]

That's not enough to prove dotProduct_star_self_eq_zero

[MohanadAhmed]

Something that gives:

variable [Fintype n]
variable [StarNormedField K]
lemma dot_product_star_self_eq_zero_iff (v : n → K) :
     Matrix.dotProduct (star v) v = 0 ↔  v = 0 := by sorry

[Eric Wieser]

[StarNormedField K] is spelt [NormedField K] [StarRing K] [CstarRing K]

[Jireh Loreaux]

Jireh Loreaux said:

I'm not really sure what that will buy us in practice.

Eric :up: ?

[MohanadAhmed]

Eric Wieser said:

[StarNormedField K] is spelt [NormedField K] [StarRing K] [CstarRing K]

Does that give dotProduct_star_self_eq_zero?

[Eric Wieser]

Jireh Loreaux said:

I'm not really sure what that will buy us in practice.

Only that you would be able to apply order-less statements without open scoped ComplexOrder

[MohanadAhmed]

MohanadAhmed said:

I meant mulitplication by *

Sorry yeah u are right vector inner product