The standard representation of the general linear group

The generic matrix defines a coaction of the coordinate Hopf algebra O(GLₙ) on the column space Rⁿ: the j-th standard basis vector goes to the j-th column of the generic matrix. This is the standard representation of GLₙ, and this file constructs it and establishes the properties of it that the structure theory uses.

It is faithful: its coefficient matrix is the generic matrix, so its coordinate morphism O(GLₙ) ⟶ O(GLₙ) is the identity, hence surjective, and the associated morphism of group schemes is a closed immersion.

Over a field and for n ≠ 0 it is simple: the only subcomodules of kⁿ are 0 and kⁿ. Contracting the coaction of a vector of a subcomodule against the linear functional given by a point of GLₙ valued in k shows that a subcomodule is stable under the action of every invertible matrix, and GL(n, k) is transitive on nonzero vectors.

Main declarations

• TauCeti.GeneralLinear.standardComodule: the standard comodule of O(GLₙ) on Rⁿ.
• TauCeti.GeneralLinear.isFaithful_standardComodule: the standard comodule is faithful.
• TauCeti.GeneralLinear.piScalarRight_comp_endOfPoint: a point acts on the standard comodule by the invertible matrix it names.
• TauCeti.GeneralLinear.mulVec_mem: a subcomodule of the standard comodule is stable under every invertible matrix.
• TauCeti.GeneralLinear.instIsSimpleOrderSubcomodule: over a field and in positive size, the standard comodule is simple.

References

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

Faithfulness and simplicity of the standard representation are the two representation-theoretic inputs to the statement that GLₙ is reductive. The remaining input is that the invariants of a normal closed subgroup form a subrepresentation.

Corestriction along the coordinate morphism O(GLₙ) → O(Uₙ) gives the standard upper-unitriangular comodule in TauCeti.Algebra.AlgebraicGroup.UpperUnitriangular.Unipotent.

noncomputable def TauCeti.GeneralLinear.standardCoact (R : Type u) [CommRing R] (n : ℕ) : (Fin n → R) →ₗ[R] TensorProduct R (Fin n → R) ↑(coordinateHopfAlgebra R n)

The standard coaction of O(GLₙ) on column vectors. On the j-th basis vector it is the j-th column of the generic matrix.

Equations

• TauCeti.GeneralLinear.standardCoact R n = TauCeti.Comodule.matrixCoact R (TauCeti.GeneralLinear.genericMatrix R n)

@[simp]

theorem TauCeti.GeneralLinear.standardCoact_apply_basisFun (R : Type u) [CommRing R] (n : ℕ) (j : Fin n) : (standardCoact R n) (Pi.single j 1) = ∑ i : Fin n, Pi.single i 1 ⊗ₜ[R] (coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))

The standard coaction on a basis vector is the corresponding column of the generic matrix.

@[instance_reducible]

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

The standard right comodule of the general linear coordinate Hopf algebra.

Equations

• TauCeti.GeneralLinear.standardComodule R n = TauCeti.Comodule.matrixComodule R (TauCeti.GeneralLinear.genericMatrix R n) ⋯ ⋯

theorem TauCeti.GeneralLinear.standardComodule_coact (R : Type u) [CommRing R] (n : ℕ) : Comodule.coact = standardCoact R n

The coaction of the standard comodule is standardCoact.

theorem TauCeti.GeneralLinear.coefficientMatrix_basisFun (R : Type u) [CommRing R] (n : ℕ) : Comodule.coefficientMatrix (Pi.basisFun R (Fin n)) = genericMatrix R n

The coefficient matrix of the standard comodule is the generic matrix.

@[simp]

theorem TauCeti.GeneralLinear.coordinateBialgHom_basisFun (R : Type u) [CommRing R] (n : ℕ) : Comodule.coordinateBialgHom (Pi.basisFun R (Fin n)) = BialgHom.id R ↑(coordinateHopfAlgebra R n)

The coordinate morphism of the standard comodule is the identity of O(GLₙ).

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

The standard comodule of GLₙ is faithful.

theorem TauCeti.GeneralLinear.rid_lTensor_comp_standardCoact (R : Type u) [CommRing R] (n : ℕ) (f : ↑(coordinateHopfAlgebra R n) →ₗ[R] R) : ↑(TensorProduct.rid R (Fin n → R)) ∘ₗ LinearMap.lTensor (Fin n → R) f ∘ₗ standardCoact R n = (Matrix.of fun (i j : Fin n) => f ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j))))).mulVecLin

Contracting the standard coaction against a linear functional on O(GLₙ) multiplies by the matrix of the functional's values on the generic entries.

@[simp]

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

A base-valued point acts on the standard comodule by multiplication with its matrix.

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

A subcomodule of the standard comodule of GLₙ is stable under every invertible matrix.

Standard comodules induced by coordinate morphisms

@[instance_reducible]

noncomputable def TauCeti.GeneralLinear.corestrictStandardComodule (R : Type u) [CommRing R] (n : ℕ) {H : Type u_1} [CommRing H] [HopfAlgebra R H] (f : ↑(coordinateHopfAlgebra R n) →ₐc[R] H) : Comodule R H (Fin n → R)

The standard comodule corestricted along a coordinate Hopf-algebra morphism.

Equations

• TauCeti.GeneralLinear.corestrictStandardComodule R n f = TauCeti.Comodule.Corestrict f.toCoalgHom

theorem TauCeti.GeneralLinear.isFaithful_corestrictStandardComodule (R : Type u) [CommRing R] (n : ℕ) {H : Type u} [CommRing H] [HopfAlgebra R H] (f : ↑(coordinateHopfAlgebra R n) →ₐc[R] H) (hf : Function.Surjective ⇑f) : have x := corestrictStandardComodule R n f; Comodule.IsFaithful

A surjective coordinate morphism gives a faithful corestricted standard representation.

theorem TauCeti.GeneralLinear.corestrictStandardComodule_mulVec_mem (R : Type u) [CommRing R] (n : ℕ) {H : Type u_1} [CommRing H] [HopfAlgebra R H] (f : ↑(coordinateHopfAlgebra R n) →ₐc[R] H) : have x := corestrictStandardComodule R n f; ∀ (N : Subcomodule R H (Fin n → R)) (g : WithConv (H →ₐ[R] R)) {w : Fin n → R}, w ∈ N → (↑(pointToGeneralLinear n ((AlgHom.mapDomain f) g))).mulVec w ∈ N

A subcomodule of the corestricted standard representation is stable under base-valued points, acting through their ambient invertible matrices.

theorem TauCeti.GeneralLinear.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 (pointToGeneralLinear n g)) ∘ₗ ↑(TensorProduct.piScalarRight R A A (Fin n))

Under the canonical scalar-extension identification A ⊗[R] Rⁿ ≃ Aⁿ, a point of GLₙ acts on the standard comodule by multiplication with the invertible matrix it names.

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

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