Functoriality of the multiplicative Jordan decomposition

The multiplicative Jordan--Chevalley decomposition of a linear automorphism does not depend on the coordinates used to describe it. A linear equivalence e : V ≃ₗ[K] W transports an automorphism by conjugation. This file proves that semisimplicity is invariant under this transport and that both canonical Jordan factors commute with it. More generally, every linear map between finite-dimensional modules over a perfect field that intertwines two automorphisms also intertwines their canonical semisimple and unipotent factors; no injectivity or surjectivity assumption is needed.

This is the first functoriality step for the Jordan decomposition requested in Layer 4 of the ReductiveGroups roadmap. In particular, it makes the general-linear decomposition invariant under a change of basis, as required before it can be transported through a faithful representation of an affine algebraic group.

Main declarations

• LinearMap.GeneralLinearGroup.isSemisimple_congrLinearEquiv_iff: semisimplicity is invariant under linear conjugation.
• LinearMap.GeneralLinearGroup.isSemisimple_conj_iff: semisimplicity is invariant under conjugation within the general linear group.
• LinearMap.GeneralLinearGroup.jordanDecomposition_congrLinearEquiv: the canonical pair is equivariant under linear conjugation.
• LinearMap.GeneralLinearGroup.semisimplePart_congrLinearEquiv and LinearMap.GeneralLinearGroup.unipotentPart_congrLinearEquiv: the two factor formulas.
• LinearMap.GeneralLinearGroup.comp_semisimplePart_eq_of_comp_eq: intertwiners commute with semisimple factors.
• LinearMap.GeneralLinearGroup.comp_unipotentPart_eq_of_comp_eq: intertwiners commute with unipotent factors.

References

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

@[simp]

theorem LinearMap.GeneralLinearGroup.isSemisimple_congrLinearEquiv_iff {K : Type u} {V : Type v} {W : Type w} [CommRing K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] (e : V ≃ₗ[K] W) (g : GeneralLinearGroup K V) : (ofLinearEquiv (e.symm ≪≫ₗ (g.toLinearEquiv ≪≫ₗ e))).IsSemisimple ↔ g.IsSemisimple

Semisimplicity of a linear automorphism is invariant under transport by a linear equivalence.

@[simp]

theorem LinearMap.GeneralLinearGroup.isSemisimple_conj_iff {K : Type u} {V : Type v} [CommRing K] [AddCommGroup V] [Module K V] (g h : GeneralLinearGroup K V) : (h * g * h⁻¹).IsSemisimple ↔ g.IsSemisimple

Semisimplicity is invariant under conjugation by a linear automorphism.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_congrLinearEquiv {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] (e : V ≃ₗ[K] W) (g : GeneralLinearGroup K V) : ((congrLinearEquiv e) g).jordanDecomposition = ((congrLinearEquiv e) g.semisimplePart, (congrLinearEquiv e) g.unipotentPart)

The multiplicative Jordan--Chevalley decomposition commutes with transport by a linear equivalence.

@[simp]

theorem LinearMap.GeneralLinearGroup.semisimplePart_congrLinearEquiv {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] (e : V ≃ₗ[K] W) (g : GeneralLinearGroup K V) : (ofLinearEquiv (e.symm ≪≫ₗ (g.toLinearEquiv ≪≫ₗ e))).semisimplePart = (congrLinearEquiv e) g.semisimplePart

The semisimple factor of the multiplicative Jordan decomposition commutes with transport by a linear equivalence.

@[simp]

theorem LinearMap.GeneralLinearGroup.unipotentPart_congrLinearEquiv {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] (e : V ≃ₗ[K] W) (g : GeneralLinearGroup K V) : (ofLinearEquiv (e.symm ≪≫ₗ (g.toLinearEquiv ≪≫ₗ e))).unipotentPart = (congrLinearEquiv e) g.unipotentPart

The unipotent factor of the multiplicative Jordan decomposition commutes with transport by a linear equivalence.

theorem LinearMap.GeneralLinearGroup.comp_semisimplePart_eq_of_comp_eq {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] (f : V →ₗ[K] W) (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) (hfg : f ∘ₗ ↑g = ↑h ∘ₗ f) : f ∘ₗ ↑g.semisimplePart = ↑h.semisimplePart ∘ₗ f

A linear map intertwining two automorphisms also intertwines their semisimple factors.

theorem LinearMap.GeneralLinearGroup.comp_unipotentPart_eq_of_comp_eq {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] (f : V →ₗ[K] W) (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) (hfg : f ∘ₗ ↑g = ↑h ∘ₗ f) : f ∘ₗ ↑g.unipotentPart = ↑h.unipotentPart ∘ₗ f

A linear map intertwining two automorphisms also intertwines their unipotent factors.