Naturality of unipotent points in the value algebra

A point of an affine group remains unipotent after extending its value algebra. More precisely, postcomposing a point g : H →ₐ[R] A with φ : A →ₐ[R] B extends every point action from A ⊗[R] V to B ⊗[R] V, so nilpotence of the difference from the identity is preserved. If φ is injective and V is flat over R, this extension also reflects nilpotence. Consequently, over a field, unipotence of a point is invariant under every injective extension of its value algebra, in particular under field extensions.

The proof uses the existing intertwining identity TauCeti.Comodule.rTensor_comp_endOfPoint. It first upgrades that identity from point actions to their powers after subtracting the identity. Preservation follows because pure tensors in the larger scalar extension are scalar multiples of tensors coming from the smaller one; reflection uses flatness to make the comparison map injective.

Main declarations

• TauCeti.Comodule.isNilpotent_endOfPoint_comp: nilpotence of a point action is preserved by postcomposition in the value algebra.
• TauCeti.Comodule.isNilpotent_endOfPoint_comp_iff_of_injective: under flatness, an injective postcomposition preserves and reflects nilpotence.
• TauCeti.HopfAlgebra.IsUnipotentPoint.mapValue: unipotent points remain unipotent after changing the value algebra.
• TauCeti.HopfAlgebra.isUnipotentPoint_mapValue_iff_of_injective: over a field, injective changes of the value algebra preserve and reflect unipotence.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, §2.4.

This supplies value-field naturality for the geometric unipotence criterion in Layer 5, "Unipotent groups", of the ReductiveGroups roadmap. It is needed to compare geometric points across algebraic closures and field extensions.

theorem TauCeti.Comodule.isNilpotent_endOfPoint_comp {R : Type u} {H : Type v} {V : Type w} {A : Type x} {B : Type y} [CommRing R] [Semiring H] [HopfAlgebra R H] [AddCommGroup V] [Module R V] [Comodule R H V] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] (g : H →ₐ[R] A) (φ : A →ₐ[R] B) (hg : IsNilpotent (endOfPoint V g - 1)) : IsNilpotent (endOfPoint V (φ.comp g) - 1)

Nilpotence of a point action after subtracting the identity is preserved by postcomposition with a morphism of value algebras.

theorem TauCeti.Comodule.isNilpotent_endOfPoint_comp_iff_of_injective {R : Type u} {H : Type v} {V : Type w} {A : Type x} {B : Type y} [CommRing R] [Semiring H] [HopfAlgebra R H] [AddCommGroup V] [Module R V] [Comodule R H V] [CommRing A] [Algebra R A] [CommRing B] [Algebra R B] [Module.Flat R V] (g : H →ₐ[R] A) (φ : A →ₐ[R] B) (hφ : Function.Injective ⇑φ) : IsNilpotent (endOfPoint V (φ.comp g) - 1) ↔ IsNilpotent (endOfPoint V g - 1)

If the coefficient module is flat, postcomposition with an injective morphism of value algebras preserves and reflects nilpotence of a point action after subtracting the identity.

theorem TauCeti.HopfAlgebra.IsUnipotentPoint.mapValue {k : Type u} {H : Type v} {K : Type w} {L : Type x} [CommRing k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] [CommRing L] [Algebra k L] {g : WithConv (H →ₐ[k] K)} (hg : IsUnipotentPoint g) (φ : K →ₐ[k] L) : IsUnipotentPoint ((AlgHom.mapValue φ) g)

A unipotent point remains unipotent after postcomposition with a morphism of value algebras.

theorem TauCeti.HopfAlgebra.isUnipotentPoint_mapValue_iff_of_injective {k : Type u} {H : Type v} {K : Type w} {L : Type x} [Field k] [Semiring H] [HopfAlgebra k H] [CommRing K] [Algebra k K] [CommRing L] [Algebra k L] (g : WithConv (H →ₐ[k] K)) (φ : K →ₐ[k] L) (hφ : Function.Injective ⇑φ) : IsUnipotentPoint ((AlgHom.mapValue φ) g) ↔ IsUnipotentPoint g

Over a field, postcomposition with an injective morphism of value algebras preserves and reflects unipotence of points.

@[simp]

theorem TauCeti.HopfAlgebra.isUnipotentPoint_toConv_comp_iff {k : Type u} {H : Type v} {K : Type w} {L : Type x} [Field k] [Semiring H] [HopfAlgebra k H] [Field K] [Algebra k K] [Field L] [Algebra k L] (g : WithConv (H →ₐ[k] K)) (φ : K →ₐ[k] L) : IsUnipotentPoint (WithConv.toConv (φ.comp g.ofConv)) ↔ IsUnipotentPoint g

Unipotence of a point is invariant under extension of its value field.