Transporting eigenspaces along intertwining maps

If a linear equivalence e : U ≃ₗ[R] W intertwines endomorphisms f of U and g of W, then every eigenspace of f is the preimage under e of the corresponding eigenspace of g. Mathlib's Module.End.map_genEigenspace_le gives only the inclusion of the image; this file records the equality available for an equivalence.

Over a domain, a surjective intertwining map into a torsion-free module carries each maximal generalized eigenspace of f onto the corresponding one of g, provided U is the sum of the maximal generalized eigenspaces of f (for instance, when U is finite-dimensional over an algebraically closed field). In particular, taking generalized eigenspaces is exact on quotients.

Main results

• TauCeti.eigenspace_eq_comap_of_intertwine: an intertwining linear equivalence identifies the eigenspaces of the two endomorphisms.
• TauCeti.map_maxGenEigenspace_eq_of_intertwine: a surjective intertwining map carries the maximal generalized eigenspaces of f onto those of g.

theorem TauCeti.eigenspace_eq_comap_of_intertwine {R : Type u_1} {U : Type u_2} {W : Type u_3} [CommRing R] [AddCommGroup U] [Module R U] [AddCommGroup W] [Module R W] {e : U ≃ₗ[R] W} {f : U →ₗ[R] U} {g : W →ₗ[R] W} (h : ∀ (x : U), e (f x) = g (e x)) (μ : R) : Module.End.eigenspace f μ = Submodule.comap (↑e) (Module.End.eigenspace g μ)

An intertwining linear equivalence identifies the eigenspaces of the two endomorphisms.

theorem TauCeti.map_maxGenEigenspace_eq_of_intertwine {R : Type u_1} {U : Type u_2} {W : Type u_3} [CommRing R] [AddCommGroup U] [Module R U] [AddCommGroup W] [Module R W] [IsDomain R] [Module.IsTorsionFree R W] {e : U →ₗ[R] W} (he : Function.Surjective ⇑e) {f : Module.End R U} {g : Module.End R W} (h : ∀ (x : U), e (f x) = g (e x)) (hf : ⨆ (μ : R), f.maxGenEigenspace μ = ⊤) (μ : R) : Submodule.map e (f.maxGenEigenspace μ) = g.maxGenEigenspace μ

A surjective linear map intertwining f and g carries each maximal generalized eigenspace of f onto the maximal generalized eigenspace of g for the same eigenvalue, provided the maximal generalized eigenspaces of f span the source.