Unipotence over reduced Hopf algebras

An injective morphism H ⟶ K of coordinate Hopf algebras represents a schematically dense homomorphism Spec K ⟶ Spec H. When K is reduced and finite type, its geometric points separate elements. Applying this to the coefficients of the characteristic polynomial of every representation shows that geometric unipotence descends from K to H.

The same universal characteristic-polynomial identity also shows that every point valued in any commutative algebra over the ground field is unipotent.

Main declarations

• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_injective_of_reduced: geometric unipotence descends along an injective coordinate morphism with reduced finite-type codomain.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.isUnipotentPoint: geometric unipotence can be evaluated in any commutative algebra.
• TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.iff_forall_isUnipotentPoint: geometric unipotence can be characterized over any algebraically closed extension.
• TauCeti.smoothUnipotentCommHopfAlgProperty.isUnipotentPoint: the smooth finite-type specialization, where reducedness follows from smoothness.
• TauCeti.smoothUnipotentCommHopfAlgProperty.iff_smooth_and_forall_isUnipotentPoint: the corresponding characterization for smooth unipotence.

References

• A. Borel, Linear Algebraic Groups, Proposition 14.4, for the unipotent-radical application.

This supplies the reduced-source descent input for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.coefficientMatrix_charpoly_eq {k : Type u} [Field k] {A : CommHopfAlgCat k} [Algebra.FiniteType k ↑A] [IsReduced ↑A] (hA : geometricallyUnipotentPointsCommHopfAlgProperty k A) (M : FGComoduleCat k ↑A) {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι k ↑M) : (Comodule.coefficientMatrix b).charpoly = Polynomial.map (algebraMap k ↑A) ((Polynomial.X - 1) ^ Module.finrank k ↑M)

For a geometrically unipotent reduced finite-type Hopf algebra, the characteristic polynomial of every universal coefficient matrix is a power of X - 1.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.isUnipotentPoint {k : Type u} [Field k] {A : CommHopfAlgCat k} [Algebra.FiniteType k ↑A] [IsReduced ↑A] (hA : geometricallyUnipotentPointsCommHopfAlgProperty k A) {L : Type w} [CommRing L] [Algebra k L] (g : WithConv (↑A →ₐ[k] L)) : HopfAlgebra.IsUnipotentPoint g

If a reduced finite-type Hopf algebra is geometrically unipotent, every point valued in any commutative algebra over the ground field is unipotent. In particular, the defining hypothesis over the chosen algebraic closure implies unipotence for points over every other algebraically closed extension.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.iff_forall_isUnipotentPoint {k : Type u} [Field k] {A : CommHopfAlgCat k} [Algebra.FiniteType k ↑A] [IsReduced ↑A] (L : Type w) [Field L] [Algebra k L] [IsAlgClosed L] : geometricallyUnipotentPointsCommHopfAlgProperty k A ↔ ∀ (g : WithConv (↑A →ₐ[k] L)), HopfAlgebra.IsUnipotentPoint g

A reduced finite-type Hopf algebra is geometrically unipotent if and only if every point valued in any fixed algebraically closed extension is unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_injective_of_reduced {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (hf : Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)) [Algebra.FiniteType k ↑K] [IsReduced ↑K] (hK : geometricallyUnipotentPointsCommHopfAlgProperty k K) : geometricallyUnipotentPointsCommHopfAlgProperty k H

Geometric unipotence descends along an injective morphism of coordinate Hopf algebras whose codomain is reduced and finite type.

Contravariantly, the morphism represents a schematically dense homomorphism from Spec K to Spec H. For a finite-dimensional H-comodule, every geometric point of Spec K makes the characteristic polynomial of the restricted action equal to (X - 1) ^ n. Point separation in the reduced algebra K gives the same identity for the universal coefficient matrix. Injectivity then reflects it to H, where evaluation proves that every geometric point of Spec H acts unipotently.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.isUnipotentPoint {k : Type u} [Field k] {A : FiniteTypeCommHopfAlgCat k} (hA : smoothUnipotentCommHopfAlgProperty k A) {L : Type w} [CommRing L] [Algebra k L] (g : WithConv (↑A.obj →ₐ[k] L)) : HopfAlgebra.IsUnipotentPoint g

Every point of a smooth geometrically unipotent affine group valued in a commutative algebra over the ground field is unipotent.

theorem TauCeti.smoothUnipotentCommHopfAlgProperty.iff_smooth_and_forall_isUnipotentPoint {k : Type u} [Field k] {A : FiniteTypeCommHopfAlgCat k} (L : Type w) [Field L] [Algebra k L] [IsAlgClosed L] : smoothUnipotentCommHopfAlgProperty k A ↔ Algebra.Smooth k ↑A.obj ∧ ∀ (g : WithConv (↑A.obj →ₐ[k] L)), HopfAlgebra.IsUnipotentPoint g

A finite-type Hopf algebra is smooth unipotent if and only if it is smooth and every point valued in any fixed algebraically closed extension is unipotent.