Embedding unipotent affine groups in upper-unitriangular groups

Let H be a reduced finite-type commutative Hopf algebra over an algebraically closed field k. If every k-valued point of H is unipotent, Kolchin's common fixed vector theorem gives a nonzero fixed vector in every nonzero finite-dimensional H-comodule. Point separation promotes the pointwise fixed-vector equation to the comodule equation v ↦ v ⊗ 1. Induction on dimension then produces a basis in which the coefficient matrix is upper unitriangular.

Applying this to a faithful finite-dimensional subcomodule of the regular comodule gives a closed immersion of the represented affine group into some upper-unitriangular group U_n. The geometric unipotence property implies the required hypothesis on k-points by extension to the chosen algebraic closure.

Reducedness is explicit in this file because it is exactly the hypothesis used by point separation. A future smooth-implies-geometrically-reduced theorem will discharge it for the roadmap's smooth formulation.

Main declarations

• TauCeti.Comodule.hasNonzeroFixedVector_of_forall_isNilpotent_endOfPoint_sub_one: Kolchin's theorem promoted from point actions to a comodule fixed vector.
• TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperUnitriangular_of_forall_isUnipotentPoint: every finite-dimensional comodule has an upper-unitriangular basis.
• iff_exists_isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom in the TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty namespace: the upper-unitriangular embedding characterization.
• iff_exists_isClosedImmersion_upperUnitriangularGroupScheme in that namespace: the represented affine group is geometrically unipotent exactly when it embeds as a closed subgroup of some U_n.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.2.
• T. A. Springer, Linear Algebraic Groups, Proposition 2.4.12: a subgroup of GLₙ consisting of unipotent matrices is conjugate into Uₙ. A. Borel, Linear Algebraic Groups, §4.8 has the same statement, with its Corollary the closed-subgroup form proved here.

This closes the Kolchin and faithful-embedding step of Layer 5, "Unipotent groups", of the ReductiveGroups roadmap for reduced groups over an algebraically closed field.

theorem TauCeti.Comodule.hasNonzeroFixedVector_of_forall_isNilpotent_endOfPoint_sub_one {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] [Nontrivial M] (hM : ∀ (g : WithConv (H →ₐ[k] k)), IsNilpotent (endOfPoint M g.ofConv - 1)) : HasNonzeroFixedVector k H M

If every point acts nilpotently minus the identity on a given comodule over a reduced finite-type commutative Hopf algebra over an algebraically closed field, then that comodule has a nonzero fixed vector.

theorem TauCeti.Comodule.hasNonzeroFixedVector_of_forall_isUnipotentPoint {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] [Nontrivial M] (hH : ∀ (g : WithConv (H →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : HasNonzeroFixedVector k H M

If every point of a reduced finite-type commutative Hopf algebra over an algebraically closed field is unipotent, then every nonzero finite-dimensional comodule has a nonzero fixed vector.

theorem TauCeti.Comodule.exists_basis_coefficientMatrix_isUpperUnitriangular_of_forall_isUnipotentPoint {k : Type u} {H : Type v} {M : Type w} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] (hH : ∀ (g : WithConv (H →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : ∃ (n : ℕ) (b : Module.Basis (Fin n) k M), (coefficientMatrix b).IsUpperUnitriangular

If all points are unipotent, every finite-dimensional comodule has a basis with upper unitriangular coefficient matrix.

theorem TauCeti.Comodule.upperUnitriangularCoordinateGroupSchemeHom.exists_isClosedImmersion_of_forall_isUnipotentPoint {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hH : ∀ (g : WithConv (H →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) : ∃ (M : Subcomodule k H H) (n : ℕ) (b : Module.Basis (Fin n) k ↥M) (hb : (coefficientMatrix b).IsUpperUnitriangular), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (upperUnitriangularCoordinateGroupSchemeHom b hb).hom.hom)

A reduced finite-type affine group over an algebraically closed field whose points are all unipotent embeds as a closed subgroup of an upper-unitriangular group. The witness includes the faithful comodule and its upper-unitriangular basis.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.forall_isUnipotentPoint {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] (hH : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) (g : WithConv (H →ₐ[k] k)) : HopfAlgebra.IsUnipotentPoint g

Geometric unipotence implies that every point valued in the ground field is unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom {k H M : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [AddCommGroup M] [Module k M] [Comodule k H M] {n : ℕ} (b : Module.Basis (Fin n) k M) (hb : (Comodule.coefficientMatrix b).IsUpperUnitriangular) (hclosed : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (Comodule.upperUnitriangularCoordinateGroupSchemeHom b hb).hom.hom)) : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H

A closed immersion given by an upper-unitriangular comodule makes the represented affine group geometrically unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.exists_isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hH : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) : ∃ (M : Subcomodule k H H) (n : ℕ) (b : Module.Basis (Fin n) k ↥M) (hb : (Comodule.coefficientMatrix b).IsUpperUnitriangular), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (Comodule.upperUnitriangularCoordinateGroupSchemeHom b hb).hom.hom)

Geometric unipotence implies that the represented reduced affine group has a faithful upper-unitriangular coordinate morphism.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.exists_isClosedImmersion_upperUnitriangularGroupScheme {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hH : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) : ∃ (n : ℕ) (f : (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op ↧H) ⟶ UpperUnitriangular.groupScheme k (Fin n)), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)

A geometrically unipotent reduced finite-type affine group over an algebraically closed field embeds as a closed subgroup of some upper-unitriangular group U_n.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.of_isClosedImmersion_upperUnitriangularGroupScheme {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] {n : ℕ} (f : (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op ↧H) ⟶ UpperUnitriangular.groupScheme k (Fin n)) (hclosed : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)) : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H

A closed immersion of the represented affine group into an upper-unitriangular group makes it geometrically unipotent.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.iff_exists_isClosedImmersion_upperUnitriangularGroupScheme {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H ↔ ∃ (n : ℕ) (f : (AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op ↧H) ⟶ UpperUnitriangular.groupScheme k (Fin n)), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left f.hom.hom)

A reduced finite-type affine group over an algebraically closed field is geometrically unipotent if and only if it embeds as a closed subgroup of some upper-unitriangular group U_n.

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.iff_exists_isClosedImmersion_upperUnitriangularCoordinateGroupSchemeHom {k H : Type u} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H ↔ ∃ (M : Subcomodule k H H) (n : ℕ) (b : Module.Basis (Fin n) k ↥M) (hb : (Comodule.coefficientMatrix b).IsUpperUnitriangular), AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (Comodule.upperUnitriangularCoordinateGroupSchemeHom b hb).hom.hom)

A reduced finite-type affine group over an algebraically closed field has only unipotent points if and only if a finite-dimensional subcomodule of its regular comodule has an upper-unitriangular basis whose coordinate morphism is a closed immersion into U_n.