Eigenspaces of g ∘ f and f ∘ g

For linear maps f : M → N and g : N → M and a unit μ, the map f carries the μ-eigenspace of g ∘ f isomorphically onto the μ-eigenspace of f ∘ g, with inverse μ⁻¹ • g. In particular the two composites have the same eigenvalue multiplicities at every nonzero eigenvalue over a field. This is the multiplicity form of Mathlib's spectrum.nonzero_mul_comm, and applied to f = A and g = A† it shows that the source and target Gram operators A† A and A A† of a linear map between inner product spaces have the same nonzero eigenvalues with multiplicity.

Main declarations

• Module.End.eigenspaceCompEquiv: the linear equivalence induced by f between the μ-eigenspaces of g ∘ₗ f and f ∘ₗ g.
• Module.End.finrank_eigenspace_comp_comm: the two eigenspaces have the same dimension.

References

• R. A. Horn and C. R. Johnson, Matrix Analysis, second edition, Cambridge University Press, 2013, Theorem 1.3.22.

noncomputable def Module.End.eigenspaceCompEquiv {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) {μ : R} (hμ : IsUnit μ) : ↥(eigenspace (g ∘ₗ f) μ) ≃ₗ[R] ↥(eigenspace (f ∘ₗ g) μ)

For a unit μ, f restricts to a linear equivalence from the μ-eigenspace of g ∘ₗ f onto the μ-eigenspace of f ∘ₗ g; the inverse is the restriction of μ⁻¹ • g.

@[simp]

theorem Module.End.coe_eigenspaceCompEquiv_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) {μ : R} (hμ : IsUnit μ) (x : ↥(eigenspace (g ∘ₗ f) μ)) : ↑((eigenspaceCompEquiv f g hμ) x) = f ↑x

@[simp]

theorem Module.End.coe_eigenspaceCompEquiv_symm_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) {μ : R} (hμ : IsUnit μ) (y : ↥(eigenspace (f ∘ₗ g) μ)) : ↑((eigenspaceCompEquiv f g hμ).symm y) = ↑hμ.unit⁻¹ • g ↑y

theorem Module.End.finrank_eigenspace_comp_comm {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (g : N →ₗ[R] M) {μ : R} (hμ : IsUnit μ) : finrank R ↥(eigenspace (g ∘ₗ f) μ) = finrank R ↥(eigenspace (f ∘ₗ g) μ)

At a unit μ, the μ-eigenspaces of g ∘ₗ f and f ∘ₗ g have the same dimension.