Eigenvalues, eigenvectors, and eigenspaces of linear endomaps

[lowasser]

It seemed like an appropriate point to inaugurate a spectral-theory module.

Builds on #1764 .

[fredrik-bakke]

I'm not familiar enough with the subject of spectral theory to make an informed decision on whether eigenvalues and eigenvectors should go into that namespace. Could you please write an introduction to this namespace meriting the inclusion of eigenvalues and eigenvectors? Something akin to the introduction of univalent-combinatorics or set-theory or modal-type-theory

[lowasser]

I'm not familiar enough with the subject of spectral theory to make an informed decision on whether eigenvalues and eigenvectors should go into that namespace. Could you please write an introduction to this namespace meriting the inclusion of eigenvalues and eigenvectors? Something akin to the introduction of univalent-combinatorics or set-theory or modal-type-theory

Done.

[lowasser]

(tl;dr: spectral theory is the field that studies eigenvectors, eigenvalues, and their generalizations)

[malarbol]

Have you considered defining the eigen(modules|spaces) at r as the kernel of f - r id? (so the submodule laws follow from the kernel properties); and then define:

• an eigenvalue r : R is a scalar with nontrivial eigenspace;
• an eigenvector v : V is a nonzero vector of some eigenspace (and you can prove that the eigenvalue is determined by the eigenvector).

[lowasser]

Have you considered defining the eigen(modules|spaces) at r as the kernel of f - r id? (so the submodule laws follow from the kernel properties);

I'm certainly on board with this part;

and then define:

• an eigenvalue r : R is a scalar with nontrivial eigenspace;
• an eigenvector v : V is a nonzero vector of some eigenspace (and you can prove that the eigenvalue is determined by the eigenvector).

I'm not sure I see yet how to define these things for arbitrary spaces (largely because the notion of "nonzero" generally requires a space-specific notion of apartness which I don't want to demand from these spaces yet)

[malarbol]

I'm not sure I see yet how to define these things for arbitrary spaces (largely because the notion of "nonzero" generally requires a space-specific notion of apartness which I don't want to demand from these spaces yet)

I suspected so, but I was hoping the hypothesis on Heyting fields would be enough to characterize nonzero vectors. Maybe using duality (e.g. a vector v is zero if and only if for all linear forms f, f v is zero in K)? We have 0 ≠ 1 in the Heyting field and there should be some relation between pairs (v , f) of vectors v and linear forms f such that f v = 1 that maybe we could leverage?

[lowasser]

Defining nonzero vectors is the important one, and it might be plausible to define a nonzero vector as c * v = 0 => c = 0, though that definition certainly wouldn't work for arbitrary commutative rings.

If there is a viable definition here, I don't feel the need for it here; I don't really see where "zero is an eigenvalue for every vector" is a problem. Certainly I think things line up better if we keep the definition to "c is an eigenvalue with eigenvector v if f v - c * v = 0`.

[malarbol]

Defining nonzero vectors is the important one, and it might be plausible to define a nonzero vector as c * v = 0 => c = 0, though that definition certainly wouldn't work for arbitrary commutative rings.

I don't know much about spectral theory in arbitrary commutative rings but, for vector spaces, the fact that eigenvectors must be nonzero always seemed quite relevant.

If there is a viable definition here, I don't feel the need for it here; I don't really see where "zero is an eigenvalue for every vector" is a problem.

That's not it. The problem is "the zero vector is an eigenvector for all values", or, put it another way, "any value is an eigenvalue for the zero vector". So I thing the term eigen is not correctly applied.