Naturality of Jordan decomposition for algebraic-group points

A bialgebra morphism φ : H₁ →ₐc[k] H₂ between coordinate Hopf algebras represents a homomorphism in the opposite direction between the corresponding affine groups. On points this homomorphism is precomposition, TauCeti.AlgHom.mapDomain φ.

This file proves that point-level Jordan decomposition is natural under these homomorphisms. The key compatibility is representation-theoretic: acting by the precomposed point on an H₁-comodule is the same as first corestricting that comodule along φ and then acting by the original H₂-point. The earlier point-action and semisimple-point APIs provide this compatibility; uniqueness of the commuting semisimple--unipotent factorization then identifies the images of both Jordan factors.

This is the functoriality-under-homomorphisms part of Layer 4, "Jordan decomposition", in the ReductiveGroups roadmap.

Main declarations

• TauCeti.HopfAlgebra.Point.jordanDecomposition_mapDomain: Jordan decomposition commutes with a homomorphism of affine groups.
• TauCeti.HopfAlgebra.Point.semisimplePart_mapDomain and TauCeti.HopfAlgebra.Point.unipotentPart_mapDomain: the two component formulas, with semisimplePart_toConv_comp and unipotentPart_toConv_comp as their simp-normal forms.
• TauCeti.HopfAlgebra.isSemisimplePoint_mapDomain_iff_of_surjective: precomposition by a surjective coordinate morphism detects semisimple points.

References

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

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_mapDomain {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : jordanDecomposition k H₁ K ((AlgHom.mapDomain φ) g) = ((AlgHom.mapDomain φ) (semisimplePart k H₂ K g), (AlgHom.mapDomain φ) (unipotentPart k H₂ K g))

The Jordan decomposition of an algebraic-group point commutes with a homomorphism of affine groups. The coordinate-algebra morphism points in the opposite direction.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_toConv_comp {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : jordanDecomposition k H₁ K (WithConv.toConv (g.ofConv.comp ↑φ)) = (WithConv.toConv ((semisimplePart k H₂ K g).ofConv.comp ↑φ), WithConv.toConv ((unipotentPart k H₂ K g).ofConv.comp ↑φ))

Simp-normal form of jordanDecomposition_mapDomain, with each precomposed point written after normalization by AlgHom.mapDomain_apply.

theorem TauCeti.HopfAlgebra.Point.semisimplePart_mapDomain {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : semisimplePart k H₁ K ((AlgHom.mapDomain φ) g) = (AlgHom.mapDomain φ) (semisimplePart k H₂ K g)

Taking the semisimple part commutes with precomposition by a bialgebra morphism, the contravariant coordinate-algebra form of an affine-group homomorphism.

theorem TauCeti.HopfAlgebra.Point.unipotentPart_mapDomain {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : unipotentPart k H₁ K ((AlgHom.mapDomain φ) g) = (AlgHom.mapDomain φ) (unipotentPart k H₂ K g)

Taking the unipotent part commutes with precomposition by a bialgebra morphism, the contravariant coordinate-algebra form of an affine-group homomorphism.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePart_toConv_comp {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : semisimplePart k H₁ K (WithConv.toConv (g.ofConv.comp ↑φ)) = WithConv.toConv ((semisimplePart k H₂ K g).ofConv.comp ↑φ)

Simp-normal form of semisimplePart_mapDomain: taking the semisimple part commutes with AlgHom.mapDomain φ, written after normalization by AlgHom.mapDomain_apply.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPart_toConv_comp {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (φ : H₁ →ₐc[k] H₂) (g : WithConv (H₂ →ₐ[k] K)) : unipotentPart k H₁ K (WithConv.toConv (g.ofConv.comp ↑φ)) = WithConv.toConv ((unipotentPart k H₂ K g).ofConv.comp ↑φ)

Simp-normal form of unipotentPart_mapDomain: taking the unipotent part commutes with AlgHom.mapDomain φ, written after normalization by AlgHom.mapDomain_apply.

theorem TauCeti.HopfAlgebra.isSemisimplePoint_iff_unipotentPart_eq_one {k H₁ K : Type u} [Field k] [CommRing H₁] [HopfAlgebra k H₁] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H₁ →ₐ[k] K)) : IsSemisimplePoint g ↔ Point.unipotentPart k H₁ K g = 1

A point is semisimple exactly when its unipotent part is the identity.

@[simp]

theorem TauCeti.HopfAlgebra.isSemisimplePoint_mapDomain_iff_of_surjective {k H₁ H₂ K : Type u} [Field k] [CommRing H₁] [CommRing H₂] [HopfAlgebra k H₁] [HopfAlgebra k H₂] [Field K] [Algebra k K] [PerfectField K] (f : H₁ →ₐc[k] H₂) (hf : Function.Surjective ⇑f) (g : WithConv (H₂ →ₐ[k] K)) : IsSemisimplePoint (WithConv.toConv (g.ofConv.comp ↑f)) ↔ IsSemisimplePoint g

Precomposition with a surjective coordinate Hopf-algebra morphism detects semisimple points.

Contravariantly, this says that a point of a closed subgroup is semisimple exactly when its image in the ambient affine group is semisimple.