Determinant-power representations of the general linear group

This file packages the determinant and its integral powers as one-dimensional representations of the general linear group. These are the rational characters used to form determinant twists of polynomial representations.

Main definitions

• TauCeti.detPowerRep is the representation on the scalar module with action by det(g)^m.
• TauCeti.detRep is the determinant representation, the case m = 1.
• TauCeti.tprodDetPowerSLEquiv: the restriction of det^m ⊗ ρ to SL n k is the restriction of ρ, along TensorProduct.lid.

Main results

• TauCeti.detPowerRep_def is its defining equation, as the one-dimensional representation of the linear character det ^ m.
• TauCeti.detPowerRep_comp_toGL: every determinant power restricts to the trivial representation of the special linear subgroup, which is why the determinant twist is invisible to SL n k (TauCeti.tprodDetPowerSLEquiv).

References

• Classical groups roadmap

def TauCeti.detPowerRep (k : Type u) (n : ℕ) [CommRing k] (m : ℤ) : Representation k (GL (Fin n) k) k

The one-dimensional representation of GL n k on which g acts by det(g)^m. This is the representation carrying the linear character det ^ m.

Equations

• TauCeti.detPowerRep k n m = Representation.ofLinearCharacter (Matrix.GeneralLinearGroup.det ^ m)

theorem TauCeti.detPowerRep_def (k : Type u) (n : ℕ) [CommRing k] (m : ℤ) : detPowerRep k n m = Representation.ofLinearCharacter (Matrix.GeneralLinearGroup.det ^ m)

The defining equation of TauCeti.detPowerRep: it is the one-dimensional representation of the linear character det ^ m. The body is not exposed, so this is how a downstream module applies the general theory of Representation.ofLinearCharacter and of its twists to it.

@[reducible, inline]

abbrev TauCeti.detRep (k : Type u) (n : ℕ) [CommRing k] : Representation k (GL (Fin n) k) k

The determinant representation of GL n k.

Equations

• TauCeti.detRep k n = TauCeti.detPowerRep k n 1

@[simp]

theorem TauCeti.detPowerRep_apply (k : Type u) (n : ℕ) [CommRing k] (m : ℤ) (g : GL (Fin n) k) (x : k) : ((detPowerRep k n m) g) x = ↑(Matrix.GeneralLinearGroup.det g ^ m) * x

The determinant-power action is scalar multiplication by the indicated determinant power.

@[simp]

theorem TauCeti.detPowerRep_zero (k : Type u) (n : ℕ) [CommRing k] : detPowerRep k n 0 = 1

The zero determinant power is the trivial representation.

theorem TauCeti.detPowerRep_add_apply (k : Type u) (n : ℕ) [CommRing k] (m l : ℤ) (g : GL (Fin n) k) (x : k) : ((detPowerRep k n (m + l)) g) x = ((detPowerRep k n m) g) (((detPowerRep k n l) g) x)

Adding exponents composes the corresponding determinant actions.

@[simp]

theorem TauCeti.detPowerRep_comp_toGL (k : Type u) (n : ℕ) [CommRing k] (m : ℤ) : MonoidHom.comp (detPowerRep k n m) Matrix.SpecialLinearGroup.toGL = Representation.trivial k (Matrix.SpecialLinearGroup (Fin n) k) k

Every determinant-power representation restricts to the trivial representation of SL n k.

The determinant twist on the special linear group

theorem TauCeti.lid_detPowerRep_tprod_toGL_apply (k : Type u) (n : ℕ) [CommRing k] {V : Type v} [AddCommMonoid V] [Module k V] (m : ℤ) (ρ : Representation k (GL (Fin n) k) V) (g : Matrix.SpecialLinearGroup (Fin n) k) (x : TensorProduct k k V) : (TensorProduct.lid k V) ((((detPowerRep k n m).tprod ρ) (Matrix.SpecialLinearGroup.toGL g)) x) = (ρ (Matrix.SpecialLinearGroup.toGL g)) ((TensorProduct.lid k V) x)

TensorProduct.lid carries the restricted action of det^m ⊗ ρ to the restricted action of ρ: the determinant is 1 on SL n k, so the twisting factor is 1. This is the equivariance datum behind TauCeti.tprodDetPowerSLEquiv, recorded on elements so that it can be used without unfolding that equivalence.

noncomputable def TauCeti.tprodDetPowerSLEquiv (k : Type u) (n : ℕ) [CommRing k] {V : Type v} [AddCommMonoid V] [Module k V] (m : ℤ) (ρ : Representation k (GL (Fin n) k) V) : Representation.Equiv (MonoidHom.comp ((detPowerRep k n m).tprod ρ) Matrix.SpecialLinearGroup.toGL) (MonoidHom.comp ρ Matrix.SpecialLinearGroup.toGL)

The determinant twist is invisible to the special linear group: for every representation ρ of GL n k, the restriction of det^m ⊗ ρ to SL n k is the restriction of ρ, along TensorProduct.lid. This is the restricted counterpart of Representation.tprodEquivCharTwist, where the twisting character det ^ m has become 1.

Equations

• TauCeti.tprodDetPowerSLEquiv k n m ρ = Representation.Equiv.mk (TensorProduct.lid k V) ⋯

@[simp]

theorem TauCeti.toLinearMap_tprodDetPowerSLEquiv (k : Type u) (n : ℕ) [CommRing k] {V : Type v} [AddCommMonoid V] [Module k V] (m : ℤ) (ρ : Representation k (GL (Fin n) k) V) : (↑(tprodDetPowerSLEquiv k n m ρ)).toLinearMap = ↑(TensorProduct.lid k V)

@[simp]

theorem TauCeti.tprodDetPowerSLEquiv_tmul (k : Type u) (n : ℕ) [CommRing k] {V : Type v} [AddCommMonoid V] [Module k V] (m : ℤ) (ρ : Representation k (GL (Fin n) k) V) (x : k) (v : V) : (tprodDetPowerSLEquiv k n m ρ) (x ⊗ₜ[k] v) = x • v

@[reducible, inline]

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

The determinant-power representation as a finite-dimensional representation.

Equations

• TauCeti.detPowerFDRep k n m = FDRep.ofLinearCharacter (Matrix.GeneralLinearGroup.det ^ m)

@[reducible, inline]

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

The determinant representation as a finite-dimensional representation.

Equations

• TauCeti.detFDRep k n = FDRep.of (TauCeti.detRep k n)

theorem TauCeti.detPowerRep_neg_apply (k : Type u) (n : ℕ) [Field k] (m : ℤ) (g : GL (Fin n) k) (x : k) : ((detPowerRep k n (-m)) g) x = (↑(Matrix.GeneralLinearGroup.det g ^ m))⁻¹ * x

Negating the exponent makes the determinant scalar the inverse of the original power.

@[simp]

theorem TauCeti.char_detPowerRep (k : Type u) (n : ℕ) [Field k] (m : ℤ) (g : GL (Fin n) k) : (detPowerRep k n m).character g = ↑(Matrix.GeneralLinearGroup.det g ^ m)

The character of the determinant-power representation is the corresponding determinant power.

theorem TauCeti.char_detPowerFDRep (k : Type u) (n : ℕ) [Field k] (m : ℤ) (g : GL (Fin n) k) : (detPowerFDRep k n m).character g = ↑(Matrix.GeneralLinearGroup.det g ^ m)

The bundled determinant-power character is the corresponding determinant power.

This is deliberately not a simp lemma: TauCeti.detPowerFDRep is a reducible abbreviation for FDRep.ofLinearCharacter (det ^ m), so FDRep.char_ofLinearCharacter already reduces its left-hand side.

theorem TauCeti.char_detFDRep (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (detFDRep k n).character g = ↑(Matrix.GeneralLinearGroup.det g)

The bundled determinant character is the determinant.