Jordan decomposition of commuting products

The multiplicative Jordan decomposition respects products of commuting linear automorphisms. More precisely, if g and h commute, then every Jordan factor of g commutes with every Jordan factor of h, and the semisimple and unipotent parts of g * h are the products of the corresponding parts.

The key input is that the semisimple part is a polynomial in the original automorphism. The cross-commutation statements then reduce the product formula to uniqueness of the multiplicative Jordan decomposition.

This supplies a structural compatibility for the Jordan decomposition in Layer 4 of the ReductiveGroups roadmap.

Main declarations

• LinearMap.GeneralLinearGroup.commute_coe_semisimplePart_left_of_commute and LinearMap.GeneralLinearGroup.commute_coe_unipotentPart_left_of_commute: each Jordan factor commutes with every endomorphism commuting with the original automorphism.
• LinearMap.GeneralLinearGroup.commute_semisimplePart_left_of_commute and LinearMap.GeneralLinearGroup.commute_unipotentPart_left_of_commute: the automorphism-level centralizer statements.
• LinearMap.GeneralLinearGroup.commute_semisimplePart_semisimplePart_of_commute: semisimple parts of commuting automorphisms commute.
• LinearMap.GeneralLinearGroup.commute_semisimplePart_unipotentPart_of_commute and LinearMap.GeneralLinearGroup.commute_unipotentPart_semisimplePart_of_commute: the two cross-commutation statements.
• LinearMap.GeneralLinearGroup.commute_unipotentPart_unipotentPart_of_commute: unipotent parts of commuting automorphisms commute.
• LinearMap.GeneralLinearGroup.jordanDecomposition_mul_of_commute: the ordered decomposition of a commuting product is the componentwise product.
• LinearMap.GeneralLinearGroup.semisimplePart_mul_of_commute and LinearMap.GeneralLinearGroup.unipotentPart_mul_of_commute: the two factor formulas.

References

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

theorem LinearMap.GeneralLinearGroup.commute_coe_semisimplePart_left_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} {x : Module.End K V} (hgx : Commute (↑g) x) : Commute (↑g.semisimplePart) x

The semisimple factor of an automorphism commutes with every endomorphism that commutes with the original automorphism.

theorem LinearMap.GeneralLinearGroup.commute_coe_unipotentPart_left_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g : GeneralLinearGroup K V} {x : Module.End K V} (hgx : Commute (↑g) x) : Commute (↑g.unipotentPart) x

The unipotent factor of an automorphism commutes with every endomorphism that commutes with the original automorphism.

theorem LinearMap.GeneralLinearGroup.commute_semisimplePart_left_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.semisimplePart h

The semisimple factor of an automorphism commutes with every automorphism that commutes with the original automorphism.

theorem LinearMap.GeneralLinearGroup.commute_unipotentPart_left_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.unipotentPart h

The unipotent factor of an automorphism commutes with every automorphism that commutes with the original automorphism.

theorem LinearMap.GeneralLinearGroup.commute_semisimplePart_semisimplePart_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.semisimplePart h.semisimplePart

The semisimple parts of two commuting linear automorphisms commute.

theorem LinearMap.GeneralLinearGroup.commute_semisimplePart_unipotentPart_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.semisimplePart h.unipotentPart

The semisimple part of the first of two commuting automorphisms commutes with the unipotent part of the second.

theorem LinearMap.GeneralLinearGroup.commute_unipotentPart_semisimplePart_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.unipotentPart h.semisimplePart

The unipotent part of the first of two commuting automorphisms commutes with the semisimple part of the second.

theorem LinearMap.GeneralLinearGroup.commute_unipotentPart_unipotentPart_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : Commute g.unipotentPart h.unipotentPart

The unipotent parts of two commuting linear automorphisms commute.

theorem LinearMap.GeneralLinearGroup.jordanDecomposition_mul_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : (g * h).jordanDecomposition = (g.semisimplePart * h.semisimplePart, g.unipotentPart * h.unipotentPart)

The Jordan decomposition of a product of commuting linear automorphisms is the componentwise product of their Jordan decompositions.

theorem LinearMap.GeneralLinearGroup.semisimplePart_mul_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : (g * h).semisimplePart = g.semisimplePart * h.semisimplePart

The semisimple part of a product of commuting automorphisms is the product of their semisimple parts.

theorem LinearMap.GeneralLinearGroup.unipotentPart_mul_of_commute {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [PerfectField K] [FiniteDimensional K V] {g h : GeneralLinearGroup K V} (hgh : Commute g h) : (g * h).unipotentPart = g.unipotentPart * h.unipotentPart

The unipotent part of a product of commuting automorphisms is the product of their unipotent parts.