Separating eigenspace summands

Suppose p is a sum ⨆ j ∈ s, W j of subspaces on which an endomorphism A already acts by scalars, one scalar g j per summand, and suppose the scalar g k of one distinguished summand is attained by no other. Then that summand is exactly the g k-eigenspace of A inside p: no eigenvector of eigenvalue g k hides in the other summands, because eigenspaces for distinct eigenvalues are independent. This is how a weight space is recovered from an eigenspace of a single operator once a decomposition separating the weights is available.

Main results

• TauCeti.biSup_inf_eigenspace_eq_self: a summand whose scalar is attained only by itself is cut out by the corresponding eigenspace.

theorem TauCeti.biSup_inf_eigenspace_eq_self {K : Type u} {V : Type v} [CommRing K] [IsDomain K] [AddCommGroup V] [Module K V] [Module.IsTorsionFree K V] {ι : Type w} (A : Module.End K V) (W : ι → Submodule K V) (g : ι → K) {s : Set ι} (hW : ∀ j ∈ s, W j ≤ A.eigenspace (g j)) {k : ι} (hk : k ∈ s) (hg : ∀ j ∈ s, j ≠ k → g j ≠ g k) : (⨆ j ∈ s, W j) ⊓ A.eigenspace (g k) = W k

Separated summands are cut out by their eigenspaces. If every W j, for j in a set s, consists of eigenvectors of A of eigenvalue g j, and if the scalar g k of a distinguished index k ∈ s is attained by no other index of s, then meeting the sum ⨆ j ∈ s, W j with the g k-eigenspace of A returns W k exactly.

In particular no eigenvector of eigenvalue g k in the sum lies outside W k.