Documentation

TauCeti.RepresentationTheory.ClassicalGroups.Rational

Rational and polynomial representations of the general linear group #

A representation of GL n ℂ is polynomial when, in some basis of the carrier, every matrix entry of ρ g is a polynomial in the entries gᵢⱼ, and rational when every entry is such a polynomial divided by a power of det g. The distinction is the one that separates the representations arising inside tensor powers of the standard representation from those needing a determinant twist: TauCeti.stdRep and its tensor, symmetric and exterior powers are polynomial, as is det ^ m for m ≥ 0, whereas det ^ (-1) is rational.

The two definitions quantify existentially over a basis, and the content of this file is that this costs nothing: the condition holds in one basis exactly when it holds in every basis (TauCeti.isRationalRep_iff_forall_mem_rationalFunctions and its polynomial companion), because a change of basis rewrites each entry as a fixed linear combination of the old entries, with coefficients independent of g. So the existential form is a genuinely basis-independent property of ρ, and the coordinate-entry form is available against whatever basis a computation has in hand.

The bookkeeping is carried by two algebras of functions on the group rather than by the representations. TauCeti.Matrix.GeneralLinearGroup.polynomialFunctions k n collects the f : GL (Fin n) k → k that evaluate some polynomial in the matrix entries, and TauCeti.Matrix.GeneralLinearGroup.rationalFunctions k n those f for which some determinant power det ^ m makes det ^ m * f polynomial. Both are k-subalgebras of the functions on the group, and closure under sums, products and scalars is what reduces every argument below to a single entry computation: the change-of-basis formula is a sum of scalar multiples, the entries of a tensor product are products of entries, and a determinant power is one generator. Those entry computations are themselves subalgebra-generic, and live in TauCeti.RepresentationTheory.MatrixCoefficients.

The two function algebras carry an arbitrary base ring, but the two representation-level notions are stated over ℂ. The restriction is not cosmetic: over a finite field k the group GL n k is a finite set and every function on it is the evaluation of a polynomial in the matrix entries, so TauCeti.Matrix.GeneralLinearGroup.polynomialFunctions k n is then the whole function algebra and every finite-dimensional representation would count as polynomial. The coordinate-entry condition is faithful to the intended notion only over an infinite field; here the base field is ℂ.

That the negative determinant powers are rational is TauCeti.Matrix.GeneralLinearGroup.det_zpow_mem_rationalFunctions. Whether a given representation fails to be polynomial is a separate question, not addressed here; so is complete reducibility of rational representations, which requires the theory of reductive groups.

Main definitions #

Main results #

Rationality and polynomiality of a representation #

source
def TauCeti.IsPolynomialRep {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] (ρ : Representation ℂ (GL (Fin n) ℂ) W) :
Prop

A polynomial representation of GL n ℂ: in some basis of the carrier, every matrix entry of ρ g is a polynomial in the entries of g. The carrier is forced to be finite-dimensional, since no basis indexed by Fin (Module.finrank ℂ W) exists otherwise (TauCeti.IsPolynomialRep.finite). The condition does not depend on the basis: see TauCeti.isPolynomialRep_iff_forall_mem_polynomialFunctions.

The base field is ℂ rather than a general field because the coordinate-entry condition is faithful only over an infinite field: over a finite k the group GL n k is finite, so every function on it — hence every matrix entry of every representation — is polynomial in the entries of g.

Instances For
    source
    theorem TauCeti.isPolynomialRep_iff {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] (ρ : Representation ℂ (GL (Fin n) ℂ) W) :
    IsPolynomialRep ρ ↔ ∃ (b : Module.Basis (Fin (Module.finrank ℂ W)) ℂ W) (P : Fin (Module.finrank ℂ W) → Fin (Module.finrank ℂ W) → MvPolynomial (Fin n × Fin n) ℂ), ∀ (g : GL (Fin n) ℂ) (i j : Fin (Module.finrank ℂ W)), (LinearMap.toMatrix b b) (ρ g) i j = (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) (P i j)

    The coordinate-entry form of TauCeti.IsPolynomialRep, as a lemma.

    source
    def TauCeti.IsRationalRep {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] (ρ : Representation ℂ (GL (Fin n) ℂ) W) :
    Prop

    A rational representation of GL n ℂ: in some basis of the carrier, every matrix entry of ρ g is a polynomial in the entries of g divided by a fixed power of det g. The carrier is forced to be finite-dimensional (TauCeti.IsRationalRep.finite), and the condition does not depend on the basis: see TauCeti.isRationalRep_iff_forall_mem_rationalFunctions. The base field is ℂ for the reason recorded on TauCeti.IsPolynomialRep.

    Instances For
      source
      theorem TauCeti.isRationalRep_iff {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] (ρ : Representation ℂ (GL (Fin n) ℂ) W) :
      IsRationalRep ρ ↔ ∃ (b : Module.Basis (Fin (Module.finrank ℂ W)) ℂ W) (P : Fin (Module.finrank ℂ W) → Fin (Module.finrank ℂ W) → MvPolynomial (Fin n × Fin n) ℂ) (m : ℕ), ∀ (g : GL (Fin n) ℂ) (i j : Fin (Module.finrank ℂ W)), (LinearMap.toMatrix b b) (ρ g) i j = ((↑g).det ^ m)⁻¹ * (MvPolynomial.eval fun (p : Fin n × Fin n) => ↑g p.1 p.2) (P i j)

      The coordinate-entry form of TauCeti.IsRationalRep, as a lemma.

      source
      theorem TauCeti.IsPolynomialRep.finite {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsPolynomialRep ρ) :
      Module.Finite ℂ W

      The carrier of a polynomial representation is finite-dimensional.

      source
      theorem TauCeti.IsRationalRep.finite {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) :
      Module.Finite ℂ W

      The carrier of a rational representation is finite-dimensional.

      source
      theorem TauCeti.isPolynomialRep_iff_forall_mem_polynomialFunctions {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℂ W) :
      IsPolynomialRep ρ ↔ ∀ (i j : ι), (fun (g : GL (Fin n) ℂ) => (LinearMap.toMatrix b b) (ρ g) i j) ∈ Matrix.GeneralLinearGroup.polynomialFunctions ℂ n

      Polynomiality is basis independent. A representation is polynomial exactly when, against any chosen basis, each matrix entry is a polynomial function of the entries of g.

      source
      theorem TauCeti.isRationalRep_iff_forall_mem_rationalFunctions {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {ι : Type w} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℂ W) :
      IsRationalRep ρ ↔ ∀ (i j : ι), (fun (g : GL (Fin n) ℂ) => (LinearMap.toMatrix b b) (ρ g) i j) ∈ Matrix.GeneralLinearGroup.rationalFunctions ℂ n

      Rationality is basis independent. A representation is rational exactly when, against any chosen basis, each matrix entry is a rational function of the entries of g.

      source
      theorem TauCeti.IsPolynomialRep.isRationalRep {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsPolynomialRep ρ) :
      IsRationalRep ρ

      A polynomial representation is rational.

      source
      theorem TauCeti.IsPolynomialRep.of_surjective {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type y} [AddCommMonoid V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (h : IsPolynomialRep ρ) (f : ρ.IntertwiningMap σ) (hf : Function.Surjective ⇑f) :
      IsPolynomialRep σ

      A quotient of a polynomial representation is polynomial. This is the form in which the functorial powers below inherit polynomiality from the tensor power.

      source
      theorem TauCeti.IsRationalRep.of_surjective {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type y} [AddCommMonoid V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (h : IsRationalRep ρ) (f : ρ.IntertwiningMap σ) (hf : Function.Surjective ⇑f) :
      IsRationalRep σ

      A quotient of a rational representation is rational.

      Matrix coefficients of a rational representation #

      source
      theorem TauCeti.IsRationalRep.dual_apply_mem_rationalFunctions {n : ℕ} {W : Type v} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (f : Module.Dual ℂ W) (w : W) :
      (fun (g : GL (Fin n) ℂ) => f ((ρ g) w)) ∈ Matrix.GeneralLinearGroup.rationalFunctions ℂ n

      The matrix coefficients of a rational representation are rational functions. For a linear functional f and a vector w, the function g ↦ f (ρ g w) is a polynomial in the entries of g divided by a power of det g.

      source
      theorem TauCeti.isRationalRep_iff_forall_dual_apply_mem_rationalFunctions {n : ℕ} {W : Type v} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} [Module.Finite ℂ W] :
      IsRationalRep ρ ↔ ∀ (f : Module.Dual ℂ W) (w : W), (fun (g : GL (Fin n) ℂ) => f ((ρ g) w)) ∈ Matrix.GeneralLinearGroup.rationalFunctions ℂ n

      Rationality from matrix coefficients. A finite-dimensional representation is rational exactly when all its matrix coefficients g ↦ f (ρ g w) are rational functions.

      source
      theorem TauCeti.IsRationalRep.directSum {n : ℕ} {ι : Type u_1} [Finite ι] {V : ι → Type u_2} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℂ (V i)] {σ : (i : ι) → Representation ℂ (GL (Fin n) ℂ) (V i)} (h : ∀ (i : ι), IsRationalRep (σ i)) :
      IsRationalRep (Representation.directSum σ)

      A finite direct sum of rational representations is rational. A matrix coefficient of the direct sum is a sum of matrix coefficients of the summands.

      The basic examples #

      source
      @[simp]
      theorem TauCeti.isPolynomialRep_stdRep (n : ℕ) :
      IsPolynomialRep (stdRep ℂ n)

      The standard representation is polynomial: in the standard basis its matrix is g itself.

      source
      @[simp]
      theorem TauCeti.isRationalRep_detPowerRep {n : ℕ} (m : ℤ) :
      IsRationalRep (detPowerRep ℂ n m)

      The determinant powers are rational representations.

      source
      @[simp]
      theorem TauCeti.isPolynomialRep_detPowerRep_of_nonneg {n : ℕ} {m : ℤ} (hm : 0 ≤ m) :
      IsPolynomialRep (detPowerRep ℂ n m)

      The nonnegative determinant powers are polynomial representations.

      source
      theorem TauCeti.IsPolynomialRep.tprod {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {W' : Type x} [AddCommMonoid W'] [Module ℂ W'] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsPolynomialRep ρ) (hσ : IsPolynomialRep σ) :
      IsPolynomialRep (ρ.tprod σ)

      A tensor product of polynomial representations is polynomial.

      source
      theorem TauCeti.IsRationalRep.tprod {n : ℕ} {W : Type v} [AddCommMonoid W] [Module ℂ W] {W' : Type x} [AddCommMonoid W'] [Module ℂ W'] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) :
      IsRationalRep (ρ.tprod σ)

      A tensor product of rational representations is rational.

      The functorial powers #

      source
      theorem TauCeti.IsPolynomialRep.tensorPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsPolynomialRep ρ) (d : ℕ) :
      IsPolynomialRep (ρ.tensorPower d)

      A tensor power of a polynomial representation is polynomial.

      source
      theorem TauCeti.IsRationalRep.tensorPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (d : ℕ) :
      IsRationalRep (ρ.tensorPower d)

      A tensor power of a rational representation is rational.

      source
      theorem TauCeti.IsPolynomialRep.symmetricPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsPolynomialRep ρ) (d : ℕ) :
      IsPolynomialRep (ρ.symmetricPower d)

      A symmetric power of a polynomial representation is polynomial.

      source
      theorem TauCeti.IsRationalRep.symmetricPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (d : ℕ) :
      IsRationalRep (ρ.symmetricPower d)

      A symmetric power of a rational representation is rational.

      source
      theorem TauCeti.IsPolynomialRep.exteriorPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsPolynomialRep ρ) (d : ℕ) :
      IsPolynomialRep (ρ.exteriorPower d)

      An exterior power of a polynomial representation is polynomial.

      source
      theorem TauCeti.IsRationalRep.exteriorPower {n : ℕ} {W : Type} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (d : ℕ) :
      IsRationalRep (ρ.exteriorPower d)

      An exterior power of a rational representation is rational.

      source
      @[simp]
      theorem TauCeti.isPolynomialRep_tensorPowerRep (n d : ℕ) :
      IsPolynomialRep (tensorPowerRep ℂ n d)

      The tensor powers of the standard representation are polynomial.

      source
      @[simp]
      theorem TauCeti.isPolynomialRep_symPowerRep (n d : ℕ) :
      IsPolynomialRep (symPowerRep ℂ n d)

      The symmetric powers of the standard representation are polynomial.

      source
      @[simp]
      theorem TauCeti.isPolynomialRep_extPowerRep (n d : ℕ) :
      IsPolynomialRep (extPowerRep ℂ n d)

      The exterior powers of the standard representation are polynomial.