Jordan decomposition of algebraic-group points

Let H be a commutative Hopf algebra over a field k, and let K be a perfect extension field. Every K-valued point g of the affine group represented by H acts on each finite-dimensional H-comodule. The multiplicative Jordan decompositions of these actions are natural in the comodule and compatible with tensor products, so Tannakian reconstruction turns their semisimple and unipotent factors back into K-valued points of the original group.

This file defines those two reconstructed points. They commute, their product is g, and their actions in every finite-dimensional representation are exactly the semisimple and unipotent parts of the action of g. Thus the decomposition stays inside the affine group rather than merely inside each ambient general linear group.

Main declarations

• TauCeti.HopfAlgebra.Point.semisimplePart: the semisimple part of an algebraic-group point.
• TauCeti.HopfAlgebra.Point.unipotentPart: the unipotent part of an algebraic-group point.
• TauCeti.HopfAlgebra.Point.jordanDecomposition: the ordered pair of the two parts.
• TauCeti.HopfAlgebra.Point.jordanDecomposition_spec: the defining properties of the ordered decomposition.
• TauCeti.HopfAlgebra.Point.isSemisimple_isUnipotent_unique: uniqueness of a commuting semisimple-unipotent factorization.
• TauCeti.HopfAlgebra.Point.eq_jordanDecomposition_iff: characterization of the canonical ordered pair.
• TauCeti.HopfAlgebra.Point.commute_semisimplePart_unipotentPart: the two parts commute.
• TauCeti.HopfAlgebra.Point.semisimplePart_mul_unipotentPart: their product is the original point.
• TauCeti.HopfAlgebra.Point.endOfPoint_semisimplePart and TauCeti.HopfAlgebra.Point.endOfPoint_unipotentPart: every finite-dimensional representation sees the corresponding linear Jordan factors.
• TauCeti.HopfAlgebra.Point.isUnipotentPoint_iff_unipotentPart_eq_self and TauCeti.HopfAlgebra.Point.isUnipotentPoint_iff_semisimplePart_eq_one: pointwise characterizations of unipotence by the Jordan factors.

References

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

noncomputable def TauCeti.HopfAlgebra.Point.semisimplePart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : WithConv (H →ₐ[k] K)

The semisimple part of a point of an affine group over a perfect extension field.

It is reconstructed from the tensor automorphism whose component on every finite-dimensional comodule is the semisimple part of the original point action.

Equations

• TauCeti.HopfAlgebra.Point.semisimplePart k H K g = (TauCeti.Tannaka.fgPointTensorIsoEquiv k H K).symm (TauCeti.Tannaka.fgPointSemisimplePartTensorIso k H K g)

theorem TauCeti.HopfAlgebra.Point.semisimplePart_def (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : semisimplePart k H K g = (Tannaka.fgPointTensorIsoEquiv k H K).symm (Tannaka.fgPointSemisimplePartTensorIso k H K g)

The semisimple part is reconstructed from the semisimple-factor tensor automorphism.

noncomputable def TauCeti.HopfAlgebra.Point.unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : WithConv (H →ₐ[k] K)

The unipotent part of a point of an affine group over a perfect extension field.

It is reconstructed from the tensor automorphism whose component on every finite-dimensional comodule is the unipotent part of the original point action.

Equations

• TauCeti.HopfAlgebra.Point.unipotentPart k H K g = (TauCeti.Tannaka.fgPointTensorIsoEquiv k H K).symm (TauCeti.Tannaka.fgPointUnipotentPartTensorIso k H K g)

theorem TauCeti.HopfAlgebra.Point.unipotentPart_def (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : unipotentPart k H K g = (Tannaka.fgPointTensorIsoEquiv k H K).symm (Tannaka.fgPointUnipotentPartTensorIso k H K g)

The unipotent part is reconstructed from the unipotent-factor tensor automorphism.

noncomputable def TauCeti.HopfAlgebra.Point.jordanDecomposition (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : WithConv (H →ₐ[k] K) × WithConv (H →ₐ[k] K)

The multiplicative Jordan decomposition of an algebraic-group point, with the semisimple part first and the unipotent part second.

Equations

• TauCeti.HopfAlgebra.Point.jordanDecomposition k H K g = (TauCeti.HopfAlgebra.Point.semisimplePart k H K g, TauCeti.HopfAlgebra.Point.unipotentPart k H K g)

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_fst (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (jordanDecomposition k H K g).1 = semisimplePart k H K g

The first component of the Jordan decomposition is the semisimple part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_snd (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (jordanDecomposition k H K g).2 = unipotentPart k H K g

The second component of the Jordan decomposition is the unipotent part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.fgPointTensorIso_semisimplePart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : Tannaka.fgPointTensorIso k H K (semisimplePart k H K g) = Tannaka.fgPointSemisimplePartTensorIso k H K g

The Tannakian action of the semisimple part is the semisimple-factor tensor automorphism.

@[simp]

theorem TauCeti.HopfAlgebra.Point.fgPointTensorIso_unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : Tannaka.fgPointTensorIso k H K (unipotentPart k H K g) = Tannaka.fgPointUnipotentPartTensorIso k H K g

The Tannakian action of the unipotent part is the unipotent-factor tensor automorphism.

@[simp]

theorem TauCeti.HopfAlgebra.Point.endOfPoint_semisimplePart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : Comodule.endOfPoint (↑M) (semisimplePart k H K g).ofConv = ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).semisimplePart

In every finite-dimensional comodule, the reconstructed semisimple point acts by the semisimple part of the original point action.

@[simp]

theorem TauCeti.HopfAlgebra.Point.endOfPoint_unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : Comodule.endOfPoint (↑M) (unipotentPart k H K g).ofConv = ↑(LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).unipotentPart

In every finite-dimensional comodule, the reconstructed unipotent point acts by the unipotent part of the original point action.

@[simp]

theorem TauCeti.HopfAlgebra.Point.ofLinearEquiv_pointsAction_semisimplePart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) (semisimplePart k H K g)) = (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).semisimplePart

As an element of the general linear group of any finite-dimensional comodule, the action of the reconstructed semisimple point is the canonical semisimple part of the original action.

@[simp]

theorem TauCeti.HopfAlgebra.Point.ofLinearEquiv_pointsAction_unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) (unipotentPart k H K g)) = (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).unipotentPart

As an element of the general linear group of any finite-dimensional comodule, the action of the reconstructed unipotent point is the canonical unipotent part of the original action.

theorem TauCeti.HopfAlgebra.Point.isSemisimple_pointsAction_semisimplePart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) (semisimplePart k H K g))).IsSemisimple

The semisimple part acts semisimply in every finite-dimensional representation.

theorem TauCeti.HopfAlgebra.Point.isUnipotent_pointsAction_unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) (M : FGComoduleCat k H) : (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) (unipotentPart k H K g))).IsUnipotent

The unipotent part acts unipotently in every finite-dimensional representation.

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

The semisimple and unipotent parts of an algebraic-group point commute.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePart_mul_unipotentPart (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : semisimplePart k H K g * unipotentPart k H K g = g

Multiplying the semisimple and unipotent parts recovers the original algebraic-group point.

theorem TauCeti.HopfAlgebra.Point.isSemisimple_isUnipotent_unique (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g s u : WithConv (H →ₐ[k] K)) (hc : Commute s u) (hmul : s * u = g) (hs : ∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) s)).IsSemisimple) (hu : IsUnipotentPoint u) : s = semisimplePart k H K g ∧ u = unipotentPart k H K g

A commuting factorization of a point into factors acting semisimply and unipotently in every finite-dimensional comodule is its canonical Jordan decomposition.

theorem TauCeti.HopfAlgebra.Point.jordanDecomposition_spec (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : (∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) (jordanDecomposition k H K g).1)).IsSemisimple) ∧ IsUnipotentPoint (jordanDecomposition k H K g).2 ∧ Commute (jordanDecomposition k H K g).1 (jordanDecomposition k H K g).2 ∧ g = (jordanDecomposition k H K g).1 * (jordanDecomposition k H K g).2

The canonical point-level Jordan decomposition has the defining semisimple, unipotent, commutation, and product properties.

theorem TauCeti.HopfAlgebra.Point.eq_jordanDecomposition_iff (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g s u : WithConv (H →ₐ[k] K)) : (s, u) = jordanDecomposition k H K g ↔ (∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) s)).IsSemisimple) ∧ IsUnipotentPoint u ∧ Commute s u ∧ g = s * u

A pair is the canonical point-level Jordan decomposition exactly when it is a commuting semisimple-unipotent factorization in every finite-dimensional comodule.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePart_eq_self (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g : WithConv (H →ₐ[k] K)} (hg : ∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).IsSemisimple) : semisimplePart k H K g = g

A point acting semisimply in every finite-dimensional comodule is its own semisimple part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPart_eq_one_of_isSemisimple (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g : WithConv (H →ₐ[k] K)} (hg : ∀ (M : FGComoduleCat k H), (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Comodule.pointsAction ↑M) g)).IsSemisimple) : unipotentPart k H K g = 1

A point acting semisimply in every finite-dimensional comodule has trivial unipotent part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.semisimplePart_eq_one_of_isUnipotent (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) : semisimplePart k H K g = 1

A point acting unipotently in every finite-dimensional comodule has trivial semisimple part.

@[simp]

theorem TauCeti.HopfAlgebra.Point.unipotentPart_eq_self (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) : unipotentPart k H K g = g

A point acting unipotently in every finite-dimensional comodule is its own unipotent part.

theorem TauCeti.HopfAlgebra.Point.isUnipotentPoint_iff_unipotentPart_eq_self (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] (g : WithConv (H →ₐ[k] K)) : IsUnipotentPoint g ↔ unipotentPart k H K g = g

A point is unipotent exactly when its unipotent part is the point itself.

theorem TauCeti.HopfAlgebra.Point.isUnipotentPoint_iff_semisimplePart_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)) : IsUnipotentPoint g ↔ semisimplePart k H K g = 1

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

theorem TauCeti.HopfAlgebra.Point.semisimplePart_one (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] : semisimplePart k H K 1 = 1

The semisimple part of the identity point is the identity.

theorem TauCeti.HopfAlgebra.Point.unipotentPart_one (k H K : Type u) [Field k] [CommRing H] [HopfAlgebra k H] [Field K] [Algebra k K] [PerfectField K] : unipotentPart k H K 1 = 1

The unipotent part of the identity point is the identity.