The standard representation of the special linear group

The standard representation of SL_n is obtained by restricting the standard representation of GL_n along the determinant-one closed immersion. In coordinate algebras, this is corestriction of the standard O(GL_n)-comodule along the quotient map

O(GL_n) ⟶ O(SL_n).

This representation is faithful in every rank. Over a field it is simple in every positive rank. For n ≥ 2, the special linear group acts transitively on nonzero column vectors, so a nonzero invariant subspace contains every nonzero vector; rank one follows from one-dimensional submodule theory.

Main declarations

• TauCeti.SpecialLinear.standardComodule: the standard O(SL_n)-comodule on R^n.
• TauCeti.SpecialLinear.isFaithful_standardComodule: the standard representation is faithful.
• TauCeti.SpecialLinear.mulVec_mem: a standard subcomodule is stable under every determinant-one matrix.
• TauCeti.SpecialLinear.instIsSimpleOrderSubcomodule: over a field, the standard comodule is simple in every positive rank.

References

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

The construction and the invariant-subspace argument extend TauCeti.Algebra.AlgebraicGroup.GeneralLinear.StandardComodule; the determinant-correction step is new here.

Faithfulness and simplicity are the representation-theoretic inputs for proving that SL_n is reductive, one of the worked examples accompanying Layer 6 of the ReductiveGroups roadmap.

@[instance_reducible]

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

The standard right comodule of the special linear coordinate Hopf algebra, obtained by corestricting the standard GL_n-comodule along the determinant-one quotient map.

Equations

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

@[simp]

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

The standard SL_n coaction is the standard GL_n coaction followed by the quotient map on the coordinate factor.

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

The standard comodule of SL_n is faithful.

theorem TauCeti.SpecialLinear.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 = ↑(Matrix.GeneralLinearGroup.toLin (Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R n) g))) ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin n))

Under the canonical scalar-extension identification A ⊗[R] R^n ≃ A^n, a point of SL_n acts on the standard comodule by multiplication with its determinant-one matrix.

theorem TauCeti.SpecialLinear.basePointsRepresentation_eq_mulVec (R : Type u) [CommRing R] (n : ℕ) (g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] R)) (v : Fin n → R) : ((Comodule.basePointsRepresentation (Fin n → R)) g) v = (↑((pointsMulEquiv R n) g)).mulVec v

A base-valued point acts on the standard special-linear comodule by its matrix.

theorem TauCeti.SpecialLinear.scalar_pow_eq_one_of_basePointsRepresentation_eq_smul {R : Type u} [CommRing R] {n : ℕ} (g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] R)) (c : R) (hc : (Comodule.basePointsRepresentation (Fin n → R)) g = c • 1) : c ^ n = 1

A scalar point in the standard representation of SL_n has scalar an nth root of unity.

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

A subcomodule of the standard comodule of SL_n is stable under every determinant-one matrix.

instance TauCeti.SpecialLinear.instIsSimpleOrderSubcomodule (k : Type u) [Field k] (m : ℕ) [NeZero m] : IsSimpleOrder (Subcomodule k (↑(coordinateHopfAlgebra k m)) (Fin m → k))

The standard comodule of SL_m over a field is simple for m ≠ 0: its only subcomodules are the zero comodule and the whole column space.