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:

• If semisimple then generalized eigenspace is eigenspace
• Restriction of semisimple endomorphism is semisimple
• Triangularizable iff diagonalisable for semisimple endomorphisms

@[inline, reducible]

abbrev 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

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

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} : Module.End.IsSemisimple f ↔ ∀ p ≤ Submodule.comap f p, ∃ q ≤ Submodule.comap f q, IsCompl p q

@[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} : Module.End.IsSemisimple (-f) ↔ Module.End.IsSemisimple f

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 : Module.End.IsSemisimple f) : f = 0

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) : Module.End.IsSemisimple (t • f) ↔ Module.End.IsSemisimple f

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 : Module.End.IsSemisimple f) : Module.End.IsSemisimple (t • f)

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) : Module.End.IsSemisimple f

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 : Module.End.IsSemisimple f) : 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 : Module.End.IsSemisimple f) (p : Polynomial K) : Module.End.IsSemisimple ((Polynomial.aeval f) p)

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 : Module.End.IsSemisimple f) {a : Module.End K M} (ha : a ∈ Algebra.adjoin K {f}) : Module.End.IsSemisimple a

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 : Module.End.IsSemisimple f) (n : ℕ) : Module.End.IsSemisimple (f ^ n)

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 : Module.End.IsSemisimple f) (hg : Module.End.IsSemisimple g) {a : Module.End K M} (ha : a ∈ Algebra.adjoin K {f, g}) : Module.End.IsSemisimple a

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 : Module.End.IsSemisimple f) (hg : Module.End.IsSemisimple g) : Module.End.IsSemisimple (f + g)

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 : Module.End.IsSemisimple f) (hg : Module.End.IsSemisimple g) : Module.End.IsSemisimple (f - g)

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 : Module.End.IsSemisimple f) (hg : Module.End.IsSemisimple g) : Module.End.IsSemisimple (f * g)