Eigenvalues of the products AB and BA

TheoremEigenspace of fg maps into the eigenspace of gf#✓fully proved

g sends the μ-eigenspace of f ∘ₗ g into the μ-eigenspace of g ∘ₗ f: if (f ∘ₗ g) x = μ • x then (g ∘ₗ f) (g x) = μ • (g x).

theorem mapsTo_eigenspace_comp (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) (μ : 𝕜) :
    Set.MapsTo g (Module.End.eigenspace (f ∘ₗ g) μ)
      (Module.End.eigenspace (g ∘ₗ f) μ)

Used by 4

Used byLinear equivalence of eigenspaces of fg and gf · Eigenvectors of fg map to eigenvectors of gf · Injectivity of g between eigenspaces of fg and gf · Surjectivity of g between eigenspaces of fg and gf

TheoremInjectivity of g between eigenspaces of fg and gf#✓fully proved

The map g restricted to the eigenspaces is injective when μ ≠ 0: if g x = 0 for an eigenvector x of f ∘ₗ g, then (f ∘ₗ g) x = 0 = μ • x, so x = 0.

theorem injective_restrict_eigenspace_comp (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V)
    {μ : 𝕜} (hμ : μ ≠ 0) :
    Function.Injective (LinearMap.restrict g (mapsTo_eigenspace_comp f g μ))

Uses 1 · Used by 1

Statement usesEigenspace of fg maps into the eigenspace of gf

Used byLinear equivalence of eigenspaces of fg and gf

TheoremSurjectivity of g between eigenspaces of fg and gf#✓fully proved

The map g restricted to the eigenspaces is surjective when μ ≠ 0: an eigenvector y of g ∘ₗ f is the image of μ⁻¹ • f y.

theorem surjective_restrict_eigenspace_comp (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V)
    {μ : 𝕜} (hμ : μ ≠ 0) :
    Function.Surjective (LinearMap.restrict g (mapsTo_eigenspace_comp f g μ))

Uses 1 · Used by 1

Statement usesEigenspace of fg maps into the eigenspace of gf

Used byLinear equivalence of eigenspaces of fg and gf

DefinitionLinear equivalence of eigenspaces of fg and gf#✓fully proved

For a nonzero eigenvalue, the eigenspaces of f ∘ₗ g and of g ∘ₗ f are linearly equivalent, via g in one direction.

noncomputable def eigenspaceCompEquiv (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) {μ : 𝕜}
    (hμ : μ ≠ 0) :
    Module.End.eigenspace (f ∘ₗ g) μ ≃ₗ[𝕜] Module.End.eigenspace (g ∘ₗ f) μ :=
  LinearEquiv.ofBijective (LinearMap.restrict g (mapsTo_eigenspace_comp f g μ))
    ⟨injective_restrict_eigenspace_comp f g hμ,
     surjective_restrict_eigenspace_comp f g hμ⟩

Uses 3 · Used by 2

Statement usesInjectivity of g between eigenspaces of fg and gf · Eigenspace of fg maps into the eigenspace of gf · Surjectivity of g between eigenspaces of fg and gf

Used byEigenspaces of fg and gf are equivalent, for endomorphisms · Geometric multiplicities of fg and gf agree

TheoremGeometric multiplicities of fg and gf agree#✓fully proved

The geometric multiplicities of a nonzero eigenvalue of f ∘ₗ g and of g ∘ₗ f agree.

theorem finrank_eigenspace_comp_eq (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) {μ : 𝕜}
    (hμ : μ ≠ 0) :
    Module.finrank 𝕜 (Module.End.eigenspace (f ∘ₗ g) μ) =
      Module.finrank 𝕜 (Module.End.eigenspace (g ∘ₗ f) μ)

Uses 1 · Used by 2

Proof usesLinear equivalence of eigenspaces of fg and gf

Used byGeometric multiplicities of fg and gf agree, for endomorphisms · Geometric multiplicities of matrix products AB and BA agree

TheoremEigenvectors of fg map to eigenvectors of gf#✓fully proved

An eigenvector of f ∘ₗ g for a nonzero eigenvalue is sent by g to an eigenvector of g ∘ₗ f for the same eigenvalue.

theorem hasEigenvector_comp {f : V →ₗ[𝕜] W} {g : W →ₗ[𝕜] V} {μ : 𝕜} (hμ : μ ≠ 0)
    {x : W} (hx : Module.End.HasEigenvector (f ∘ₗ g) μ x) : Module.End.HasEigenvector (g ∘ₗ f) μ (g x)

Uses 1 · Used by 2

Proof usesEigenspace of fg maps into the eigenspace of gf

Used byNonzero eigenvalues of fg and gf coincide · Eigenvectors of fg map to eigenvectors of gf, for endomorphisms

TheoremNonzero eigenvalues of fg and gf coincide#✓fully proved

A nonzero scalar is an eigenvalue of f ∘ₗ g iff it is an eigenvalue of g ∘ₗ f.

theorem hasEigenvalue_comp_iff (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.End.HasEigenvalue (f ∘ₗ g) μ ↔ Module.End.HasEigenvalue (g ∘ₗ f) μ

Uses 1 · Used by 2

Proof usesEigenvectors of fg map to eigenvectors of gf

Used byNonzero eigenvalues of fg and gf coincide, for endomorphisms · Nonzero eigenvalues of matrix products AB and BA coincide

TheoremGeneralized eigenspace of fg maps into that of gf#✓fully proved

g sends the generalized μ-eigenspace of f ∘ₗ g into the generalized μ-eigenspace of g ∘ₗ f, for every exponent. This is the intertwining (g ∘ₗ f) ∘ₗ g = g ∘ₗ (f ∘ₗ g) applied to Mathlib's Module.End.mapsTo_genEigenspace_of_comp.

theorem mapsTo_genEigenspace_comp (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) (μ : 𝕜) (k : ℕ∞) :
    Set.MapsTo g (Module.End.genEigenspace (f ∘ₗ g) μ k) (Module.End.genEigenspace (g ∘ₗ f) μ k)

Used by 1

Used byRestriction of g to generalized eigenspaces of fg and gf

TheoremKernel of g meets a generalized eigenspace of fg trivially#✓fully proved

If g x = 0 and x lies in the generalized μ-eigenspace of f ∘ₗ g with μ ≠ 0, then x = 0. Indeed, on the kernel of g the map f ∘ₗ g vanishes, so (f ∘ₗ g - μ • 1) ^ l acts as (-μ) ^ l • 1 there.

theorem eq_zero_of_apply_eq_zero_of_mem_genEigenspace
    {f : V →ₗ[𝕜] W} {g : W →ₗ[𝕜] V} {μ : 𝕜} (hμ : μ ≠ 0) {k : ℕ∞} {x : W}
    (hx : x ∈ Module.End.genEigenspace (f ∘ₗ g) μ k) (hgx : g x = 0) : x = 0

Used by 1

Used byInjectivity of g on generalized eigenspaces of fg

DefinitionRestriction of g to generalized eigenspaces of fg and gf#✓fully proved

The restriction of g to the generalized μ-eigenspaces.

noncomputable def genEigenspaceCompMap (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) (μ : 𝕜)
    (k : ℕ∞) :
    Module.End.genEigenspace (f ∘ₗ g) μ k →ₗ[𝕜] Module.End.genEigenspace (g ∘ₗ f) μ k :=
  LinearMap.restrict g (mapsTo_genEigenspace_comp f g μ k)

Uses 1 · Used by 3

Statement usesGeneralized eigenspace of fg maps into that of gf

Used byGeneralized eigenspaces of fg and gf are finite-dimensional together · Generalized eigenspaces of fg and gf have equal dimension · Injectivity of g on generalized eigenspaces of fg

TheoremInjectivity of g on generalized eigenspaces of fg#✓fully proved

The restriction of g to a generalized μ-eigenspace with μ ≠ 0 is injective.

theorem injective_genEigenspaceCompMap (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V)
    {μ : 𝕜} (hμ : μ ≠ 0) (k : ℕ∞) :
    Function.Injective (genEigenspaceCompMap f g μ k)

Uses 2 · Used by 2

Statement usesRestriction of g to generalized eigenspaces of fg and gf

Proof usesKernel of g meets a generalized eigenspace of fg trivially

Used byGeneralized eigenspaces of fg and gf are finite-dimensional together · Generalized eigenspaces of fg and gf have equal dimension

TheoremGeneralized eigenspaces of fg and gf are finite-dimensional together#✓fully proved

For a nonzero scalar, the generalized eigenspaces of f ∘ₗ g and of g ∘ₗ f are finite-dimensional together, for every exponent k : ℕ∞.

theorem finite_genEigenspace_comp_iff (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) {μ : 𝕜}
    (hμ : μ ≠ 0) (k : ℕ∞) :
    Module.Finite 𝕜 (Module.End.genEigenspace (f ∘ₗ g) μ k) ↔
      Module.Finite 𝕜 (Module.End.genEigenspace (g ∘ₗ f) μ k)

Uses 2 · Used by 3

Proof usesRestriction of g to generalized eigenspaces of fg and gf · Injectivity of g on generalized eigenspaces of fg

Used byGeneralized eigenspaces finite-dimensional together, for endomorphisms · Generalized eigenspaces of AB and BA are finite-dimensional together · Generalized eigenspaces of fg and gf have equal dimension

TheoremGeneralized eigenspaces of fg and gf have equal dimension#✓fully proved

The generalized μ-eigenspaces of f ∘ₗ g and of g ∘ₗ f have equal Module.finrank, for every exponent k : ℕ∞ and every nonzero μ. They are finite-dimensional together; if both are infinite-dimensional, both finranks are zero. In finite dimension only the stabilized generalized eigenspace (for example at exponent ⊤) measures algebraic multiplicity.

theorem finrank_genEigenspace_comp_eq (f : V →ₗ[𝕜] W) (g : W →ₗ[𝕜] V) {μ : 𝕜}
    (hμ : μ ≠ 0) (k : ℕ∞) :
    Module.finrank 𝕜 (Module.End.genEigenspace (f ∘ₗ g) μ k) =
      Module.finrank 𝕜 (Module.End.genEigenspace (g ∘ₗ f) μ k)

Uses 3 · Used by 2

Proof usesGeneralized eigenspaces of fg and gf are finite-dimensional together · Restriction of g to generalized eigenspaces of fg and gf · Injectivity of g on generalized eigenspaces of fg

Used byGeneralized eigenspace dimensions agree, for endomorphisms · Generalized eigenspaces of AB and BA have equal dimension

DefinitionEigenspaces of fg and gf are equivalent, for endomorphisms#✓fully proved

The * form of eigenspaceCompEquiv, for endomorphisms of one space.

noncomputable def eigenspaceMulEquiv (A B : Module.End 𝕜 V) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.End.eigenspace (A * B) μ ≃ₗ[𝕜] Module.End.eigenspace (B * A) μ := by
  simp only [Module.End.mul_eq_comp]
  exact eigenspaceCompEquiv A B hμ

Uses 1

Statement usesLinear equivalence of eigenspaces of fg and gf

TheoremGeometric multiplicities of fg and gf agree, for endomorphisms#✓fully proved

The * form of finrank_eigenspace_comp_eq.

theorem finrank_eigenspace_mul_eq (A B : Module.End 𝕜 V) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.finrank 𝕜 (Module.End.eigenspace (A * B) μ) =
      Module.finrank 𝕜 (Module.End.eigenspace (B * A) μ)

Uses 1 · Used by 1

Proof usesGeometric multiplicities of fg and gf agree

Used byEqual geometric multiplicities of nonzero eigenvalues of ST and TS

TheoremEigenvectors of fg map to eigenvectors of gf, for endomorphisms#✓fully proved

The * form of hasEigenvector_comp.

theorem hasEigenvector_mul {A B : Module.End 𝕜 V} {μ : 𝕜} (hμ : μ ≠ 0) {x : V}
    (hx : (A * B).HasEigenvector μ x) : (B * A).HasEigenvector μ (B x)

Uses 1

Proof usesEigenvectors of fg map to eigenvectors of gf

TheoremNonzero eigenvalues of fg and gf coincide, for endomorphisms#✓fully proved

The * form of hasEigenvalue_comp_iff.

theorem hasEigenvalue_mul_iff (A B : Module.End 𝕜 V) {μ : 𝕜} (hμ : μ ≠ 0) :
    (A * B).HasEigenvalue μ ↔ (B * A).HasEigenvalue μ

Uses 1 · Used by 1

Proof usesNonzero eigenvalues of fg and gf coincide

Used byNonzero eigenvalues of ST and TS coincide

TheoremGeneralized eigenspace dimensions agree, for endomorphisms#✓fully proved

The * form of finrank_genEigenspace_comp_eq.

theorem finrank_genEigenspace_mul_eq (A B : Module.End 𝕜 V) {μ : 𝕜} (hμ : μ ≠ 0)
    (k : ℕ∞) :
    Module.finrank 𝕜 ((A * B).genEigenspace μ k) =
      Module.finrank 𝕜 ((B * A).genEigenspace μ k)

Uses 1 · Used by 1

Proof usesGeneralized eigenspaces of fg and gf have equal dimension

Used byEqual dimensions of generalized eigenspaces of ST and TS

TheoremGeneralized eigenspaces finite-dimensional together, for endomorphisms#✓fully proved

The * form of finite_genEigenspace_comp_iff.

theorem finite_genEigenspace_mul_iff (A B : Module.End 𝕜 V) {μ : 𝕜} (hμ : μ ≠ 0)
    (k : ℕ∞) :
    Module.Finite 𝕜 ((A * B).genEigenspace μ k) ↔
      Module.Finite 𝕜 ((B * A).genEigenspace μ k)

Uses 1 · Used by 1

Proof usesGeneralized eigenspaces of fg and gf are finite-dimensional together

Used byFinite-dimensionality of generalized eigenspaces of ST and TS

TheoremNonzero eigenvalues of matrix products AB and BA coincide#✓fully proved

A nonzero scalar is an eigenvalue of the matrix product A * B iff it is an eigenvalue of B * A.

theorem hasEigenvalue_mul_iff (A : Matrix ι κ 𝕜) (B : Matrix κ ι 𝕜) {μ : 𝕜}
    (hμ : μ ≠ 0) :
    Module.End.HasEigenvalue (Matrix.toLin' (A * B)) μ ↔
      Module.End.HasEigenvalue (Matrix.toLin' (B * A)) μ

Uses 1

Proof usesNonzero eigenvalues of fg and gf coincide

TheoremGeometric multiplicities of matrix products AB and BA agree#✓fully proved

The geometric multiplicities of a nonzero eigenvalue of A * B and of B * A agree.

theorem finrank_eigenspace_mul_eq (A : Matrix ι κ 𝕜) (B : Matrix κ ι 𝕜) {μ : 𝕜}
    (hμ : μ ≠ 0) :
    Module.finrank 𝕜 (Module.End.eigenspace (Matrix.toLin' (A * B)) μ) =
      Module.finrank 𝕜 (Module.End.eigenspace (Matrix.toLin' (B * A)) μ)

Uses 1

Proof usesGeometric multiplicities of fg and gf agree

TheoremGeneralized eigenspaces of AB and BA have equal dimension#✓fully proved

The generalized μ-eigenspaces of A * B and of B * A have equal Module.finrank, for every exponent k : ℕ∞.

theorem finrank_genEigenspace_mul_eq (A : Matrix ι κ 𝕜) (B : Matrix κ ι 𝕜) {μ : 𝕜}
    (hμ : μ ≠ 0) (k : ℕ∞) :
    Module.finrank 𝕜 (Module.End.genEigenspace (Matrix.toLin' (A * B)) μ k) =
      Module.finrank 𝕜 (Module.End.genEigenspace (Matrix.toLin' (B * A)) μ k)

Uses 1

Proof usesGeneralized eigenspaces of fg and gf have equal dimension

TheoremGeneralized eigenspaces of AB and BA are finite-dimensional together#✓fully proved

The generalized eigenspaces of rectangular products in opposite orders are finite-dimensional together for a nonzero scalar and every exponent.

theorem finite_genEigenspace_mul_iff (A : Matrix ι κ 𝕜) (B : Matrix κ ι 𝕜) {μ : 𝕜}
    (hμ : μ ≠ 0) (k : ℕ∞) :
    Module.Finite 𝕜 (Module.End.genEigenspace (Matrix.toLin' (A * B)) μ k) ↔
      Module.Finite 𝕜 (Module.End.genEigenspace (Matrix.toLin' (B * A)) μ k)

Uses 1

Proof usesGeneralized eigenspaces of fg and gf are finite-dimensional together

TheoremNonzero eigenvalues of ST and TS coincide#✓fully proved

A nonzero scalar is an eigenvalue of S * T iff it is an eigenvalue of T * S, for bounded operators.

theorem hasEigenvalue_mul_iff (S T : E →L[𝕜] E) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.End.HasEigenvalue ((S * T : E →L[𝕜] E) : Module.End 𝕜 E) μ ↔
      Module.End.HasEigenvalue ((T * S : E →L[𝕜] E) : Module.End 𝕜 E) μ

Uses 1 · Used by 1

Proof usesNonzero eigenvalues of fg and gf coincide, for endomorphisms

Used byNonzero eigenvalues of an operator times its adjoint, in either order

TheoremEqual geometric multiplicities of nonzero eigenvalues of ST and TS#✓fully proved

The geometric multiplicities of a nonzero eigenvalue of S * T and of T * S agree, for bounded operators.

theorem finrank_eigenspace_mul_eq (S T : E →L[𝕜] E) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.finrank 𝕜
        (Module.End.eigenspace ((S * T : E →L[𝕜] E) : Module.End 𝕜 E) μ) =
      Module.finrank 𝕜
        (Module.End.eigenspace ((T * S : E →L[𝕜] E) : Module.End 𝕜 E) μ)

Uses 1

Proof usesGeometric multiplicities of fg and gf agree, for endomorphisms

TheoremEqual dimensions of generalized eigenspaces of ST and TS#✓fully proved

The generalized μ-eigenspaces of S * T and of T * S have equal Module.finrank, for every exponent k : ℕ∞, for bounded operators.

theorem finrank_genEigenspace_mul_eq (S T : E →L[𝕜] E) {μ : 𝕜} (hμ : μ ≠ 0)
    (k : ℕ∞) :
    Module.finrank 𝕜
        (Module.End.genEigenspace ((S * T : E →L[𝕜] E) : Module.End 𝕜 E) μ k) =
      Module.finrank 𝕜
        (Module.End.genEigenspace ((T * S : E →L[𝕜] E) : Module.End 𝕜 E) μ k)

Uses 1

Proof usesGeneralized eigenspace dimensions agree, for endomorphisms

TheoremFinite-dimensionality of generalized eigenspaces of ST and TS#✓fully proved

Generalized eigenspaces of reversed bounded-operator products are finite-dimensional together for a nonzero scalar and every exponent.

theorem finite_genEigenspace_mul_iff (S T : E →L[𝕜] E) {μ : 𝕜} (hμ : μ ≠ 0)
    (k : ℕ∞) :
    Module.Finite 𝕜
        (Module.End.genEigenspace ((S * T : E →L[𝕜] E) : Module.End 𝕜 E) μ k) ↔
      Module.Finite 𝕜
        (Module.End.genEigenspace ((T * S : E →L[𝕜] E) : Module.End 𝕜 E) μ k)

Uses 1

Proof usesGeneralized eigenspaces finite-dimensional together, for endomorphisms

TheoremNonzero eigenvalues of an operator times its adjoint, in either order#✓fully proved

A nonzero scalar is an eigenvalue of T† * T iff it is an eigenvalue of T * T†, on a Hilbert space.

theorem hasEigenvalue_adjoint_mul_self_iff {𝕜 E : Type*} [RCLike 𝕜]
    [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E]
    (T : E →L[𝕜] E) {μ : 𝕜} (hμ : μ ≠ 0) :
    Module.End.HasEigenvalue
        ((ContinuousLinearMap.adjoint T * T : E →L[𝕜] E) : Module.End 𝕜 E) μ ↔
      Module.End.HasEigenvalue
        ((T * ContinuousLinearMap.adjoint T : E →L[𝕜] E) : Module.End 𝕜 E) μ

Uses 1

Proof usesNonzero eigenvalues of ST and TS coincide

28 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.