Matrix diagonalization and eigenvector computation constructively

Question

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.

Answer 1

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}$.

Answer 2

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.