Irreducibility of the special orthogonal standard comodule

Over a field of characteristic different from two, the standard representation of SOₙ is irreducible in dimension at least three. Coordinate half-turns isolate a chosen coordinate of a vector in an invariant subspace, and coordinate rotations then carry that standard basis vector to every other one. Thus every nonzero subcomodule is the whole standard representation.

The dimension bound is sharp for this argument and for the statement: over an algebraically closed field, the standard representation of SO₂ is the sum of two one-dimensional characters. That representation is completely reducible but not irreducible.

Main declarations

• TauCeti.SpecialOrthogonal.isSimpleOrder_subcomodule_of_three_le: the subcomodules of the standard representation form a simple order in dimension at least three.
• TauCeti.SpecialOrthogonal.isCompletelyReducible_standardComodule_of_three_le: the standard representation is completely reducible in those dimensions.

References

• J. S. Milne, Algebraic Groups (2017), §§2.3 and 4.a.
• J. C. Jantzen, Representations of Algebraic Groups, I.2.

The proof uses the point-action interface of TauCeti.Algebra.AlgebraicGroup.SpecialOrthogonal.StandardComodule.

theorem TauCeti.SpecialOrthogonal.isSimpleOrder_subcomodule_of_three_le (k : Type u) [Field k] (n : ℕ) [NeZero 2] (hn : 3 ≤ n) : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra k n)) (Fin n → k))

The standard comodule of SOₙ is simple in dimension at least three over a field in characteristic different from two.

theorem TauCeti.SpecialOrthogonal.isCompletelyReducible_standardComodule_of_three_le (k : Type u) [Field k] (n : ℕ) [NeZero 2] (hn : 3 ≤ n) : Comodule.IsCompletelyReducible k (↑(coordinateHopfAlgebra k n)) (Fin n → k)

The standard comodule of SOₙ is completely reducible in dimension at least three over a field of characteristic different from two.