Assuming Bishop's constructive mathematics, is it true that any real-valued square matrix with distinct roots of the characteristic polynomial can be diagonalized? By distinct, I mean apart: $x \neq y \triangleq \exists q \in \mathbb{Q}.|x - y| > q$. (There may be similar defnitions)

For the case $n=2$, it seems true since we can deduce $a_{11} - \lambda_j \neq 0 \lor a_{22} - \lambda_j \neq 0$ for any $j = 1, 2$ where $a_{ii}, i=1,2$ are the diagonal elements and $\lambda_j$s are the roots of the characteristic polynomial. It then allows multiplying by a nonzero number and, using the property that $(a_{11} - \lambda_j)(a_{22} - \lambda_j) = a_{12}a_{21}$, solving the respective system of linear equations and consequently finding an eigenvector: $A v = \lambda_j v$.

Already for the case $n=3$, the argument seems not to work and one cannot proceed without some case distinction on reals. This work addresses the problem in Lemma 1.5, but they seem to assume $xy = 0 \implies x =0 \lor y=0$ which is not valid constructively.

Coquand and Lombardi in Theorem 2.3 constructed an effective procedure of finding eigenvectors of a projection matrix. I suspected that something like this could be done for general matrices where it is known beforehand that the roots of the characteristic polynomial are distinct.

Lombardi and Quitte addressed the problem on page 100 (top). Also in Proposition 5.3, they claim that

$$\prod_{i=1}^n ( (A - \lambda_i I)_{1 \dots n-1, 1 \dots n-1} ) \neq 0$$

by "exhibiting" the companion matrix of $\lambda^n - 1$. Their language is a bit obscure. However, it seems they imply the following lemma:

Let $A = M(\mathbb{R},n)$, and suppose that the roots $\lambda_1, \dots, \lambda_n$ of the charteristic polynomial for $A$ are mutually apart. Then, for every root $\lambda_j$ of the characteristic polynomial, there is a principal submatrix of $A - \lambda_j I$ of size $(n-1) \times (n-1)$ which is invertible.

  • $\begingroup$ Do you mean by "distinct" "not equal" or "apart"? Also, what is your definition of "eigenvalue"? A real number $\lambda$ such that there exists a vector $v$ with at least one component apart from zero such that $Av = \lambda v$? In this case, if you assume your $n$ eigenvalues to be apart, you at least obtain a linearly independent family of eigenvectors. (Unfortunately, I don't see how these are a generating family.) $\endgroup$ Dec 19 '16 at 14:53
  • $\begingroup$ @IngoBlechschmidt This is definitely not what I mean. Please see edit. $\endgroup$
    – Rubi Shnol
    Dec 19 '16 at 15:00
  • $\begingroup$ The suggestion of Lombardi and Quitte is probably to use Cramer's rule to find the eigenvectors, seeing that each eigenspace is 1-dimensional. $\endgroup$ Dec 19 '16 at 18:28

The following works constructively over an arbitrary local ring $R$ (constructively, $\mathbb{R}$ is a local ring).

Assume that you matrix $M$ is canceled by a polynomial $Q$, of degree $m$ (with leading coefficent $1$), that $Q$ can be factored into

$$Q= \prod^m_{i=1}(X-q_i)$$

and that for each $i \neq j$, $(q_i - q_j)$ is invertible (in the case of $\mathbb{R}$ it just means that $q_i$ and $q_j$ are appart).

Then one can diagonalize $M$. In particular it can be applied when you have some multiplicites in your eigenvalue as long as the minimal polynomial has simple roots.

Let $$P_i = \frac{\displaystyle \prod_{j \neq i} (X-q_j)}{ \displaystyle \prod_{j \neq i} (q_i-q_j)} $$

i.e. $P_i(q_i)=1$ and if $i \neq j$ , $P_i(q_j)=0$

It is constructive that a polynomial is divisibe by $Q$ if and only if it vanishes at all the $q_i$ (basically because polynomial division by a polynomial with unit leading coefficient works well). Hence you can easily check that:

$(P_i)^2 - P_i$

$P_i P_j$

$1-\sum_i P_i$

$X-\sum_i q_i P_i$

are all divisible by $Q$ and hence cancel $M$. So the $P_i(M)$ form a complete family of projection, and $M = \sum q_i P_i(M)$ and you get the spectral decomposition of $M$.

At this point, if you already know how to find eigen vectors for projections then you are done: the range of each $P_i$ are in direct sum so you just find a basis of each of these subspaces and you get your diagonal basis.

I have not read the paper by Coquand & Lombardi you are quoting so I'm not sure what is their method for the last step. I know of a process for this that work for local ring of 'zero residual characteristic' (i.e. in which integer are invertible sot ) I'm not sure what happen in the fully general case, but it is already enough for the case of $\mathbb{R}$.

  • $\begingroup$ So if your canceling polynomial is of the form $\prod (X-a_i)^{k_i}$ with $a_i$ appart from each other then by the argument above you can decompose you space into a direct sum of subspace on which you endomorphism is $a_i Id +N$ with $N$ nilpotent of order at most $k_i$. So the question is brought to the question of reducing nilpotent endomorphisms... I don't have much thought about this (excpte that it will require additional assumptions...) $\endgroup$ Dec 20 '16 at 14:55
  • $\begingroup$ Ok, does it mean that the case with repeated roots is more subtle even though it is known which roots are repeated? After a comment on this, I think, we can wrap up and I accept this answer. $\endgroup$
    – Rubi Shnol
    Dec 20 '16 at 14:59
  • $\begingroup$ I'm not sure I understand what you say, let me clarify what I was saying: the argument I've given above start with any polynomial candeling $M$ with simple roots ($m$ is not the size of the matrix) so you can have multiplicities in your eigen value without chaning anythings. Where things might become a little more complicated is if you have non trivial nilpotnent block (i.e. exponent $k_i$ in your cancelling polynomial) and in this case all I can says is that one need one more step in the argument which is the reduction of nilpotent matrices (to be continued...) $\endgroup$ Dec 20 '16 at 15:07
  • 1
    $\begingroup$ If you have a matrix such that $N^k = 0$, it corresponds to a case where you perfectly know all the eigen values and their multiplicites (they are all zero). But it is not clear what kind of reduction you can expect for nilpotent matrix constructively. If you want a full Jordan form then you clearly need additional assumption: for a matrix in Jordan form all the $Im N^k$ are nice complemented subspaces so this at least has to be an assumption. but I can imagine than one can manage something from assumptions on the singular values instead... $\endgroup$ Dec 20 '16 at 15:12

Without polishing up on linear algebra, the not very subtle topological answer is yes. Different eigenvalues $\lambda_i$ mean unique solutions (the eigenvectors) on the unit hemisphere, of the kernel equations $(A-\lambda_i I)v=0$.

These solutions can be found by approximation using compactness and uniform continuity.

With the $n$ different eigenvectors at hand, diagonalization should give no trouble at all.

  • $\begingroup$ "Different eigenvalues $\lambda_i$ mean unique solutions (the eigenvectors) on the unit hemisphere" how do they mean that? $\endgroup$
    – Rubi Shnol
    Dec 19 '16 at 17:08
  • $\begingroup$ eigenvectors with different eigenvalues are linearly independent. $\endgroup$ Dec 19 '16 at 17:19
  • $\begingroup$ since there are already $n$ eigenvectors, the $\lambda_i$ kernel dim must be 1, meaning unique solution on the unit hemisphere. $\endgroup$ Dec 19 '16 at 17:28
  • $\begingroup$ ? It might help you to read the book Constructive Analysis by Bishop & Bridges, to get a feel for the basics of constructive reasoning. It would take me too much time and space to do that here. $\endgroup$ Dec 19 '16 at 19:47
  • 1
    $\begingroup$ Like I said, this is becoming more a question about constructive reasoning in general. The theorem you ask for is given above, under the conditions that you provided. If there are less than $n$ different eigenvalues, things become more complicated. So in general settings, for instance outside of $\mathbb{R}^n$, finding eigenvectors becomes a different ball game. But that is not what you asked. $\endgroup$ Dec 19 '16 at 20:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.