Documentation

Mathlib.LinearAlgebra.Semisimple

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: #

TODO #

In finite dimensions over a field:

@[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
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 pSubmodule.comap f p, qSubmodule.comap f q, IsCompl p q
    @[simp]
    theorem Module.End.isSemisimple_id {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] :
    @[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 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) :
    (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) :

    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