Invariant subspaces of an endomorphism diagonal in a basis

An endomorphism f of a module that is diagonal in a basis b, so f (b i) = a i • b i, scales the i-th coordinate of every vector by the eigenvalue a i. When the eigenvalues are pairwise distinct, that is when a is injective, this pins down the invariant subspaces: an f-invariant subspace contains every basis vector occurring in one of its elements, hence is spanned by the basis vectors it contains, and a nonzero eigenvector of f is a multiple of a single basis vector. Neither is automatic for an operator with repeated eigenvalues.

The mechanism is that a coordinate of a vector w can be cleared without disturbing the others: f w - a j • w again lies in any invariant subspace containing w, and its k-th coordinate is (a k - a j) * b.repr w k, which vanishes at k = j and, by injectivity of a, at no other index where w had a nonzero coordinate. An induction on the number of nonzero coordinates then strips a vector down to a single basis vector.

Mathlib records the neighbouring facts in eigenspace language: eigenspaces for distinct eigenvalues are independent (Module.End.eigenspaces_iSupIndep), and eigenvectors for distinct eigenvalues are linearly independent (Module.End.eigenvectors_linearIndependent'); neither says what an invariant subspace looks like. TauCeti.iSup_inf_iInf_eigenspace_of_invariant does cut an invariant submodule out by eigenspaces, but for a commuting family over an algebraically closed field, in finite dimension, and with semisimple restrictions. A diagonalizing basis carries all of that for free and in coordinates, which is the form used here: no finiteness, no algebraic closedness, and the answer names the basis vectors involved.

Main results

• Module.Basis.repr_apply_of_apply_basis: the coordinates of f w are those of w scaled by the eigenvalues.
• Module.Basis.repr_eq_zero_of_weight_ne: a joint eigenvector has zero coordinate at a basis vector of a different joint weight.
• Module.Basis.self_mem_of_repr_ne_zero and Module.Basis.eq_span_self_mem: an invariant subspace contains every basis vector occurring in one of its elements, and is spanned by the basis vectors it contains.
• Module.Basis.exists_apply_eq_and_mem_span_singleton: a nonzero eigenvector of f is a multiple of a single basis vector, whose eigenvalue is its eigenvalue.

The coordinates are scaled by the eigenvalues

theorem Module.Basis.repr_apply_of_apply_basis {ι : Type u_1} {K : Type u_2} {V : Type u_3} [CommSemiring K] [AddCommMonoid V] [Module K V] {f : V →ₗ[K] V} {a : ι → K} (b : Basis ι K V) (hf : ∀ (i : ι), f (b i) = a i • b i) (w : V) (i : ι) : (b.repr (f w)) i = a i * (b.repr w) i

An endomorphism diagonal in a basis scales the coordinates: if f (b i) = a i • b i for every i, then f multiplies the i-th coordinate of every vector by a i.

theorem Module.Basis.repr_eq_zero_of_weight_ne {ι : Type u_1} {K : Type u_2} {V : Type u_3} {κ : Type u_4} [CommSemiring K] [IsCancelMulZero K] [AddCommMonoid V] [Module K V] {f : κ → End K V} {a : ι → κ → K} (b : Basis ι K V) (hf : ∀ (i : ι) (j : κ), (f j) (b i) = a i j • b i) {w : V} {c : κ → K} (hw : ∀ (j : κ), (f j) w = c j • w) {i : ι} (hi : a i ≠ c) : (b.repr w) i = 0

A joint eigenvector has zero coordinate at every basis vector of a different joint weight, when a family of endomorphisms is diagonal in the basis.

Invariant subspaces are spanned by basis vectors

theorem Module.Basis.self_mem_of_repr_ne_zero {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] {f : V →ₗ[K] V} {a : ι → K} {W : Submodule K V} (b : Basis ι K V) (hf : ∀ (i : ι), f (b i) = a i • b i) (ha : Function.Injective a) (hW : ∀ v ∈ W, f v ∈ W) {w : V} (hw : w ∈ W) {i : ι} (hi : (b.repr w) i ≠ 0) : b i ∈ W

An invariant subspace contains every basis vector occurring in one of its elements, when the endomorphism is diagonal in the basis with pairwise distinct eigenvalues: the coordinates of an element can then be separated by repeatedly clearing one of them.

theorem Module.Basis.eq_span_self_mem {ι : Type u_1} {K : Type u_2} {V : Type u_3} [Field K] [AddCommGroup V] [Module K V] {f : V →ₗ[K] V} {a : ι → K} {W : Submodule K V} (b : Basis ι K V) (hf : ∀ (i : ι), f (b i) = a i • b i) (ha : Function.Injective a) (hW : ∀ v ∈ W, f v ∈ W) : W = Submodule.span K {v : V | ∃ (i : ι), b i = v ∧ v ∈ W}

An invariant subspace is spanned by the basis vectors it contains, when the endomorphism is diagonal in the basis with pairwise distinct eigenvalues.

Eigenvectors are multiples of basis vectors

theorem Module.Basis.exists_apply_eq_and_mem_span_singleton {ι : Type u_1} {K : Type u_2} {V : Type u_3} [CommSemiring K] [IsCancelMulZero K] [AddCommMonoid V] [Module K V] {f : V →ₗ[K] V} {a : ι → K} (b : Basis ι K V) (hf : ∀ (i : ι), f (b i) = a i • b i) (ha : Function.Injective a) {w : V} (hw : w ≠ 0) {c : K} (hfw : f w = c • w) : ∃ (i : ι), a i = c ∧ w ∈ K ∙ b i

A nonzero eigenvector is a multiple of a single basis vector, when the endomorphism is diagonal in the basis with pairwise distinct eigenvalues, and its eigenvalue is the eigenvalue of that basis vector.