Reductivity of the special orthogonal groups

Let SOₙ be the special orthogonal group of the standard symmetric form over a field of characteristic different from two. In dimension at least three, every normal smooth unipotent closed subgroup of SOₙ is trivial. Equivalently, its unipotent radical is trivial.

The standard representation supplies the decisive input. It is faithful in every dimension and simple in dimension at least three, hence completely reducible. The general normal-invariants theorem then forces a normal smooth unipotent subgroup to act trivially, and faithfulness identifies its defining Hopf ideal with the augmentation ideal.

Smoothness is already known away from characteristic two, and so is geometric connectedness, so reductivity follows in dimension at least three. Together with the dimension-zero and dimension-one cases, where the group is special linear, and the dimension-two case, where it is a torus, this makes every standard special orthogonal group reductive away from characteristic two.

Main declarations

• TauCeti.SpecialOrthogonal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_three_le: every normal smooth unipotent closed subgroup of SOₙ is trivial when 3 ≤ n.
• TauCeti.SpecialOrthogonal.unipotentRadicalDefiningIdeal_eq_augmentation_of_three_le: the unipotent radical of SOₙ is trivial when 3 ≤ n.
• TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_iff_geometricallyConnected_of_three_le: in these dimensions and characteristics, SOₙ is reductive exactly when it is geometrically connected.
• TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra: SOₙ is reductive in every dimension, over every field of characteristic different from two.

References

• J. S. Milne, Algebraic Groups (2017), §§ 4.a, 19.b, and 21.
• T. A. Springer, Linear Algebraic Groups, §§ 2.2, 2.4, and Chapter 8.
• Formal proof architecture: TauCeti.Algebra.AlgebraicGroup.Symplectic.Reductive.

theorem TauCeti.SpecialOrthogonal.eq_augmentation_of_isNormal_of_smoothUnipotent_of_three_le (k : Type u) [Field k] [IsAlgClosed k] [NeZero 2] (n : ℕ) (hn : 3 ≤ n) (I : HopfIdeal k ↑(finiteTypeCoordinateHopfAlgebra k n).obj) (hI : I.IsNormal) (hU : smoothUnipotentCommHopfAlgProperty k ((finiteTypeCoordinateHopfAlgebra k n).quotient I)) : I = HopfIdeal.augmentation k ↑(finiteTypeCoordinateHopfAlgebra k n).obj

Every normal smooth unipotent closed subgroup of SOₙ is trivial in dimension at least three, over an algebraically closed field of characteristic different from two.

The conclusion is contravariant: the defining Hopf ideal of the subgroup is the augmentation ideal of the special-orthogonal coordinate algebra.

theorem TauCeti.SpecialOrthogonal.unipotentRadicalDefiningIdeal_eq_augmentation_of_three_le (k : Type u) [Field k] [IsAlgClosed k] [NeZero 2] (n : ℕ) (hn : 3 ≤ n) : (finiteTypeCoordinateHopfAlgebra k n).unipotentRadicalDefiningIdeal = HopfIdeal.augmentation k ↑(finiteTypeCoordinateHopfAlgebra k n).obj

The unipotent radical of SOₙ is trivial in dimension at least three over an algebraically closed field of characteristic different from two.

theorem TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_iff_geometricallyConnected_of_three_le (k : Type u) [Field k] [NeZero 2] (n : ℕ) (hn : 3 ≤ n) : reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k n) ↔ geometricallyConnectedCommHopfAlgProperty k (coordinateHopfAlgebra k n)

In dimension at least three and characteristic different from two, SOₙ is reductive if and only if it is geometrically connected.

Smoothness and triviality of every normal smooth unipotent subgroup of the geometric fibre are automatic under these hypotheses, so geometric connectedness is the only remaining condition.

theorem TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra (k : Type u) [Field k] [NeZero 2] (n : ℕ) : reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k n)

Every standard special orthogonal group is reductive, over every field of characteristic different from two.

The dimension-zero and dimension-one groups are special linear, the dimension-two group is a torus, and from dimension three on the standard representation is simple, which makes the unipotent radical trivial.