Products of multiplicative Jordan decompositions

Semisimple and unipotent linear automorphisms are preserved by componentwise products. On finite-dimensional modules over a perfect field, the multiplicative Jordan decomposition of a product automorphism is therefore computed componentwise.

These identities describe the Jordan decomposition on a direct sum of two representations.

Main declarations

• LinearMap.GeneralLinearGroup.jordanDecomposition_prodMap: Jordan decomposition is componentwise on product modules.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.

theorem LinearMap.GeneralLinearGroup.IsUnipotent.prodMap {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] {g : GeneralLinearGroup K V} {h : GeneralLinearGroup K W} (hg : g.IsUnipotent) (hh : h.IsUnipotent) : (g.prodMap h).IsUnipotent

The product map of two unipotent automorphisms is unipotent.

theorem LinearMap.GeneralLinearGroup.IsSemisimple.prodMap {K : Type u} {V : Type v} {W : Type w} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] {g : GeneralLinearGroup K V} {h : GeneralLinearGroup K W} (hg : g.IsSemisimple) (hh : h.IsSemisimple) : (g.prodMap h).IsSemisimple

The product map of two semisimple automorphisms is semisimple.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_prodMap {K : Type u} {V : Type v} {W : Type w} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [PerfectField K] [FiniteDimensional K V] [FiniteDimensional K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : (g.prodMap h).jordanDecomposition = (g.semisimplePart.prodMap h.semisimplePart, g.unipotentPart.prodMap h.unipotentPart)

The multiplicative Jordan decomposition of a product-map automorphism is the product map of the decompositions of its two factors.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_prodMap {K : Type u} {V : Type v} {W : Type w} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [PerfectField K] [FiniteDimensional K V] [FiniteDimensional K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : (g.prodMap h).semisimplePart = g.semisimplePart.prodMap h.semisimplePart

The semisimple factor of a product-map automorphism is computed componentwise.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_prodMap {K : Type u} {V : Type v} {W : Type w} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [PerfectField K] [FiniteDimensional K V] [FiniteDimensional K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : (g.prodMap h).unipotentPart = g.unipotentPart.prodMap h.unipotentPart

The unipotent factor of a product-map automorphism is computed componentwise.