Semisimple linear endomorphisms #
Given an R-module M together with an R-linear endomorphism f : M → M, the following two
conditions are equivalent:
- Every
f-invariant submodule ofMhas anf-invariant complement. Mis a semisimpleR[X]-module, where the action of the polynomial ring is induced byf.
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 semisimpleModule.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
@[reducible, inline]
abbrev
Module.End.IsSemisimple
{R : Type u_1}
{M : Type u_2}
[CommRing R]
[AddCommGroup M]
[Module R M]
(f : Module.End R M)
:
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)
Instances For
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 ≤ 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]
:
@[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}
:
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
@[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 : Set.MapsTo ⇑f ↑p ↑p}
(hf : f.IsSemisimple)
:
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)
:
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