A linearly reductive unipotent affine group is trivial

Let H be a reduced finite-type commutative Hopf algebra over an algebraically closed field k all of whose points are unipotent. Kolchin's theorem, in the form already available from TauCeti.Algebra.AlgebraicGroup.Unipotent.Embedding, gives a nonzero fixed vector in every nonzero finite-dimensional comodule, hence in every nonzero subcomodule of one. If H is also linearly reductive, the fixed subcomodule of a finite-dimensional comodule has a subcomodule complement, which then has no nonzero fixed vector and so vanishes: the coaction of every finite-dimensional comodule is trivial.

Applying this to the finite-dimensional subcoalgebras of the regular comodule, which exhaust H over a field, gives Δ h = h ⊗ 1 for every h, hence h = ε(h) · 1. So the counit is injective, the augmentation ideal vanishes, and the counit is a bialgebra equivalence H ≃ k; equivalently the group of points over every commutative value algebra is trivial.

Smoothness may replace reducedness, since a smooth algebra over a field is reduced. That is the form the roadmap's definitions are stated in, so it is also given for the object properties TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty and TauCeti.linearlyReductiveCommHopfAlgProperty.

Main declarations

• TauCeti.Comodule.exists_mem_ne_zero_coact_eq_tmul_one_of_forall_isUnipotentPoint: every nonzero subcomodule of a finite-dimensional comodule over a unipotent group has a nonzero fixed vector.
• TauCeti.Comodule.coact_eq_tmul_one_of_isCompletelyReducible_of_forall_isUnipotentPoint: a unipotent group acts trivially on every completely reducible finite-dimensional representation.
• TauCeti.HopfAlgebra.comul_eq_tmul_one_of_isLinearlyReductive_of_forall_exists_fixed: the regular comodule of a linearly reductive coalgebra with enough fixed vectors is trivial; this is the step of the argument that does not mention unipotence.
• TauCeti.HopfAlgebra.comul_eq_tmul_one_of_isLinearlyReductive_of_forall_isUnipotentPoint and TauCeti.HopfAlgebra.eq_counit_smul_one_of_isLinearlyReductive_of_forall_isUnipotentPoint: the coordinate algebra of a linearly reductive unipotent group is spanned by 1.
• TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint: a linearly reductive unipotent affine group is trivial, together with its smooth form TauCeti.HopfAlgebra.counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint and the object-property form counitBialgEquivOfLinearlyReductive in the TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty namespace.
• TauCeti.HopfAlgebra.subsingleton_algHom_of_isLinearlyReductive_of_forall_isUnipotentPoint: the functor-of-points form of triviality.

References

• J. S. Milne, Algebraic Groups (2017), Corollary 12.45 and §22.42: a linearly reductive group has no nontrivial unipotent normal subgroup, of which this is the case where the whole group is unipotent.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §3.2 and §8.3.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

This is the first theorem relating the two Layer 6 notions of the ReductiveGroups roadmap, reductivity defined by a trivial geometric unipotent radical and linear reductivity defined by complete reducibility. It is the step that rules out unipotent subgroups; deducing reductivity from linear reductivity in general still needs the invariants of a normal closed subgroup to be a subrepresentation of the ambient group.

theorem TauCeti.Comodule.exists_mem_ne_zero_coact_eq_tmul_one_of_forall_isUnipotentPoint {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] {M : Type w} [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 : Subcomodule k H M) (hN : N ≠ ⊥) : ∃ v ∈ N, v ≠ 0 ∧ coact v = v ⊗ₜ[k] 1

Kolchin's theorem, applied to a nonzero subcomodule: over a reduced finite-type commutative Hopf algebra with unipotent points, every nonzero subcomodule of a finite-dimensional comodule contains a nonzero vector fixed by the ambient coaction.

theorem TauCeti.Comodule.coact_eq_tmul_one_of_isCompletelyReducible_of_forall_isUnipotentPoint {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] {M : Type w} [AddCommGroup M] [Module k M] [Comodule k H M] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] [FiniteDimensional k M] (hcr : IsCompletelyReducible k H M) (hH : ∀ (g : WithConv (H →ₐ[k] k)), HopfAlgebra.IsUnipotentPoint g) (m : M) : coact m = m ⊗ₜ[k] 1

If a finite-dimensional comodule over a reduced finite-type commutative Hopf algebra with unipotent points is completely reducible, then the coaction is trivial on it: the represented unipotent group acts trivially on every completely reducible representation.

theorem TauCeti.HopfAlgebra.comul_eq_tmul_one_of_isLinearlyReductive_of_forall_exists_fixed (k' : Type u) (H' : Type v) [Field k'] [AddCommGroup H'] [Module k' H'] [Coalgebra k' H'] [One H'] (hlr : Coalgebra.IsLinearlyReductive k' H') (hfix : ∀ (V : Type v) [inst : AddCommGroup V] [inst_1 : Module k' V] [inst_2 : Comodule k' H' V] [FiniteDimensional k' V] (N : Subcomodule k' H' V), N ≠ ⊥ → ∃ v ∈ N, v ≠ 0 ∧ Comodule.coact v = v ⊗ₜ[k'] 1) (h : H') : CoalgebraStruct.comul h = h ⊗ₜ[k'] 1

If H is linearly reductive and every nonzero subcomodule of a finite-dimensional comodule contains a nonzero fixed vector, then comultiplication sends every element h to h ⊗ 1: the regular comodule is trivial.

This is the coalgebra-level core of the triviality theorem. The element h lies in a finite-dimensional subcoalgebra, hence in a finite-dimensional subcomodule of the regular comodule, on which complete reducibility and the supply of fixed vectors force the coaction to be trivial. Unipotence enters only through that supply of fixed vectors.

theorem TauCeti.HopfAlgebra.comul_eq_tmul_one_of_isLinearlyReductive_of_forall_isUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (h : H) : CoalgebraStruct.comul h = h ⊗ₜ[k] 1

In a linearly reductive reduced finite-type commutative Hopf algebra over an algebraically closed field with unipotent points, comultiplication sends every element h to h ⊗ 1: the regular comodule is trivial.

theorem TauCeti.HopfAlgebra.eq_counit_smul_one_of_isLinearlyReductive_of_forall_isUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (h : H) : h = CoalgebraStruct.counit h • 1

Under the same hypotheses every element is a scalar multiple of 1, the scalar being its counit.

theorem TauCeti.HopfAlgebra.augmentation_eq_bot_of_isLinearlyReductive_of_forall_isUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) : HopfIdeal.augmentation k H = ⊥

Under the same hypotheses the augmentation ideal vanishes: the counit is injective.

noncomputable def TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) : H ≃ₐc[k] k

A linearly reductive unipotent affine group is trivial.

A reduced finite-type commutative Hopf algebra over an algebraically closed field, all of whose points are unipotent, is bialgebra-equivalent to the ground field via its counit as soon as it is linearly reductive.

Equations

• TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hlr hH = TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot ⋯

@[simp]

theorem TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint_apply (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (x : H) : (counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hlr hH) x = (Bialgebra.counitBialgHom k H) x

The triviality equivalence is the counit.

@[simp]

theorem TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint_symm_apply (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (r : k) : (counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hlr hH).symm r = (algebraMap k H) r

The inverse of the triviality equivalence is the structure map.

theorem TauCeti.HopfAlgebra.subsingleton_algHom_of_isLinearlyReductive_of_forall_isUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] [IsReduced H] (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (A : Type w) [CommRing A] [Algebra k A] : Subsingleton (H →ₐ[k] A)

Under the same hypotheses the group of points over every commutative value algebra is trivial: this is the functor-of-points form of the statement that the group is trivial.

noncomputable def TauCeti.HopfAlgebra.counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hsm : Algebra.Smooth k H) (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) : H ≃ₐc[k] k

The smooth form of TauCeti.HopfAlgebra.counitBialgEquivOfIsLinearlyReductiveOfForallIsUnipotentPoint: over a field, smoothness supplies the reducedness hypothesis.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.HopfAlgebra.counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint_apply (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hsm : Algebra.Smooth k H) (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (x : H) : (counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hsm hlr hH) x = (Bialgebra.counitBialgHom k H) x

The smooth triviality equivalence is the counit.

@[simp]

theorem TauCeti.HopfAlgebra.counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint_symm_apply (k : Type u) (H : Type v) [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hsm : Algebra.Smooth k H) (hlr : Coalgebra.IsLinearlyReductive k H) (hH : ∀ (g : WithConv (H →ₐ[k] k)), IsUnipotentPoint g) (r : k) : (counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hsm hlr hH).symm r = (algebraMap k H) r

The inverse of the smooth triviality equivalence is the structure map.

noncomputable def TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.counitBialgEquivOfLinearlyReductive {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hu : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) (hsm : Algebra.Smooth k H) (hlr : linearlyReductiveCommHopfAlgProperty k ↧H) : H ≃ₐc[k] k

A smooth linearly reductive unipotent affine group of finite type over an algebraically closed field is trivial, stated for the object properties on commutative Hopf algebras: the counit is a bialgebra equivalence onto the ground field.

Equations

• hu.counitBialgEquivOfLinearlyReductive hsm hlr = TauCeti.HopfAlgebra.counitBialgEquivOfSmoothOfIsLinearlyReductiveOfForallIsUnipotentPoint k H hsm ⋯ ⋯

@[simp]

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.counitBialgEquivOfLinearlyReductive_apply {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hu : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) (hsm : Algebra.Smooth k H) (hlr : linearlyReductiveCommHopfAlgProperty k ↧H) (x : H) : (hu.counitBialgEquivOfLinearlyReductive hsm hlr) x = (Bialgebra.counitBialgHom k H) x

The object-property triviality equivalence is the counit.

@[simp]

theorem TauCeti.geometricallyUnipotentPointsCommHopfAlgProperty.counitBialgEquivOfLinearlyReductive_symm_apply {k : Type u} {H : Type v} [Field k] [CommRing H] [HopfAlgebra k H] [IsAlgClosed k] [Algebra.FiniteType k H] (hu : geometricallyUnipotentPointsCommHopfAlgProperty k ↧H) (hsm : Algebra.Smooth k H) (hlr : linearlyReductiveCommHopfAlgProperty k ↧H) (r : k) : (hu.counitBialgEquivOfLinearlyReductive hsm hlr).symm r = (algebraMap k H) r

The inverse of the object-property triviality equivalence is the structure map.