Scalar extension of multiplicative Jordan decomposition

Let R be a commutative semiring, let K and L be R-algebras that are fields, and let f : K →ₐ[R] L. An automorphism of K ⊗[R] V extends canonically to an automorphism of L ⊗[R] V. If K is perfect, scalar extension preserves semisimplicity: the squarefree minimal polynomial of the original endomorphism maps to a squarefree annihilating polynomial over L. Scalar extension also preserves unipotence directly, so uniqueness of the multiplicative Jordan–Chevalley decomposition identifies the extended factors.

Main declarations

• LinearMap.GeneralLinearGroup.IsSemisimple.mapValue: scalar extension preserves semisimple automorphisms when the source field is perfect.
• LinearMap.GeneralLinearGroup.IsUnipotent.mapValue: scalar extension preserves unipotent automorphisms, for arbitrary commutative value rings.
• LinearMap.GeneralLinearGroup.jordanDecomposition_mapValue: multiplicative Jordan decomposition commutes with scalar extension between perfect fields.

This is the linear-algebra input for value-field naturality of the Jordan decomposition of algebraic-group points.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.
• Mathlib.LinearAlgebra.Semisimple for the squarefree-minimal-polynomial criterion.

theorem LinearMap.GeneralLinearGroup.IsUnipotent.mapValue {R : Type u} {K : Type v} {L : Type w} {V : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [CommRing K] [Algebra R K] [CommRing L] [Algebra R L] {g : GeneralLinearGroup K (TensorProduct R K V)} (hg : g.IsUnipotent) (f : K →ₐ[R] L) : ((Module.End.mapValueGL f) g).IsUnipotent

Scalar extension preserves unipotence of a linear automorphism.

theorem LinearMap.GeneralLinearGroup.IsSemisimple.mapValue {R : Type u} {K : Type v} {L : Type w} {V : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [Field K] [Algebra R K] [Field L] [Algebra R L] [PerfectField K] [FiniteDimensional K (TensorProduct R K V)] {g : GeneralLinearGroup K (TensorProduct R K V)} (hg : g.IsSemisimple) (f : K →ₐ[R] L) : ((Module.End.mapValueGL f) g).IsSemisimple

Extending scalars from a perfect field preserves semisimplicity of an automorphism of a scalar extension.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_mapValue {R : Type u} {K : Type v} {L : Type w} {V : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [Field K] [Algebra R K] [Field L] [Algebra R L] [PerfectField K] [PerfectField L] [FiniteDimensional K (TensorProduct R K V)] [FiniteDimensional L (TensorProduct R L V)] (f : K →ₐ[R] L) (g : GeneralLinearGroup K (TensorProduct R K V)) : ((Module.End.mapValueGL f) g).jordanDecomposition = ((Module.End.mapValueGL f) g.semisimplePart, (Module.End.mapValueGL f) g.unipotentPart)

Multiplicative Jordan–Chevalley decomposition commutes with extension between perfect value fields.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_mapValue {R : Type u} {K : Type v} {L : Type w} {V : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [Field K] [Algebra R K] [Field L] [Algebra R L] [PerfectField K] [PerfectField L] [FiniteDimensional K (TensorProduct R K V)] [FiniteDimensional L (TensorProduct R L V)] (f : K →ₐ[R] L) (g : GeneralLinearGroup K (TensorProduct R K V)) : ((Module.End.mapValueGL f) g).semisimplePart = (Module.End.mapValueGL f) g.semisimplePart

The semisimple factor of an automorphism commutes with extension between perfect value fields.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_mapValue {R : Type u} {K : Type v} {L : Type w} {V : Type x} [CommSemiring R] [AddCommMonoid V] [Module R V] [Field K] [Algebra R K] [Field L] [Algebra R L] [PerfectField K] [PerfectField L] [FiniteDimensional K (TensorProduct R K V)] [FiniteDimensional L (TensorProduct R L V)] (f : K →ₐ[R] L) (g : GeneralLinearGroup K (TensorProduct R K V)) : ((Module.End.mapValueGL f) g).unipotentPart = (Module.End.mapValueGL f) g.unipotentPart

The unipotent factor of an automorphism commutes with extension between perfect value fields.