Semisimple linear endomorphisms

Given an R-module M together with an R-linear endomorphism f : M → M, the following two conditions are equivalent:

1. Every f-invariant submodule of M has an f-invariant complement.
2. M is a semisimple R[X]-module, where the action of the polynomial ring is induced by f.

A linear endomorphism f satisfying these equivalent conditions is known as a semisimple endomorphism. We provide basic definitions and results about such endomorphisms in this file.

Main definitions / results:

• Module.End.IsSemisimple: the definition that a linear endomorphism is semisimple
• Module.End.isSemisimple_iff: the characterisation of semisimplicity in terms of invariant submodules.
• Module.End.eq_zero_of_isNilpotent_isSemisimple: the zero endomorphism is the only endomorphism that is both nilpotent and semisimple.
• Module.End.isSemisimple_of_squarefree_aeval_eq_zero: an endomorphism that is a root of a square-free polynomial is semisimple (in finite dimensions over a field).
• Module.End.IsSemisimple.minpoly_squarefree: the minimal polynomial of a semisimple endomorphism is squarefree.
• IsSemisimple.of_mem_adjoin_pair: every endomorphism in the subalgebra generated by two commuting semisimple endomorphisms is semisimple, if the base field is perfect.

TODO

In finite dimensions over a field:

• Triangularizable iff diagonalisable for semisimple endomorphisms

def Module.End.IsSemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : Prop

A linear endomorphism of an R-module M is called semisimple if the induced R[X]-module structure on M is semisimple. This is equivalent to saying that every f-invariant R-submodule of M has an f-invariant complement: see Module.End.isSemisimple_iff.

Equations

• f.IsSemisimple = IsSemisimpleModule (Polynomial R) (Module.AEval' f)

def Module.End.IsFinitelySemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) : Prop

A weaker version of semisimplicity that only prescribes behaviour on finitely-generated submodules.

Equations

• f.IsFinitelySemisimple = ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule), Module.Finite R ↥p → Module.End.IsSemisimple (LinearMap.restrict f hp)

theorem Module.End.isSemisimple_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : f.IsSemisimple ↔ ∀ (p : ↥f.invtSubmodule), ∃ (q : ↥f.invtSubmodule), IsCompl p q

A linear endomorphism is semisimple if every invariant submodule has in invariant complement.

See also Module.End.isSemisimple_iff.

theorem Module.End.isSemisimple_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : f.IsSemisimple ↔ ∀ p ∈ f.invtSubmodule, ∃ q ∈ f.invtSubmodule, IsCompl p q

theorem Module.End.isSemisimple_restrict_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (p : Submodule R M) (hp : p ∈ f.invtSubmodule) : Module.End.IsSemisimple (LinearMap.restrict f hp) ↔ ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

theorem Module.End.isFinitelySemisimple_iff' {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : f.IsFinitelySemisimple ↔ ∀ (p : Submodule R M) (hp : p ∈ f.invtSubmodule), Module.Finite R ↥p → Module.End.IsSemisimple (LinearMap.restrict f hp)

A linear endomorphism is finitely semisimple if it is semisimple on every finitely-generated invariant submodule.

See also Module.End.isFinitelySemisimple_iff.

theorem Module.End.isFinitelySemisimple_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : f.IsFinitelySemisimple ↔ ∀ p ∈ f.invtSubmodule, Module.Finite R ↥p → ∀ q ∈ f.invtSubmodule, q ≤ p → ∃ r ≤ p, r ∈ f.invtSubmodule ∧ Disjoint q r ∧ q ⊔ r = p

A characterisation of Module.End.IsFinitelySemisimple using only the lattice of submodules of M (thus avoiding submodules of submodules).

@[simp]

theorem Module.End.isSemisimple_zero {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Module.End.IsSemisimple 0

@[simp]

theorem Module.End.isSemisimple_id {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : Module.End.IsSemisimple LinearMap.id

@[simp]

theorem Module.End.isSemisimple_neg {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} : (-f).IsSemisimple ↔ f.IsSemisimple

theorem LinearEquiv.isSemisimple_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (f : Module.End R M) {M₂ : Type u_3} [AddCommGroup M₂] [Module R M₂] (g : Module.End R M₂) (e : M ≃ₗ[R] M₂) (he : ↑e ∘ₗ f = g ∘ₗ ↑e) : f.IsSemisimple ↔ g.IsSemisimple

theorem Module.End.eq_zero_of_isNilpotent_isSemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (hn : IsNilpotent f) (hs : f.IsSemisimple) : f = 0

theorem Module.End.eq_zero_of_isNilpotent_of_isFinitelySemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (hn : IsNilpotent f) (hs : f.IsFinitelySemisimple) : f = 0

@[simp]

theorem Module.End.isSemisimple_sub_algebraMap_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} : (f - (algebraMap R (Module.End R M)) μ).IsSemisimple ↔ f.IsSemisimple

theorem Module.End.IsSemisimple.restrict {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hp : p ∈ f.invtSubmodule) (hf : f.IsSemisimple) : Module.End.IsSemisimple (LinearMap.restrict f hp)

theorem Module.End.IsSemisimple.isFinitelySemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} (hf : f.IsSemisimple) : f.IsFinitelySemisimple

@[simp]

theorem Module.End.isFinitelySemisimple_iff_isSemisimple {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} [Module.Finite R M] : f.IsFinitelySemisimple ↔ f.IsSemisimple

@[simp]

theorem Module.End.isFinitelySemisimple_sub_algebraMap_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {μ : R} : (f - (algebraMap R (Module.End R M)) μ).IsFinitelySemisimple ↔ f.IsFinitelySemisimple

theorem Module.End.IsFinitelySemisimple.restrict {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {f : Module.End R M} {p : Submodule R M} (hp : p ∈ f.invtSubmodule) (hf : f.IsFinitelySemisimple) : Module.End.IsFinitelySemisimple (LinearMap.restrict f hp)

theorem Module.End.IsSemisimple_smul_iff {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {t : K} (ht : t ≠ 0) : (t • f).IsSemisimple ↔ f.IsSemisimple

theorem Module.End.IsSemisimple_smul {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} (t : K) (h : f.IsSemisimple) : (t • f).IsSemisimple

theorem Module.End.isSemisimple_of_squarefree_aeval_eq_zero {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {p : Polynomial K} (hp : Squarefree p) (hpf : (Polynomial.aeval f) p = 0) : f.IsSemisimple

theorem Module.End.IsSemisimple.minpoly_squarefree {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) : Squarefree (minpoly K f)

The minimal polynomial of a semisimple endomorphism is square free

theorem Module.End.IsSemisimple.aeval {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) (p : Polynomial K) : ((Polynomial.aeval f) p).IsSemisimple

theorem Module.End.IsSemisimple.of_mem_adjoin_singleton {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) {a : Module.End K M} (ha : a ∈ Algebra.adjoin K {f}) : a.IsSemisimple

theorem Module.End.IsSemisimple.pow {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} [FiniteDimensional K M] (hf : f.IsSemisimple) (n : ℕ) : (f ^ n).IsSemisimple

theorem Module.End.IsSemisimple.of_mem_adjoin_pair {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) {a : Module.End K M} (ha : a ∈ Algebra.adjoin K {f, g}) : a.IsSemisimple

theorem Module.End.IsSemisimple.add_of_commute {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f + g).IsSemisimple

theorem Module.End.IsSemisimple.sub_of_commute {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f - g).IsSemisimple

theorem Module.End.IsSemisimple.mul_of_commute {M : Type u_2} [AddCommGroup M] {K : Type u_3} [Field K] [Module K M] {f : Module.End K M} {g : Module.End K M} [FiniteDimensional K M] [PerfectField K] (comm : Commute f g) (hf : f.IsSemisimple) (hg : g.IsSemisimple) : (f * g).IsSemisimple