Weyl's unitarian trick for the rational representations of GL n ℂ

A rational representation ρ of GL n ℂ restricts, along the inclusion Unitary.toUnits : U(n) →* GL n ℂ of the unitary group, to a representation of the compact group U(n). Weyl's unitarian trick is that nothing is lost in this restriction: a subspace is GL n ℂ-invariant exactly when it is U(n)-invariant, and a linear map between two rational representations intertwines the GL n ℂ-actions exactly when it intertwines the U(n)-actions. Consequently a rational representation is irreducible exactly when its restriction to U(n) is, and, since every finite-dimensional continuous representation of a compact group is completely reducible, every rational representation of GL n ℂ is completely reducible.

The bridge between the two groups is that U(n) is Zariski dense in GL n ℂ (TauCeti.Matrix.GeneralLinearGroup.eq_of_mem_rationalFunctions_of_forall_unitary), together with the fact that every matrix coefficient g ↦ f (ρ g w) of a rational representation is a rational function on GL n ℂ (TauCeti.IsRationalRep.dual_apply_mem_rationalFunctions). If p is U(n)-invariant, w ∈ p, and f is a linear functional vanishing on p, the rational function g ↦ f (ρ g w) vanishes on U(n), hence everywhere, so ρ g w ∈ p for every g.

These are the inputs that let the compact-group theory of U(n) (Haar averaging, Schur orthogonality, the Weyl integration formula) be applied to the rational representations of GL n ℂ. Complete reducibility in particular means that a rational representation is a direct sum of irreducible ones, so that it is described by the multiplicities of its irreducible constituents rather than by a composition series alone.

Main results

• TauCeti.IsRationalRep.apply_mem_of_forall_unitary: a subspace invariant under the unitary group is invariant under GL n ℂ.
• TauCeti.IsRationalRep.subrepresentationOrderIso: the subrepresentations of ρ are those of its restriction to U(n).
• TauCeti.IsRationalRep.isIrreducible_comp_toUnits_iff: ρ is irreducible exactly when its restriction to U(n) is.
• TauCeti.IsRationalRep.isIntertwiningMap_of_comp_toUnits and TauCeti.IsRationalRep.intertwiningMapEquiv: the intertwining maps between two rational representations are those between their restrictions to U(n).
• TauCeti.IsRationalRep.continuous_dual_apply_toUnits: the restriction of a rational representation to U(n) has continuous matrix coefficients.
• TauCeti.IsRationalRep.isSemisimpleRepresentation: every rational representation of GL n ℂ is completely reducible.
• TauCeti.IsRationalRep.nonempty_equiv_of_forall_character_diagGL_eq: rational representations whose characters agree on the diagonal torus are equivalent.

References

• H. Weyl, The Classical Groups, Princeton University Press (1939), Chapter VIII, §11.
• R. Goodman and N. R. Wallach, Symmetry, Representations, and Invariants (2009), Section 2.4.
• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 9.3.

theorem TauCeti.IsRationalRep.apply_mem_of_forall_unitary {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) {p : Submodule ℂ W} (hp : ∀ (u : ↥(Matrix.unitaryGroup (Fin n) ℂ)), ∀ v ∈ p, (ρ (Unitary.toUnits u)) v ∈ p) (g : GL (Fin n) ℂ) {v : W} (hv : v ∈ p) : (ρ g) v ∈ p

A subspace invariant under the unitary group is invariant under GL n ℂ. If ρ is rational and p is preserved by every unitary matrix, then it is preserved by every invertible matrix: for w ∈ p and a linear functional f vanishing on p, the rational function g ↦ f (ρ g w) vanishes on the unitary group, hence everywhere.

def TauCeti.IsRationalRep.subrepresentationOrderIso {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : Subrepresentation (MonoidHom.comp ρ Unitary.toUnits) ≃o Subrepresentation ρ

The subrepresentations of a rational representation are those of its restriction to the unitary group. Restriction along Unitary.toUnits keeps the underlying submodule, and every subspace invariant under the unitary group is already invariant under GL n ℂ (TauCeti.IsRationalRep.apply_mem_of_forall_unitary).

@[simp]

theorem TauCeti.IsRationalRep.subrepresentationOrderIso_apply_toSubmodule {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (S : Subrepresentation (MonoidHom.comp ρ Unitary.toUnits)) : (h.subrepresentationOrderIso S).toSubmodule = S.toSubmodule

The correspondence TauCeti.IsRationalRep.subrepresentationOrderIso keeps the underlying submodule.

@[simp]

theorem TauCeti.IsRationalRep.subrepresentationOrderIso_symm_apply_toSubmodule {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (S : Subrepresentation ρ) : (h.subrepresentationOrderIso.symm S).toSubmodule = S.toSubmodule

The inverse correspondence TauCeti.IsRationalRep.subrepresentationOrderIso keeps the underlying submodule.

theorem TauCeti.IsRationalRep.isIrreducible_comp_toUnits_iff {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : Representation.IsIrreducible (MonoidHom.comp ρ Unitary.toUnits) ↔ ρ.IsIrreducible

A rational representation is irreducible exactly when its restriction to the unitary group is.

theorem TauCeti.IsRationalRep.isIntertwiningMap_of_comp_toUnits {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {W' : Type u_2} [AddCommGroup W'] [Module ℂ W'] {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) {φ : W →ₗ[ℂ] W'} (hφ : Representation.IsIntertwiningMap (MonoidHom.comp ρ Unitary.toUnits) (MonoidHom.comp σ Unitary.toUnits) φ) : ρ.IsIntertwiningMap σ φ

A linear map between rational representations intertwining the unitary group intertwines GL n ℂ. For w and a linear functional f, the two rational functions g ↦ f (φ (ρ g w)) and g ↦ f (σ g (φ w)) agree on the unitary group, hence everywhere.

noncomputable def TauCeti.IsRationalRep.intertwiningMapEquiv {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {W' : Type u_2} [AddCommGroup W'] [Module ℂ W'] {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) : Representation.IntertwiningMap (MonoidHom.comp ρ Unitary.toUnits) (MonoidHom.comp σ Unitary.toUnits) ≃ₗ[ℂ] ρ.IntertwiningMap σ

The intertwining maps between two rational representations are those between their restrictions to the unitary group, as a linear equivalence keeping the underlying linear map (TauCeti.IsRationalRep.isIntertwiningMap_of_comp_toUnits).

@[simp]

theorem TauCeti.IsRationalRep.coe_intertwiningMapEquiv_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {W' : Type u_2} [AddCommGroup W'] [Module ℂ W'] {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (φ : Representation.IntertwiningMap (MonoidHom.comp ρ Unitary.toUnits) (MonoidHom.comp σ Unitary.toUnits)) : ⇑((hρ.intertwiningMapEquiv hσ) φ) = ⇑φ

The equivalence TauCeti.IsRationalRep.intertwiningMapEquiv keeps the underlying function.

@[simp]

theorem TauCeti.IsRationalRep.coe_intertwiningMapEquiv_symm_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {W' : Type u_2} [AddCommGroup W'] [Module ℂ W'] {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (φ : ρ.IntertwiningMap σ) : ⇑((hρ.intertwiningMapEquiv hσ).symm φ) = ⇑φ

The inverse of TauCeti.IsRationalRep.intertwiningMapEquiv keeps the underlying function.

theorem TauCeti.IsRationalRep.continuous_dual_apply_toUnits {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) (f : Module.Dual ℂ W) (w : W) : Continuous fun (u : ↥(Matrix.unitaryGroup (Fin n) ℂ)) => f ((ρ (Unitary.toUnits u)) w)

The restriction of a rational representation to the unitary group has continuous matrix coefficients.

theorem TauCeti.IsRationalRep.isSemisimpleRepresentation {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (h : IsRationalRep ρ) : ρ.IsSemisimpleRepresentation

Every rational representation of GL n ℂ is completely reducible. Its restriction to the compact group U(n) is continuous, hence completely reducible by Haar averaging (Representation.isSemisimpleRepresentation_of_continuous), and it has the same subrepresentations (TauCeti.IsRationalRep.subrepresentationOrderIso).

theorem TauCeti.IsRationalRep.nonempty_equiv_of_forall_character_diagGL_eq {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {W' : Type u_2} [AddCommGroup W'] [Module ℂ W'] {σ : Representation ℂ (GL (Fin n) ℂ) W'} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (h : ∀ (t : Fin n → ℂˣ), ρ.character (diagGL t) = σ.character (diagGL t)) : Nonempty (ρ.Equiv σ)

Rational representations are determined by their characters on the diagonal torus. Two rational representations of GL n ℂ whose characters agree at every invertible diagonal matrix are equivalent.

Every unitary matrix is unitarily conjugate to a diagonal one (TauCeti.exists_isConj_unitaryTorusHom), so the restrictions to U(n) have the same character. They are semisimple, hence equivalent (Representation.nonempty_equiv_of_character_eq_of_isSemisimpleRepresentation), and an equivalence of the restrictions intertwines GL n ℂ (TauCeti.IsRationalRep.intertwiningMapEquiv).