Documentation

Mathlib.LinearAlgebra.Eigenspace.Basic

Eigenvectors and eigenvalues #

This file defines eigenspaces, eigenvalues, and eigenvalues, as well as their generalized counterparts. We follow Axler's approach [axler2015] because it allows us to derive many properties without choosing a basis and without using matrices.

An eigenspace of a linear map f for a scalar μ is the kernel of the map (f - μ • id). The nonzero elements of an eigenspace are eigenvectors x. They have the property f x = μ • x. If there are eigenvectors for a scalar μ, the scalar μ is called an eigenvalue.

There is no consensus in the literature whether 0 is an eigenvector. Our definition of HasEigenvector permits only nonzero vectors. For an eigenvector x that may also be 0, we write x ∈ f.eigenspace μ.

A generalized eigenspace of a linear map f for a natural number k and a scalar μ is the kernel of the map (f - μ • id) ^ k. The nonzero elements of a generalized eigenspace are generalized eigenvectors x. If there are generalized eigenvectors for a natural number k and a scalar μ, the scalar μ is called a generalized eigenvalue.

The fact that the eigenvalues are the roots of the minimal polynomial is proved in LinearAlgebra.Eigenspace.Minpoly.

The existence of eigenvalues over an algebraically closed field (and the fact that the generalized eigenspaces then span) is deferred to LinearAlgebra.Eigenspace.IsAlgClosed.

References #

Tags #

eigenspace, eigenvector, eigenvalue, eigen

def Module.End.eigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :

The submodule eigenspace f μ for a linear map f and a scalar μ consists of all vectors x such that f x = μ • x. (Def 5.36 of [axler2015])

Equations
Instances For
    def Module.End.HasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (x : M) :

    A nonzero element of an eigenspace is an eigenvector. (Def 5.7 of [axler2015])

    Equations
    Instances For
      def Module.End.HasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (a : R) :

      A scalar μ is an eigenvalue for a linear map f if there are nonzero vectors x such that f x = μ • x. (Def 5.5 of [axler2015])

      Equations
      Instances For
        def Module.End.Eigenvalues {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) :

        The eigenvalues of the endomorphism f, as a subtype of R.

        Equations
        Instances For
          Equations
          • f = Subtype.val
          Instances For
            Equations
            • Module.End.Eigenvalues.instCoeOut = { coe := f }
            theorem Module.End.mem_eigenspace_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} :
            theorem Module.End.HasEigenvector.apply_eq_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} (hx : Module.End.HasEigenvector f μ x) :
            f x = μ x
            theorem Module.End.HasEigenvector.pow_apply {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {v : M} (hv : Module.End.HasEigenvector f μ v) (n : ) :
            (f ^ n) v = μ ^ n v
            theorem Module.End.HasEigenvalue.exists_hasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : Module.End.HasEigenvalue f μ) :
            ∃ (v : M), Module.End.HasEigenvector f μ v
            theorem Module.End.mem_spectrum_of_hasEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : Module.End.HasEigenvalue f μ) :
            μ spectrum R f
            theorem Module.End.eigenspace_div {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (a : K) (b : K) (hb : b 0) :
            def Module.End.generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :

            The generalized eigenspace for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the kernel of (f - μ • id) ^ k. (Def 8.10 of [axler2015]). Furthermore, a generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

            Equations
            Instances For
              @[simp]
              theorem Module.End.mem_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) (m : M) :
              m (Module.End.generalizedEigenspace f μ) k ((f - μ 1) ^ k) m = 0
              def Module.End.HasGeneralizedEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) (x : M) :

              A nonzero element of a generalized eigenspace is a generalized eigenvector. (Def 8.9 of [axler2015])

              Equations
              Instances For
                def Module.End.HasGeneralizedEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) :

                A scalar μ is a generalized eigenvalue for a linear map f and an exponent k ∈ ℕ if there are generalized eigenvectors for f, k, and μ.

                Equations
                Instances For
                  def Module.End.generalizedEigenrange {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) :

                  The generalized eigenrange for a linear map f, a scalar μ, and an exponent k ∈ ℕ is the range of (f - μ • id) ^ k.

                  Equations
                  Instances For
                    theorem Module.End.exp_ne_zero_of_hasGeneralizedEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } (h : Module.End.HasGeneralizedEigenvalue f μ k) :
                    k 0

                    The exponent of a generalized eigenvalue is never 0.

                    def Module.End.maximalGeneralizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :

                    The union of the kernels of (f - μ • id) ^ k over all k.

                    Equations
                    Instances For
                      @[simp]
                      theorem Module.End.mem_maximalGeneralizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (m : M) :
                      m Module.End.maximalGeneralizedEigenspace f μ ∃ (k : ), ((f - μ 1) ^ k) m = 0
                      noncomputable def Module.End.maximalGeneralizedEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :

                      If there exists a natural number k such that the kernel of (f - μ • id) ^ k is the maximal generalized eigenspace, then this value is the least such k. If not, this value is not meaningful.

                      Equations
                      Instances For

                        For an endomorphism of a Noetherian module, the maximal eigenspace is always of the form kernel (f - μ • id) ^ k for some k.

                        A generalized eigenvalue for some exponent k is also a generalized eigenvalue for exponents larger than k.

                        theorem Module.End.eigenspace_le_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } (hk : 0 < k) :

                        The eigenspace is a subspace of the generalized eigenspace.

                        All eigenvalues are generalized eigenvalues.

                        All generalized eigenvalues are eigenvalues.

                        @[simp]

                        Generalized eigenvalues are actually just eigenvalues.

                        Every generalized eigenvector is a generalized eigenvector for exponent finrank K V. (Lemma 8.11 of [axler2015])

                        Generalized eigenspaces for exponents at least finrank K V are equal to each other.

                        theorem Module.End.mapsTo_generalizedEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {g : Module.End R M} (h : Commute f g) (μ : R) (k : ) :
                        theorem Module.End.mapsTo_iSup_generalizedEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {g : Module.End R M} (h : Commute f g) (μ : R) :
                        Set.MapsTo g (⨆ (k : ), (Module.End.generalizedEigenspace f μ) k) (⨆ (k : ), (Module.End.generalizedEigenspace f μ) k)
                        theorem Module.End.isNilpotent_restrict_sub_algebraMap {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) (h : optParam (Set.MapsTo (f - (algebraMap R (Module.End R M)) μ) ((Module.End.generalizedEigenspace f μ) k) ((Module.End.generalizedEigenspace f μ) k)) ) :

                        The restriction of f - μ • 1 to the k-fold generalized μ-eigenspace is nilpotent.

                        theorem Module.End.isNilpotent_restrict_iSup_sub_algebraMap {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) (h : optParam (Set.MapsTo (f - (algebraMap R (Module.End R M)) μ) (⨆ (k : ), (Module.End.generalizedEigenspace f μ) k) (⨆ (k : ), (Module.End.generalizedEigenspace f μ) k)) ) :

                        The restriction of f - μ • 1 to the generalized μ-eigenspace is nilpotent.

                        theorem Module.End.disjoint_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ : R} {μ₂ : R} (hμ : μ₁ μ₂) (k : ) (l : ) :
                        theorem Module.End.disjoint_iSup_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ : R} {μ₂ : R} (hμ : μ₁ μ₂) :
                        Disjoint (⨆ (k : ), (Module.End.generalizedEigenspace f μ₁) k) (⨆ (k : ), (Module.End.generalizedEigenspace f μ₂) k)
                        theorem Module.End.injOn_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) :
                        Set.InjOn (fun (x : R) => ⨆ (k : ), (Module.End.generalizedEigenspace f x) k) {μ : R | ⨆ (k : ), (Module.End.generalizedEigenspace f μ) k }

                        The eigenspaces of a linear operator form an independent family of subspaces of M. That is, any eigenspace has trivial intersection with the span of all the other eigenspaces.

                        theorem Module.End.eigenvectors_linearIndependent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) (μs : Set R) (xs : μsM) (h_eigenvec : ∀ (μ : μs), Module.End.HasEigenvector f (μ) (xs μ)) :
                        LinearIndependent (ι := μs) R xs

                        Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent. (Lemma 5.10 of [axler2015])

                        We use the eigenvalues as indexing set to ensure that there is only one eigenvector for each eigenvalue in the image of xs.

                        theorem Module.End.generalizedEigenspace_restrict {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (p : Submodule R M) (k : ) (μ : R) (hfp : xp, f x p) :

                        If f maps a subspace p into itself, then the generalized eigenspace of the restriction of f to p is the part of the generalized eigenspace of f that lies in p.

                        theorem Submodule.inf_generalizedEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (p : Submodule R M) {k : } {μ : R} (hfp : xp, f x p) :
                        theorem Module.End.eigenspace_restrict_le_eigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) {p : Submodule R M} (hfp : xp, f x p) (μ : R) :

                        If p is an invariant submodule of an endomorphism f, then the μ-eigenspace of the restriction of f to p is a submodule of the μ-eigenspace of f.

                        Generalized eigenrange and generalized eigenspace for exponent finrank K V are disjoint.

                        theorem Module.End.eigenspace_restrict_eq_bot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hfp : xp, f x p) {μ : R} (hμp : Disjoint (Module.End.eigenspace f μ) p) :

                        If an invariant subspace p of an endomorphism f is disjoint from the μ-eigenspace of f, then the restriction of f to p has trivial μ-eigenspace.

                        The generalized eigenspace of an eigenvalue has positive dimension for positive exponents.

                        A linear map maps a generalized eigenrange into itself.

                        theorem Module.End.iSup_generalizedEigenspace_le_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (t : R) :
                        ⨆ (k : ), (Module.End.generalizedEigenspace f μ) k ⨆ (k : ), (Module.End.generalizedEigenspace (t f) (t * μ)) k
                        theorem Module.End.iSup_generalizedEigenspace_inf_le_add {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f₁ : Module.End R M) (f₂ : Module.End R M) (μ₁ : R) (μ₂ : R) (h : Commute f₁ f₂) :
                        (⨆ (k : ), (Module.End.generalizedEigenspace f₁ μ₁) k) ⨆ (k : ), (Module.End.generalizedEigenspace f₂ μ₂) k ⨆ (k : ), (Module.End.generalizedEigenspace (f₁ + f₂) (μ₁ + μ₂)) k
                        theorem Module.End.map_smul_of_iInf_generalizedEigenspace_ne_bot {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {L : Type u_1} {F : Type u_2} [SMul R L] [FunLike F L (Module.End R M)] [SMulHomClass F R L (Module.End R M)] (f : F) (μ : LR) (h_ne : ⨅ (x : L), ⨆ (k : ), (Module.End.generalizedEigenspace (f x) (μ x)) k ) (t : R) (x : L) :
                        μ (t x) = t μ x
                        theorem Module.End.map_add_of_iInf_generalizedEigenspace_ne_bot_of_commute {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {L : Type u_1} {F : Type u_2} [Add L] [FunLike F L (Module.End R M)] [AddHomClass F L (Module.End R M)] (f : F) (μ : LR) (h_ne : ⨅ (x : L), ⨆ (k : ), (Module.End.generalizedEigenspace (f x) (μ x)) k ) (h : ∀ (x y : L), Commute (f x) (f y)) (x : L) (y : L) :
                        μ (x + y) = μ x + μ y