Module.End.iSup_generalizedEigenspace_restrict_eq_top
theorem Module.End.iSup_generalizedEigenspace_restrict_eq_top :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
{f : Module.End K V} [inst_3 : FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p),
⨆ μ, ⨆ k, (f.generalizedEigenspace μ) k = ⊤ →
⨆ μ, ⨆ k, (Module.End.generalizedEigenspace (LinearMap.restrict f h) μ) k = ⊤
This theorem states that in a finite-dimensional vector space, if the generalized eigenspaces of a linear endomorphism span the entire vector space, then the same holds true for its restriction to any invariant submodule. In other words, if the direct sum of the generalized eigenspaces for every eigenvalue of a linear endomorphism equals the whole space, then the direct sum of the generalized eigenspaces for every eigenvalue of its restricted endomorphism to an invariant submodule also equals the entire submodule.
More concisely: If a linear endomorphism of a finite-dimensional vector space and its restriction to any invariant submodule have identical spans of generalized eigenspaces for all eigenvalues, then these spans equal the entire vector space and submodule, respectively.
|
Module.End.exists_eigenvalue
theorem Module.End.exists_eigenvalue :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : IsAlgClosed K] [inst_4 : FiniteDimensional K V] [inst_5 : Nontrivial V] (f : Module.End K V),
∃ c, f.HasEigenvalue c
This theorem states that for any finite dimensional vector space `V` over an algebraically closed field `K`, every linear endomorphism `f` from `V` to `V` has an eigenvalue. An eigenvalue here is a scalar `c` from the field `K` such that there exists a vector in `V` which is scaled by `f` by the factor of `c`. In other words, for any transformation that can be represented as a square matrix (the linear endomorphism), if the vector space has a finite basis and the field of scalars is algebraically closed (like the field of complex numbers), then there exists a scalar such that subtracting it along the diagonal of the matrix (the linear transformation) produces a matrix that is not invertible. This is a fundamental result in linear algebra, known as the Fundamental Theorem of Algebra.
More concisely: Every linear endomorphism of a finite-dimensional vector space over an algebraically closed field has an eigenvalue.
|
Module.End.iSup_generalizedEigenspace_eq_top
theorem Module.End.iSup_generalizedEigenspace_eq_top :
∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
[inst_3 : IsAlgClosed K] [inst_4 : FiniteDimensional K V] (f : Module.End K V),
⨆ μ, ⨆ k, (f.generalizedEigenspace μ) k = ⊤
The theorem `Module.End.iSup_generalizedEigenspace_eq_top` states that for any field `K` which also is algebraically closed, and for any finite dimensional vector space `V` over `K`, for any linear endomorphism `f` of `V`, the direct sum (or sup) of the generalized eigenspaces of `f` spans the whole space `V`. This means that every vector in `V` can be written as a linear combination of vectors in the generalized eigenspaces of `f` for some eigenvalue `μ` and some non-negative integer `k`. This theorem is essentially a restatement of one of the key results in linear algebra about the structure of linear operators on finite-dimensional vector spaces over algebraically closed fields.
More concisely: For any finite-dimensional vector space over an algebraically closed field and any linear endomorphism, the direct sum of the generalized eigenspaces spans the entire space.
|