Tensor products of multiplicative Jordan decompositions

For finite-dimensional vector spaces over a perfect field, the multiplicative Jordan decomposition of a tensor product of linear automorphisms is obtained by tensoring their semisimple factors and their unipotent factors. Preservation of unipotence holds more generally over any commutative semiring acting on additive commutative groups.

This is the tensor-product compatibility needed to assemble the componentwise Jordan factors of point actions on finite comodules into tensor automorphisms. Together with the intertwining results in TauCeti.LinearAlgebra.JordanChevalley.Functoriality, it is the linear-algebraic bridge from Jordan decomposition in general linear groups to Jordan decomposition in an affine group via Tannakian reconstruction.

Main declarations

• LinearMap.GeneralLinearGroup.IsSemisimple.tensorProduct: tensor products of semisimple automorphisms are semisimple.
• LinearMap.GeneralLinearGroup.IsUnipotent.tensorProduct: tensor products of unipotent automorphisms are unipotent.
• LinearMap.GeneralLinearGroup.jordanDecomposition_tensorProduct: the canonical decomposition is factorwise on tensor products.

References

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

theorem LinearMap.GeneralLinearGroup.IsSemisimple.tensorProduct {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} (hg : g.IsSemisimple) (hh : h.IsSemisimple) : (g.tensorProduct h).IsSemisimple

The tensor product of semisimple linear automorphisms is semisimple.

theorem LinearMap.GeneralLinearGroup.IsUnipotent.tensorProduct {K : Type u} {V : Type v} {W : Type w} [CommSemiring 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.tensorProduct h).IsUnipotent

The tensor product of unipotent linear automorphisms is unipotent.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_tensorProduct {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.tensorProduct h).jordanDecomposition = (g.semisimplePart.tensorProduct h.semisimplePart, g.unipotentPart.tensorProduct h.unipotentPart)

The multiplicative Jordan decomposition of a tensor product is the tensor product of the corresponding factors.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_tensorProduct {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.tensorProduct h).semisimplePart = g.semisimplePart.tensorProduct h.semisimplePart

The semisimple factor of a tensor product is the tensor product of the semisimple factors.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_tensorProduct {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.tensorProduct h).unipotentPart = g.unipotentPart.tensorProduct h.unipotentPart

The unipotent factor of a tensor product is the tensor product of the unipotent factors.