Scalar extension of Jordan decomposition for algebraic-group points

For a morphism f : K →ₐ[k] L between perfect value fields, postcomposition sends the Jordan decomposition of a K-valued point to the Jordan decomposition of its resulting L-valued point. The proof compares point actions before and after scalar extension. Their underlying endomorphisms are related by Module.End.mapValue, so semisimplicity is preserved by the corresponding linear Jordan–Chevalley theorem. Unipotence is already natural in the value algebra. The point-level result then follows from uniqueness of the commuting semisimple–unipotent factorization.

Together with coordinate-domain naturality, this supplies both variances needed to compare geometric Jordan decompositions across affine-group morphisms and extensions of geometric point fields.

Main declarations

• TauCeti.HopfAlgebra.Point.jordanDecomposition_mapValue: point-level Jordan decomposition commutes with extension between perfect value fields.
• TauCeti.HopfAlgebra.Point.semisimplePart_mapValue and TauCeti.HopfAlgebra.Point.unipotentPart_mapValue: the component formulas, with jordanDecomposition_toConv_algHom_comp, semisimplePart_toConv_algHom_comp, and unipotentPart_toConv_algHom_comp as the simp-normal forms.

References

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

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_mapValue {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : jordanDecomposition k H L ((AlgHom.mapValue f) g) = ((AlgHom.mapValue f) (semisimplePart k H K g), (AlgHom.mapValue f) (unipotentPart k H K g))

The Jordan decomposition of an algebraic-group point commutes with extension between perfect value fields.

theorem TauCeti.HopfAlgebra.Point.semisimplePart_mapValue {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : semisimplePart k H L ((AlgHom.mapValue f) g) = (AlgHom.mapValue f) (semisimplePart k H K g)

The semisimple part of an algebraic-group point commutes with extension between perfect value fields.

theorem TauCeti.HopfAlgebra.Point.unipotentPart_mapValue {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : unipotentPart k H L ((AlgHom.mapValue f) g) = (AlgHom.mapValue f) (unipotentPart k H K g)

The unipotent part of an algebraic-group point commutes with extension between perfect value fields.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_toConv_algHom_comp {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : jordanDecomposition k H L (WithConv.toConv (f.comp g.ofConv)) = (WithConv.toConv (f.comp (semisimplePart k H K g).ofConv), WithConv.toConv (f.comp (unipotentPart k H K g).ofConv))

Simp-normal form of jordanDecomposition_mapValue, with each postcomposed point written after normalization by AlgHom.mapValue_apply.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePart_toConv_algHom_comp {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : semisimplePart k H L (WithConv.toConv (f.comp g.ofConv)) = WithConv.toConv (f.comp (semisimplePart k H K g).ofConv)

Simp-normal form of semisimplePart_mapValue, written after normalization by AlgHom.mapValue_apply.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPart_toConv_algHom_comp {k H K L : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] [PerfectField K] [PerfectField L] (f : K →ₐ[k] L) (g : WithConv (H →ₐ[k] K)) : unipotentPart k H L (WithConv.toConv (f.comp g.ofConv)) = WithConv.toConv (f.comp (unipotentPart k H K g).ofConv)

Simp-normal form of unipotentPart_mapValue, written after normalization by AlgHom.mapValue_apply.