Jordan decomposition of commuting algebraic-group points

The Jordan decomposition of algebraic-group points respects commuting products. If two points commute, then all of their reconstructed Jordan factors commute across the two decompositions, and the semisimple and unipotent parts of their product are the corresponding products.

The proof checks the linear result in every finite-dimensional comodule and then uses Tannakian reconstruction to separate points. This compatibility completes a standard structural property of the pointwise Jordan decomposition constructed in Layer 4 of the ReductiveGroups roadmap.

Main declarations

• TauCeti.HopfAlgebra.Point.commute_semisimplePart_left_of_commute and TauCeti.HopfAlgebra.Point.commute_unipotentPart_left_of_commute: each Jordan factor commutes with every point commuting with the original point.
• TauCeti.HopfAlgebra.Point.commute_semisimplePart_semisimplePart_of_commute: semisimple parts of commuting points commute.
• TauCeti.HopfAlgebra.Point.commute_semisimplePart_unipotentPart_of_commute and TauCeti.HopfAlgebra.Point.commute_unipotentPart_semisimplePart_of_commute: the two cross-commutation statements.
• TauCeti.HopfAlgebra.Point.commute_unipotentPart_unipotentPart_of_commute: unipotent parts of commuting points commute.
• TauCeti.HopfAlgebra.Point.jordanDecomposition_mul_of_commute: the ordered decomposition of a commuting product is the componentwise product.
• TauCeti.HopfAlgebra.Point.semisimplePart_mul_of_commute and TauCeti.HopfAlgebra.Point.unipotentPart_mul_of_commute: the two factor formulas.

References

• T. A. Springer, Linear Algebraic Groups, §2.4.
• J. S. Milne, Algebraic Groups (2017), §9.4.

theorem TauCeti.HopfAlgebra.Point.commute_semisimplePart_left_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (semisimplePart k H K g) h

The semisimple factor of a point commutes with every point that commutes with the original point.

theorem TauCeti.HopfAlgebra.Point.commute_unipotentPart_left_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (unipotentPart k H K g) h

The unipotent factor of a point commutes with every point that commutes with the original point.

theorem TauCeti.HopfAlgebra.Point.commute_semisimplePart_semisimplePart_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (semisimplePart k H K g) (semisimplePart k H K h)

The semisimple parts of two commuting algebraic-group points commute.

theorem TauCeti.HopfAlgebra.Point.commute_semisimplePart_unipotentPart_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (semisimplePart k H K g) (unipotentPart k H K h)

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

theorem TauCeti.HopfAlgebra.Point.commute_unipotentPart_semisimplePart_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (unipotentPart k H K g) (semisimplePart k H K h)

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

theorem TauCeti.HopfAlgebra.Point.commute_unipotentPart_unipotentPart_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : Commute (unipotentPart k H K g) (unipotentPart k H K h)

The unipotent parts of two commuting algebraic-group points commute.

theorem TauCeti.HopfAlgebra.Point.semisimplePart_mul_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : semisimplePart k H K (g * h) = semisimplePart k H K g * semisimplePart k H K h

The semisimple part of a product of commuting algebraic-group points is the product of their semisimple parts.

theorem TauCeti.HopfAlgebra.Point.unipotentPart_mul_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : unipotentPart k H K (g * h) = unipotentPart k H K g * unipotentPart k H K h

The unipotent part of a product of commuting algebraic-group points is the product of their unipotent parts.

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_mul_of_commute (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g h : WithConv (H →ₐ[k] K)} (hgh : Commute g h) : jordanDecomposition k H K (g * h) = (semisimplePart k H K g * semisimplePart k H K h, unipotentPart k H K g * unipotentPart k H K h)

The Jordan decomposition of a product of commuting algebraic-group points is the componentwise product of their Jordan decompositions.