The Perron-Frobenius theorem states that any matrix over the reals with positive entries has at least one positive eigenvalue (and a bit more). The easiest proof that I know of runs as follows: any $M \in M_n(\mathbb{R}_{>0})$ induces a map from the non-negative orthant of the sphere (i.e., $S^{n-1} \cap (\mathbb{R}_{\ge 0}^n)$) to itself via $v \mapsto Mv/\|Mv\|$. This orthant is homeomorphic to the disk $B^{n-1}$, and so we get a map $\tilde{M}: B^{n-1} \to B^{n-1}$. The Brouwer fixed-point theorem gives a fixed-point of this map, i.e. an eigenvector of $M$ with some necessarily positive eigenvalue as desired.
If we want to extend this theorem to real closed fields, we could come up with a non-topological argument, which seems a bit more involved.
However, it seems like there may be a model-theoretic elementary equivalence argument that can be used here, but I know little about this. Roughly speaking the steps that I think I need are as follows:
- Give a first-order predicate for positivity (and hence ordering).
- Write down the first-order statement of Perron-Frobenius, that is, something like $(\forall a_{11}, \cdots, a_{nn} > 0)(\exists \lambda > 0)(\det(A-\lambda I) = 0)$ which is a perfectly valid first-order statement, assuming part 1.
- Use elementary equivalence of real closed fields in the first-order language of (ordered?) fields, coupled with the truth of the statement for $F = \mathbb{R}$, to conclude that the statement holds for all real fields.
I'm currently having a bit of trouble being precise in part 1, and verifying that I'm working in the correct language in part 3.
In part 1 it seems like for all real closed fields the defintion $a \le b \Leftrightarrow (\exists x)(a + x^2 = b)$ gives a valid order relation. Is this true?
For part 3, Wikipedia states that the real closed fields are elementarily equivalent to the reals in the first-order language of fields (as opposed to, say, ordered fields). To my eyes, the order predicate used in part 1 is in the language of fields, and so I think that I've got a valid statement of Perron-Frobenius in the first-order language of fields that does what I want for all real closed fields. But I'm not sure if the elementary equivalence is over the language of fields or ordered fields.
Is all this enough to conclude Perron-Frobenius for all real closed fields?