The standard representation of the special orthogonal group

The standard representation of the special orthogonal group scheme SOₙ is obtained by corestricting the standard O(GLₙ)-comodule along the quotient coordinate morphism

O(GLₙ) ⟶ O(SOₙ).

This representation is faithful in every rank. Its action on algebra-valued points is ordinary matrix-vector multiplication by the corresponding special orthogonal matrix. Consequently every subcomodule is stable under the action of every base-valued special orthogonal matrix.

Main declarations

• TauCeti.SpecialOrthogonal.standardComodule: the standard O(SOₙ)-comodule on Rⁿ.
• TauCeti.SpecialOrthogonal.isFaithful_standardComodule: the standard comodule is faithful.
• TauCeti.SpecialOrthogonal.piScalarRight_comp_endOfPoint: a point acts after scalar extension by its special orthogonal matrix.
• TauCeti.SpecialOrthogonal.mulVec_mem: standard subcomodules are stable under special orthogonal matrices.

References

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

The construction follows the corestriction and point-action interface of TauCeti.Algebra.AlgebraicGroup.SpecialLinear.StandardComodule.

@[instance_reducible]

noncomputable def TauCeti.SpecialOrthogonal.standardComodule (R : Type u) [CommRing R] (n : ℕ) : Comodule R (↑(coordinateHopfAlgebra R n)) (Fin n → R)

The standard right comodule of the special orthogonal coordinate Hopf algebra, obtained by corestricting the standard GLₙ-comodule along the special orthogonal quotient map.

Equations

• TauCeti.SpecialOrthogonal.standardComodule R n = TauCeti.Comodule.Corestrict (CommHopfAlgCat.Hom.hom (TauCeti.SpecialOrthogonal.coordinateMap R n)).toCoalgHom

@[simp]

theorem TauCeti.SpecialOrthogonal.standardComodule_coact (R : Type u) [CommRing R] (n : ℕ) : have x := GeneralLinear.standardComodule R n; Comodule.corestrictCoact (CommHopfAlgCat.Hom.hom (coordinateMap R n)).toCoalgHom = TensorProduct.map LinearMap.id (Bialgebra.Quotient.mkBialgHom (definingHopfIdeal R n).toIdeal).toLinearMap ∘ₗ GeneralLinear.standardCoact R n

The standard special orthogonal coaction is the standard general-linear coaction followed by the quotient map on the coordinate factor.

theorem TauCeti.SpecialOrthogonal.isFaithful_standardComodule (R : Type u) [CommRing R] (n : ℕ) : Comodule.IsFaithful

The standard comodule of SOₙ is faithful.

theorem TauCeti.SpecialOrthogonal.piScalarRight_comp_endOfPoint (R : Type u) [CommRing R] (n : ℕ) {A : Type u_1} [CommRing A] [Algebra R A] (g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)) : ↑(TensorProduct.piScalarRight R A A (Fin n)) ∘ₗ Comodule.endOfPoint (Fin n → R) g.ofConv = (↑((pointsMulEquiv R n) g)).mulVecLin ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin n))

Under the canonical scalar-extension identification A ⊗[R] Rⁿ ≃ Aⁿ, a point of SOₙ acts on the standard comodule by multiplication with its special orthogonal matrix.

theorem TauCeti.SpecialOrthogonal.mulVec_mem (R : Type u) [CommRing R] (n : ℕ) (N : Subcomodule R (↑(coordinateHopfAlgebra R n)) (Fin n → R)) (g : ↥(Matrix.specialOrthogonalGroup (Fin n) R)) {w : Fin n → R} (hw : w ∈ N) : (↑g).mulVec w ∈ N

A subcomodule of the standard special orthogonal comodule is stable under every special orthogonal matrix.