Eigenspaces and tensoring with a flat module

Let f be an endomorphism of a module S over a commutative ring k, and X a flat k-module. The eigenspace inclusion of f at μ is exact against f - μ, and tensoring with X preserves this: the kernel of (f - μ) ⊗ id on S ⊗[k] X is the image of Eig(f, μ) ⊗[k] X. Flatness cannot be dropped: for S = k and a non-zero-divisor r ∈ k, the 0-eigenspace of r is zero, while the kernel of r ⊗ id on X is its r-torsion.

When f is the action of an element a of a k-algebra A acting on S, the endomorphism (f - μ) ⊗ id is the action of a - μ on S ⊗[k] X through the left factor.

A linear map l from S to a vector space over a field K extending k with l ∘ f = μ • l has a K-linear extension l.liftBaseChange K to K ⊗[k] S vanishing on every eigenspace of the base change of f for an eigenvalue other than μ.

Main results

• Module.End.exact_rTensor_eigenspace: Eig(f, μ) ⊗ X → S ⊗ X → S ⊗ X is exact for flat X.
• TauCeti.rTensor_lsmul_sub_smul_apply: (a - μ) ⊗ id acts as a - μ on the left factor.
• LinearMap.liftBaseChange_eq_zero_of_mem_eigenspace_baseChange: the extension of an eigenvector of precomposition by f kills the other eigenspaces of the base change of f.

theorem Module.End.exact_rTensor_eigenspace {k : Type u_1} {S : Type u_2} [CommRing k] [AddCommGroup S] [Module k S] (f : End k S) (μ : k) (X : Type u_3) [AddCommGroup X] [Module k X] [Flat k X] : Function.Exact ⇑(LinearMap.rTensor X (f.eigenspace μ).subtype) ⇑(LinearMap.rTensor X (f - μ • 1))

For a flat module X, the eigenspace inclusion of f at μ, tensored with X, is exact against (f - μ) ⊗ id.

theorem LinearMap.liftBaseChange_eq_zero_of_mem_eigenspace_baseChange {k : Type u_1} {S : Type u_2} [CommRing k] [AddCommGroup S] [Module k S] {K : Type u_3} {N : Type u_4} [Field K] [Algebra k K] [AddCommGroup N] [Module k N] [Module K N] [IsScalarTower k K N] (l : S →ₗ[k] N) (f : Module.End k S) {μ ν : K} (hl : ∀ (v : S), l (f v) = μ • l v) (hνμ : ν ≠ μ) {X : TensorProduct k K S} (hX : X ∈ Module.End.eigenspace (baseChange K f) ν) : (liftBaseChange K l) X = 0

If l (f v) = μ • l v for all v, the K-linear extension of l vanishes on the eigenspace of the base change of f for every eigenvalue ν ≠ μ.

theorem TauCeti.rTensor_lsmul_sub_smul_apply {k : Type u_1} {S : Type u_2} [CommRing k] [AddCommGroup S] [Module k S] {A : Type u_3} [Ring A] [Algebra k A] [Module A S] [IsScalarTower k A S] (X : Type u_4) [AddCommGroup X] [Module k X] (a : A) (μ : k) (t : TensorProduct k S X) : (LinearMap.rTensor X ((Algebra.lsmul k k S) a - μ • 1)) t = a • t - μ • t

(a - μ) ⊗ id acts on S ⊗[k] X as a - μ for the action of A on the left factor.