The standard representation of the general linear group

This file defines the tautological representation of GL n k on column vectors, together with its finite-dimensional and dual forms. Its action and character are identified with matrix-vector multiplication and the matrix trace.

Main definitions

• TauCeti.stdRep: the standard representation of GL n k.
• TauCeti.stdFDRep: the standard representation as a finite-dimensional representation.
• TauCeti.stdDualRep: the contragredient of the standard representation.

References

• Classical groups roadmap
• Suggested declarations

def TauCeti.stdRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (GL (Fin n) k) (Fin n → k)

The standard representation of GL n k on column vectors.

Equations

• TauCeti.stdRep k n = (Units.coeHom ((Fin n → k) →ₗ[k] Fin n → k)).comp Matrix.GeneralLinearGroup.toLin.toMonoidHom

@[simp]

theorem TauCeti.stdRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : GL (Fin n) k) : (stdRep k n) g = (↑g).mulVecLin

The standard representation acts by matrix-vector multiplication.

theorem TauCeti.stdRep_apply_apply (k : Type u) (n : ℕ) [CommRing k] (g : GL (Fin n) k) (v : Fin n → k) : ((stdRep k n) g) v = (↑g).mulVec v

Evaluation of the standard action is matrix-vector multiplication.

theorem TauCeti.stdRep_injective (k : Type u) (n : ℕ) [CommRing k] : Function.Injective ⇑(stdRep k n)

The standard representation is faithful.

@[reducible, inline]

noncomputable abbrev TauCeti.stdFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k (GL (Fin n) k)

The standard representation of GL n k, bundled as an object of FDRep.

Equations

• TauCeti.stdFDRep k n = FDRep.of (TauCeti.stdRep k n)

@[simp]

theorem TauCeti.char_stdRep (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (stdRep k n).character g = (↑g).trace

The character of the standard representation is the matrix trace.

@[simp]

theorem TauCeti.char_stdFDRep (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (stdFDRep k n).character g = (↑g).trace

The character of the bundled standard representation is the matrix trace.

noncomputable def TauCeti.stdDualRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (GL (Fin n) k) (Module.Dual k (Fin n → k))

The dual, or contragredient, of the standard representation.

Equations

• TauCeti.stdDualRep k n = (TauCeti.stdRep k n).dual

@[simp]

theorem TauCeti.stdDualRep_apply (k : Type u) (n : ℕ) [CommRing k] (g : GL (Fin n) k) : (stdDualRep k n) g = Module.Dual.transpose (↑g⁻¹).mulVecLin

The dual standard action is the transpose of the inverse standard action.

@[reducible, inline]

noncomputable abbrev TauCeti.stdDualFDRep (k : Type u) (n : ℕ) [CommRing k] : FDRep k (GL (Fin n) k)

The dual standard representation, bundled as an object of FDRep.

Equations

• TauCeti.stdDualFDRep k n = FDRep.of (TauCeti.stdDualRep k n)

@[simp]

theorem TauCeti.char_stdDualRep (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (stdDualRep k n).character g = (↑g⁻¹).trace

The character of the dual standard representation is the trace at the inverse matrix.

@[simp]

theorem TauCeti.char_stdDualFDRep (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (stdDualFDRep k n).character g = (↑g⁻¹).trace

The character of the bundled dual standard representation is the inverse matrix trace.