Determinant of Complex Hermitian Matrix is a Real Number

Stream: new members

[MohanadAhmed]

A complex Hermitian matrix has real eigenvalues and real determinants. However, the way the determinant is defined it has the same type as the matrix elements. Hence, the following lemma statement does not type check:

import linear_algebra.matrix.pos_def
import linear_algebra.matrix.spectrum
import linear_algebra.matrix.nondegenerate
import linear_algebra.matrix.determinant
import data.complex.basic

variables {m: Type*}[fintype m][decidable_eq m]

lemma det_pos{A: matrix m m ℂ} (hA: matrix.pos_def A)  :
 0 < (A.det) :=
begin

end

The error given is shown below. Which makes sense, I mean as far as I know complex numbers have no less than comparison.

failed to synthesize type class instance for
m : Type u_1,
_inst_1 : fintype m,
_inst_2 : decidable_eq m,
A : matrix m m ℂ,
hA : A.pos_def
⊢ has_lt ℂ

Is there a way to tell lean, "hey this is going to be a real number, please don't stand in the way" ?

[MohanadAhmed]

My current work around is

lemma det_pos{A: matrix m m ℂ} (hA: matrix.pos_def A)  :
 0 < (A.det).re ∧ (A.det).im = 0  :=
begin

end

But this does not feel as clean as just saying this is a real number that is going to be less than zero

[MohanadAhmed]

And it will not work in places that require the determinant itself to be positive for example.

[Ruben Van de Velde]

You could do something like \exists r : R, A.det = r \and 0 < r, where r is just A.det.re, but I'm not sure that will help much

[Damiano Testa]

In the long run, if you are planning to work with hermitian matrices extensively, it might make sense to define a type of HM, construct a real-valued determinant on them and prove that it's coercion to ℂ equals the determinant of the underlying matrix. It will take some time...

[Damiano Testa]

Ultimately, this is not too different from Ruben's suggestion, it simply bundles up the information instead of flattening it out.

[Eric Wieser]

docs#complex.strict_ordered_comm_ring exists

[Eric Wieser]

open_locale complex_order will make your statement work

[Eric Wieser]

Your statement is probably true more generally for a star_ordered_ring

[Kevin Buzzard]

Eric Wieser said:

open_locale complex_order will make your statement work

Just to be clear -- this puts some hideous noncanonical order on the complexes.

The mathematical approach would be to do what Ruben suggests, prove that 0 < A.det.re and then prove that A.det = A.det.re (the latter will be coerced back to a complex number)

[MohanadAhmed]

docs#complex.strict_ordered_comm_ring

That looks like some neat trickery. Any gotchas or side effects to be wary of???

[Eric Wieser]

Just to be clear -- this puts some hideous noncanonical order on the complexes.

Indeed, but it's the order that we decided to use for docs#complex.star_ordered_ring, and mathlib does use it

[Eric Wieser]

So I think this is precisely the type of situation this hack was designed for, even if we might eventually want to redesign it

[MohanadAhmed]

@Kevin Buzzard

If I use the mathematical approach you describe:
Does that mean I will be calling norm cast everywhere I use this? For example I want to use the ne_of_lt on det_pos To prove that the determinant is_unit??

[Kevin Buzzard]

You should define real_det (defined for complex hermitian matrices) as well as det (defined for all matrices) and then prove that when you apply the obvious map from R to C which in Lean is not "the identity" or "the inclusion" but a genuine function, with an invisible name indicated by an up-arrow, then it sends real_det to det. Then you just use whichever function is appropriate.

[Eric Wieser]

I'd argue you should prove a single lemma for star_ordered_ring, and recover the .det.re version as a special case for complex

[Kevin Buzzard]

What does the pathological ordering on the complexes have to do with this question? This is mathematics.

[Eric Wieser]

The pathological ordering is the one that lets us generalize x * conj x >= 0so that it applies to the reals and the complex numbers

[Eric Wieser]

You could argue that's the wrong thing to generalize, but it's too late for that; we already did the generalization!

[Eric Wieser]

Eric Wieser said:

I'd argue you should prove a single lemma for star_ordered_ring, and recover the .det.re version as a special case for complex

Maybe I'm wrong and is_R_or_C is the right assumption after all

[Kevin Buzzard]

I understand that but what I am saying is that it's not the right answer here. In the Langlands program one wants to consider unitary and Hermitian matrices in more general situations, where there is more than one ordering on the base, and yet we definitely want the assertion that the determinant of the matrix with coefficients in the bigger field is taking values in the smaller field, so for this a modified det is needed. We have something like docs#complex.norm_sq which adopts the same approach.

[Eric Wieser]

I think this maybe that statement should be (h : is_skew_adjoint M) : is_self_adjoint M.det?

[Kevin Buzzard]

This sounds much more like what I was envisaging.

[Kevin Buzzard]

In Langlands you might consider fields like the splitting field of $x^2-2$. This is a field $\mathbb{Q}(x)$ with $x^2=2$ but $x$ is neither "the positive square root of 2" or "the negative square root of 2", it is a square root of 2 whose sign has not been determined yet. There are two maps from this field to the reals, one sending $x$ to $+\sqrt{2}$ and one sending it to $-\sqrt{2}$. There is a notation of "totally positive element", which means "positive under both embeddings" in this case, so for example $x$ is not totally positive but $x+37$ is (because both $37+\sqrt{2}$ and $37-\sqrt{2}$ are positive). In this situation it's really important that one does not fix an ordering on the base field, and yet exactly the question which Mohanad raises arises when one is doing unitary matrices over a totally imaginary extension $K$ of $\mathbb{Q}(x)$ (which will be a star_ring), for example the splitting field of $y^2+1$ over $\mathbb{Q}(x)$ (and again it's important not to identify $y$ with $+i$ or $-i$, this is the problem I have with is_R_or_C; the star exists even without this identification). Here the statement would be that the determinant was totally positive, but if we have some fixed order on everything then it will be difficult to make that statement cleanly.

[Kevin Buzzard]

docs#is_self_adjoint

[Eric Wieser]

Just to note, my complex_order comments above are a distraction; after all this we don't have the instance for is_R_or_C anyway!

[Eric Wieser]

(I lied about is_skew_adjoint, we don't actually have it, only the add_subgroup version docs#skew_adjoint)

[Kevin Buzzard]

Yeah, is_self_adjoint looks perfect for this. Then there should be some lemma stating that if you're a self-adjoint complex number then you're the coercion of a real number, and you can build real_det from this.

[Eric Wieser]

docs#complex.conj_eq_iff_re

[Eric Wieser]

⇑(star_ring_end ℂ) z = z is defeq to is_self_adjoint z

[Eric Wieser]

And if you have h : is_self_adjoint z then h.star_eq : star z = z

[Eric Wieser]

The star vs star_ring_end (aka conj) thing is annoying (at least in this scenario)

[Eric Wieser]

docs#star_ring_end_apply is deliberately not a simp lemma, because for complex analysis it's convenient to have conj be the bundled version, but elsewhere all the lemmas are about the unbundled version

[Eric Wieser]

Eric Wieser said:

I think this maybe that statement should be (h : is_hermitian M) : is_self_adjoint M.det?

Note this result follows trivially from docs#matrix.det_conj_transpose