HepLean 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.genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :

The submodule genEigenspace f μ k for a linear map f, a scalar μ, and a number k : ℕ∞ is the kernel of (f - μ • id) ^ k if k is a natural number (see Def 8.10 of [axler2015]), or the union of all these kernels if k = ∞. A generalized eigenspace for some exponent k is contained in the generalized eigenspace for exponents larger than k.

Equations
Instances For
    theorem Module.End.mem_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} {x : M} :
    x (f.genEigenspace μ) k ∃ (l : ), l k x LinearMap.ker ((f - μ 1) ^ l)
    theorem Module.End.genEigenspace_directed {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} :
    Directed (fun (x1 x2 : Submodule R M) => x1 x2) fun (l : { l : // l k }) => (f.genEigenspace μ) l
    theorem Module.End.mem_genEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } {x : M} :
    x (f.genEigenspace μ) k x LinearMap.ker ((f - μ 1) ^ k)
    theorem Module.End.mem_genEigenspace_top {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} :
    x (f.genEigenspace μ) ∃ (k : ), x LinearMap.ker ((f - μ 1) ^ k)
    theorem Module.End.genEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } :
    (f.genEigenspace μ) k = LinearMap.ker ((f - μ 1) ^ k)
    theorem Module.End.genEigenspace_eq_iSup_genEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ∞) :
    (f.genEigenspace μ) k = ⨆ (l : { l : // l k }), (f.genEigenspace μ) l
    theorem Module.End.genEigenspace_top {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :
    (f.genEigenspace μ) = ⨆ (k : ), (f.genEigenspace μ) k
    theorem Module.End.genEigenspace_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} :
    (f.genEigenspace μ) 1 = LinearMap.ker (f - μ 1)
    @[simp]
    theorem Module.End.mem_genEigenspace_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} :
    x (f.genEigenspace μ) 1 f x = μ x
    theorem Module.End.mem_genEigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} :
    x (f.genEigenspace μ) 0 x = 0
    @[simp]
    theorem Module.End.genEigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} :
    (f.genEigenspace μ) 0 =
    @[simp]
    theorem Module.End.genEigenspace_zero_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (k : ) :
    (f.genEigenspace 0) k = LinearMap.ker (f ^ k)
    def Module.End.HasUnifEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ∞) (x : M) :

    Let M be an R-module, and f an R-linear endomorphism of M, and let μ : R and k : ℕ∞ be given. Then x : M satisfies HasUnifEigenvector f μ k x if x ∈ f.genEigenspace μ k and x ≠ 0.

    For k = 1, this means that x is an eigenvector of f with eigenvalue μ.

    Equations
    • f.HasUnifEigenvector μ k x = (x (f.genEigenspace μ) k x 0)
    Instances For
      def Module.End.HasUnifEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ℕ∞) :

      Let M be an R-module, and f an R-linear endomorphism of M. Then μ : R and k : ℕ∞ satisfy HasUnifEigenvalue f μ k if f.genEigenspace μ k ≠ ⊥.

      For k = 1, this means that μ is an eigenvalue of f.

      Equations
      • f.HasUnifEigenvalue μ k = ((f.genEigenspace μ) k )
      Instances For
        def Module.End.UnifEigenvalues {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (k : ℕ∞) :

        Let M be an R-module, and f an R-linear endomorphism of M. For k : ℕ∞, we define UnifEigenvalues f k to be the type of all μ : R that satisfy f.HasUnifEigenvalue μ k.

        For k = 1 this is the type of all eigenvalues of f.

        Equations
        • f.UnifEigenvalues k = { μ : R // f.HasUnifEigenvalue μ k }
        Instances For
          def Module.End.UnifEigenvalues.val {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (k : ℕ∞) :
          f.UnifEigenvalues kR

          The underlying value of a bundled eigenvalue.

          Equations
          • f k = Subtype.val
          Instances For
            instance Module.End.UnifEigenvalues.instCoeOut {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (k : ℕ∞) :
            CoeOut (f.UnifEigenvalues k) R
            Equations
            instance Module.End.UnivEigenvalues.instDecidableEq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [DecidableEq R] (f : Module.End R M) (k : ℕ∞) :
            DecidableEq (f.UnifEigenvalues k)
            Equations
            theorem Module.End.HasUnifEigenvector.hasUnifEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} {x : M} (h : f.HasUnifEigenvector μ k x) :
            f.HasUnifEigenvalue μ k
            theorem Module.End.HasUnifEigenvector.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 : f.HasUnifEigenvector μ 1 x) :
            f x = μ x
            theorem Module.End.HasUnifEigenvector.pow_apply {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {v : M} (hv : f.HasUnifEigenvector μ 1 v) (n : ) :
            (f ^ n) v = μ ^ n v
            theorem Module.End.HasUnifEigenvalue.exists_hasUnifEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} (hμ : f.HasUnifEigenvalue μ k) :
            ∃ (v : M), f.HasUnifEigenvector μ k v
            theorem Module.End.HasUnifEigenvalue.pow {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (h : f.HasUnifEigenvalue μ 1) (n : ) :
            (f ^ n).HasUnifEigenvalue (μ ^ n) 1
            theorem Module.End.HasUnifEigenvalue.isNilpotent_of_isNilpotent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {f : Module.End R M} (hfn : IsNilpotent f) {μ : R} (hf : f.HasUnifEigenvalue μ 1) :

            A nilpotent endomorphism has nilpotent eigenvalues.

            See also LinearMap.isNilpotent_trace_of_isNilpotent.

            theorem Module.End.HasUnifEigenvalue.mem_spectrum {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasUnifEigenvalue μ 1) :
            μ spectrum R f
            theorem Module.End.hasUnifEigenvalue_iff_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} :
            f.HasUnifEigenvalue μ 1 μ spectrum K f
            theorem Module.End.HasUnifEigenvalue.of_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} :
            μ spectrum K ff.HasUnifEigenvalue μ 1

            Alias of the reverse direction of Module.End.hasUnifEigenvalue_iff_mem_spectrum.

            theorem Module.End.genEigenspace_div {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (a b : K) (hb : b 0) :
            (f.genEigenspace (a / b)) 1 = LinearMap.ker (b f - a 1)
            def Module.End.genEigenrange {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 if k is a natural number, or the infimum of these ranges if k = ∞.

            Equations
            Instances For
              theorem Module.End.genEigenrange_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } :
              f.genEigenrange μ k = LinearMap.range ((f - μ 1) ^ k)
              theorem Module.End.HasUnifEigenvalue.exp_ne_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } (h : f.HasUnifEigenvalue μ k) :
              k 0

              The exponent of a generalized eigenvalue is never 0.

              noncomputable def Module.End.maxUnifEigenspaceIndex {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
                theorem Module.End.genEigenspace_top_eq_maxUnifEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [h : IsNoetherian R M] (f : Module.End R M) (μ : R) :
                (f.genEigenspace μ) = (f.genEigenspace μ) (f.maxUnifEigenspaceIndex μ)

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

                theorem Module.End.genEigenspace_le_genEigenspace_maxUnifEigenspaceIndex {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) (k : ℕ∞) :
                (f.genEigenspace μ) k (f.genEigenspace μ) (f.maxUnifEigenspaceIndex μ)
                theorem Module.End.genEigenspace_eq_genEigenspace_maxUnifEigenspaceIndex_of_le {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) {k : } (hk : f.maxUnifEigenspaceIndex μ k) :
                (f.genEigenspace μ) k = (f.genEigenspace μ) (f.maxUnifEigenspaceIndex μ)

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

                theorem Module.End.HasUnifEigenvalue.le {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k m : ℕ∞} (hm : k m) (hk : f.HasUnifEigenvalue μ k) :
                f.HasUnifEigenvalue μ m

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

                theorem Module.End.HasUnifEigenvalue.lt {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k m : ℕ∞} (hm : 0 < m) (hk : f.HasUnifEigenvalue μ k) :
                f.HasUnifEigenvalue μ m

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

                @[simp]
                theorem Module.End.hasUnifEigenvalue_iff_hasUnifEigenvalue_one {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : ℕ∞} (hk : 0 < k) :
                f.HasUnifEigenvalue μ k f.HasUnifEigenvalue μ 1

                Generalized eigenvalues are actually just eigenvalues.

                theorem Module.End.maxUnifEigenspaceIndex_le_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) :
                f.maxUnifEigenspaceIndex μ Module.finrank K V
                theorem Module.End.genEigenspace_le_genEigenspace_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) (k : ℕ∞) :
                (f.genEigenspace μ) k (f.genEigenspace μ) (Module.finrank K V)

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

                theorem Module.End.genEigenspace_eq_genEigenspace_finrank_of_le {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) {k : } (hk : Module.finrank K V k) :
                (f.genEigenspace μ) k = (f.genEigenspace μ) (Module.finrank K V)

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

                theorem Module.End.mapsTo_genEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f g : Module.End R M} (h : Commute f g) (μ : R) (k : ℕ∞) :
                Set.MapsTo g ((f.genEigenspace μ) k) ((f.genEigenspace μ) k)
                theorem Module.End.isNilpotent_restrict_genEigenspace_nat {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) (h : Set.MapsTo (f - μ 1) ((f.genEigenspace μ) k) ((f.genEigenspace μ) k) := ) :

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

                theorem Module.End.isNilpotent_restrict_genEigenspace_top {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) (h : Set.MapsTo (f - μ 1) ((f.genEigenspace μ) ) ((f.genEigenspace μ) ) := ) :

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

                @[reducible, inline]
                abbrev 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
                • f.eigenspace μ = (f.genEigenspace μ) 1
                Instances For
                  theorem Module.End.eigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} :
                  f.eigenspace μ = LinearMap.ker (f - μ 1)
                  @[simp]
                  theorem Module.End.eigenspace_zero {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) :
                  f.eigenspace 0 = LinearMap.ker f
                  @[reducible, inline]
                  abbrev 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
                  • f.HasEigenvector μ x = f.HasUnifEigenvector μ 1 x
                  Instances For
                    theorem Module.End.hasEigenvector_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} :
                    f.HasEigenvector μ x x f.eigenspace μ x 0
                    @[reducible, inline]
                    abbrev 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
                    • f.HasEigenvalue a = f.HasUnifEigenvalue a 1
                    Instances For
                      theorem Module.End.hasEigenvalue_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} :
                      f.HasEigenvalue μ f.eigenspace μ
                      @[reducible, inline]
                      abbrev 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
                      • f.Eigenvalues = f.UnifEigenvalues 1
                      Instances For
                        @[reducible, inline]
                        abbrev Module.End.Eigenvalues.val {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) :
                        f.EigenvaluesR
                        Equations
                        • f = f 1
                        Instances For
                          theorem Module.End.hasEigenvalue_of_hasEigenvector {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {x : M} (h : f.HasEigenvector μ x) :
                          f.HasEigenvalue μ
                          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} :
                          x f.eigenspace μ f x = μ x
                          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 : f.HasEigenvector μ 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 : f.HasEigenvector μ 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μ : f.HasEigenvalue μ) :
                          ∃ (v : M), f.HasEigenvector μ v
                          theorem Module.End.HasEigenvalue.pow {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (h : f.HasEigenvalue μ) (n : ) :
                          (f ^ n).HasEigenvalue (μ ^ n)
                          theorem Module.End.HasEigenvalue.isNilpotent_of_isNilpotent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {f : Module.End R M} (hfn : IsNilpotent f) {μ : R} (hf : f.HasEigenvalue μ) :

                          A nilpotent endomorphism has nilpotent eigenvalues.

                          See also LinearMap.isNilpotent_trace_of_isNilpotent.

                          theorem Module.End.HasEigenvalue.mem_spectrum {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} (hμ : f.HasEigenvalue μ) :
                          μ spectrum R f
                          theorem Module.End.hasEigenvalue_iff_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} :
                          f.HasEigenvalue μ μ spectrum K f
                          theorem Module.End.HasEigenvalue.of_mem_spectrum {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {μ : K} :
                          μ spectrum K ff.HasEigenvalue μ

                          Alias of the reverse direction of Module.End.hasEigenvalue_iff_mem_spectrum.

                          theorem Module.End.eigenspace_div {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] (f : Module.End K V) (a b : K) (hb : b 0) :
                          f.eigenspace (a / b) = LinearMap.ker (b f - (algebraMap K (Module.End K V)) a)
                          @[deprecated Module.End.genEigenspace_nat]
                          theorem Module.End.genEigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) :
                          (f.genEigenspace μ) k = LinearMap.ker ((f - μ 1) ^ k)
                          @[reducible, inline]
                          abbrev Module.End.HasGenEigenvector {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
                          • f.HasGenEigenvector μ k x = f.HasUnifEigenvector μ (↑k) x
                          Instances For
                            theorem Module.End.hasGenEigenvector_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } {x : M} :
                            f.HasGenEigenvector μ k x x (f.genEigenspace μ) k x 0
                            @[reducible, inline]
                            abbrev Module.End.HasGenEigenvalue {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
                            • f.HasGenEigenvalue μ k = f.HasUnifEigenvalue μ k
                            Instances For
                              theorem Module.End.hasGenEigenvalue_iff {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } :
                              f.HasGenEigenvalue μ k (f.genEigenspace μ) k
                              @[deprecated Module.End.genEigenrange_nat]
                              theorem Module.End.genEigenrange_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } :
                              f.genEigenrange μ k = LinearMap.range ((f - μ 1) ^ k)
                              theorem Module.End.exp_ne_zero_of_hasGenEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } (h : f.HasGenEigenvalue μ k) :
                              k 0

                              The exponent of a generalized eigenvalue is never 0.

                              @[reducible, inline]
                              abbrev Module.End.maxGenEigenspace {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
                              • f.maxGenEigenspace μ = (f.genEigenspace μ)
                              Instances For
                                theorem Module.End.iSup_genEigenspace_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :
                                ⨆ (k : ), (f.genEigenspace μ) k = f.maxGenEigenspace μ
                                @[deprecated Module.End.iSup_genEigenspace_eq]
                                theorem Module.End.maxGenEigenspace_def {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) :
                                f.maxGenEigenspace μ = ⨆ (k : ), (f.genEigenspace μ) k
                                theorem Module.End.genEigenspace_le_maximal {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (k : ) :
                                (f.genEigenspace μ) k f.maxGenEigenspace μ
                                @[simp]
                                theorem Module.End.mem_maxGenEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ : R) (m : M) :
                                m f.maxGenEigenspace μ ∃ (k : ), ((f - μ 1) ^ k) m = 0
                                @[reducible, inline]
                                noncomputable abbrev Module.End.maxGenEigenspaceIndex {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
                                • f.maxGenEigenspaceIndex μ = f.maxUnifEigenspaceIndex μ
                                Instances For
                                  theorem Module.End.maxGenEigenspace_eq {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : Module.End R M) (μ : R) :
                                  f.maxGenEigenspace μ = (f.genEigenspace μ) (f.maxGenEigenspaceIndex μ)

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

                                  theorem Module.End.hasGenEigenvalue_of_hasGenEigenvalue_of_le {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k m : } (hm : k m) (hk : f.HasGenEigenvalue μ k) :
                                  f.HasGenEigenvalue μ m

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

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

                                  The eigenspace is a subspace of the generalized eigenspace.

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

                                  All eigenvalues are generalized eigenvalues.

                                  theorem Module.End.hasEigenvalue_of_hasGenEigenvalue {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} {k : } (hμ : f.HasGenEigenvalue μ k) :
                                  f.HasEigenvalue μ

                                  All generalized eigenvalues are eigenvalues.

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

                                  Generalized eigenvalues are actually just eigenvalues.

                                  theorem Module.End.maxGenEigenspace_eq_genEigenspace_finrank {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) :
                                  f.maxGenEigenspace μ = (f.genEigenspace μ) (Module.finrank K V)
                                  theorem Module.End.mapsTo_maxGenEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f g : Module.End R M} (h : Commute f g) (μ : R) :
                                  Set.MapsTo g (f.maxGenEigenspace μ) (f.maxGenEigenspace μ)
                                  @[deprecated Module.End.mapsTo_iSup_genEigenspace_of_comm]
                                  theorem Module.End.mapsTo_iSup_genEigenspace_of_comm {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {f g : Module.End R M} (h : Commute f g) (μ : R) :
                                  Set.MapsTo g (⨆ (k : ), (f.genEigenspace μ) k) (⨆ (k : ), (f.genEigenspace μ) 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 : Set.MapsTo (f - (algebraMap R (Module.End R M)) μ) ((f.genEigenspace μ) k) ((f.genEigenspace μ) k) := ) :

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

                                  theorem Module.End.isNilpotent_restrict_maxGenEigenspace_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 : Set.MapsTo (f - (algebraMap R (Module.End R M)) μ) (f.maxGenEigenspace μ) (f.maxGenEigenspace μ) := ) :

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

                                  @[deprecated Module.End.isNilpotent_restrict_maxGenEigenspace_sub_algebraMap]
                                  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 : Set.MapsTo (f - (algebraMap R (Module.End R M)) μ) (⨆ (k : ), (f.genEigenspace μ) k) (⨆ (k : ), (f.genEigenspace μ) k) := ) :

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

                                  theorem Module.End.disjoint_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ μ₂ : R} (hμ : μ₁ μ₂) (k l : ℕ∞) :
                                  Disjoint ((f.genEigenspace μ₁) k) ((f.genEigenspace μ₂) l)
                                  theorem Module.End.injOn_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) (k : ℕ∞) :
                                  Set.InjOn (fun (x : R) => (f.genEigenspace x) k) {μ : R | (f.genEigenspace μ) k }
                                  @[deprecated Module.End.disjoint_genEigenspace]
                                  theorem Module.End.disjoint_iSup_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) {μ₁ μ₂ : R} (hμ : μ₁ μ₂) :
                                  Disjoint (⨆ (k : ), (f.genEigenspace μ₁) k) (⨆ (k : ), (f.genEigenspace μ₂) k)
                                  theorem Module.End.injOn_maxGenEigenspace {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) => f.maxGenEigenspace x) {μ : R | f.maxGenEigenspace μ }
                                  @[deprecated Module.End.injOn_genEigenspace]
                                  theorem Module.End.injOn_iSup_genEigenspace {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 : ), (f.genEigenspace x) k) {μ : R | ⨆ (k : ), (f.genEigenspace μ) k }
                                  theorem Module.End.independent_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) (k : ℕ∞) :
                                  iSupIndep fun (x : R) => (f.genEigenspace x) k
                                  theorem Module.End.independent_maxGenEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) :
                                  iSupIndep f.maxGenEigenspace
                                  @[deprecated Module.End.independent_genEigenspace]
                                  theorem Module.End.independent_iSup_genEigenspace {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) :
                                  iSupIndep fun (μ : R) => ⨆ (k : ), (f.genEigenspace μ) k
                                  theorem Module.End.eigenspaces_iSupIndep {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) :
                                  iSupIndep f.eigenspace

                                  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.

                                  @[deprecated Module.End.eigenspaces_iSupIndep]
                                  theorem Module.End.eigenspaces_independent {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (f : Module.End R M) :
                                  iSupIndep f.eigenspace

                                  Alias of Module.End.eigenspaces_iSupIndep.


                                  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] {ι : Type u_1} [NoZeroSMulDivisors R M] (f : Module.End R M) (μ : ιR) (hμ : Function.Injective μ) (v : ιM) (h_eigenvec : ∀ (i : ι), f.HasEigenvector (μ i) (v i)) :

                                  Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent.

                                  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), f.HasEigenvector (↑μ) (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. See Module.End.eigenvectors_linearIndependent' for an indexed variant.

                                  theorem Module.End.genEigenspace_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) :
                                  (Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)

                                  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_genEigenspace {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) :
                                  p (f.genEigenspace μ) k = Submodule.map p.subtype ((Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k)
                                  theorem Module.End.mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] {p : Submodule R M} (f g : Module.End R M) (hf : Set.MapsTo f p p) (hg : Set.MapsTo g p p) {μ₁ μ₂ : R} (h : Set.MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) :
                                  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) :
                                  Submodule.map p.subtype (Module.End.eigenspace (LinearMap.restrict f hfp) μ) f.eigenspace μ

                                  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.

                                  theorem Module.End.generalized_eigenvec_disjoint_range_ker {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (f : Module.End K V) (μ : K) :
                                  Disjoint (f.genEigenrange μ (Module.finrank K V)) ((f.genEigenspace μ) (Module.finrank K V))

                                  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 (f.eigenspace μ) 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.

                                  theorem Module.End.pos_finrank_genEigenspace_of_hasEigenvalue {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {f : Module.End K V} {k : } {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) :
                                  0 < Module.finrank K ((f.genEigenspace μ) k)

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

                                  theorem Module.End.map_genEigenrange_le {K : Type v} {V : Type w} [Field K] [AddCommGroup V] [Module K V] {f : Module.End K V} {μ : K} {n : } :
                                  Submodule.map f (f.genEigenrange μ n) f.genEigenrange μ n

                                  A linear map maps a generalized eigenrange into itself.

                                  theorem Module.End.genEigenspace_le_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ t : R) (k : ℕ∞) :
                                  (f.genEigenspace μ) k ((t f).genEigenspace (t * μ)) k
                                  @[deprecated Module.End.genEigenspace_le_smul]
                                  theorem Module.End.iSup_genEigenspace_le_smul {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) (μ t : R) :
                                  ⨆ (k : ), (f.genEigenspace μ) k ⨆ (k : ), ((t f).genEigenspace (t * μ)) k
                                  theorem Module.End.genEigenspace_inf_le_add {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f₁ f₂ : Module.End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) :
                                  (f₁.genEigenspace μ₁) k₁ (f₂.genEigenspace μ₂) k₂ ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) (k₁ + k₂)
                                  @[deprecated Module.End.genEigenspace_inf_le_add]
                                  theorem Module.End.iSup_genEigenspace_inf_le_add {R : Type v} {M : Type w} [CommRing R] [AddCommGroup M] [Module R M] (f₁ f₂ : Module.End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) :
                                  (⨆ (k : ), (f₁.genEigenspace μ₁) k) ⨆ (k : ), (f₂.genEigenspace μ₂) k ⨆ (k : ), ((f₁ + f₂).genEigenspace (μ₁ + μ₂)) k
                                  theorem Module.End.map_smul_of_iInf_genEigenspace_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)] [MulActionHomClass F R L (Module.End R M)] (f : F) (μ : LR) (k : ℕ∞) (h_ne : ⨅ (x : L), ((f x).genEigenspace (μ x)) k ) (t : R) (x : L) :
                                  μ (t x) = t μ x
                                  @[deprecated Module.End.map_smul_of_iInf_genEigenspace_ne_bot]
                                  theorem Module.End.map_smul_of_iInf_iSup_genEigenspace_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)] [MulActionHomClass F R L (Module.End R M)] (f : F) (μ : LR) (h_ne : ⨅ (x : L), ⨆ (k : ), ((f x).genEigenspace (μ x)) k ) (t : R) (x : L) :
                                  μ (t x) = t μ x
                                  theorem Module.End.map_add_of_iInf_genEigenspace_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) (k : ℕ∞) (h_ne : ⨅ (x : L), ((f x).genEigenspace (μ x)) k ) (h : ∀ (x y : L), Commute (f x) (f y)) (x y : L) :
                                  μ (x + y) = μ x + μ y
                                  @[deprecated Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute]
                                  theorem Module.End.map_add_of_iInf_iSup_genEigenspace_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 : ), ((f x).genEigenspace (μ x)) k ) (h : ∀ (x y : L), Commute (f x) (f y)) (x y : L) :
                                  μ (x + y) = μ x + μ y