The differential of a rational representation of GL n ℂ

A rational representation ρ of GL n ℂ (TauCeti.IsRationalRep), whose matrix entries are polynomials in the entries of g divided by powers of det g, is the same thing as a representation of the algebraic group GLₙ: a comodule over its coordinate Hopf algebra O(GLₙ). This file constructs that comodule, TauCeti.IsRationalRep.comodule, characterizes it as the unique comodule on which each invertible matrix g acts by ρ g, and differentiates it at the identity. Since the tangent Lie algebra of GLₙ is the matrix Lie algebra (TauCeti.GeneralLinear.tangentLieEquivMatrix), this gives the differential

dρ : 𝔤𝔩ₙ(ℂ) →ₗ⁅ℂ⁆ End W,

TauCeti.IsRationalRep.differential, a representation of the Lie algebra of n × n complex matrices. The construction is algebraic: it differentiates the matrix coefficients of ρ, viewed as elements of O(GLₙ), at the identity, and needs no topology on W. On the standard representation ℂⁿ it is matrix multiplication (TauCeti.IsRationalRep.differential_stdRep).

Because GLₙ is connected and ℂ is algebraically closed of characteristic zero, the differential loses nothing that the subspace and morphism structure of ρ sees: a subspace is ρ-invariant exactly when it is dρ-stable, a vector is ρ-fixed exactly when dρ kills it, and a linear map intertwines two rational representations exactly when it intertwines their differentials. These statements let the representation theory of the Lie algebra 𝔤𝔩ₙ be applied to rational representations of the group, and conversely.

Main definitions

• TauCeti.IsRationalRep.comodule: the O(GLₙ)-comodule of a rational representation.
• TauCeti.IsRationalRep.differential: the differential of a rational representation, a Lie algebra representation of 𝔤𝔩ₙ(ℂ).

Main results

• TauCeti.IsRationalRep.basePointsRepresentation_comodule: each invertible matrix g acts on the comodule by ρ g; TauCeti.IsRationalRep.eq_comodule: no other comodule structure does.
• TauCeti.IsRationalRep.differential_stdRep: the standard representation differentiates to matrix multiplication.
• TauCeti.IsRationalRep.mem_invtSubmodule_iff_forall_mem_invtSubmodule_differential: the invariant subspaces of ρ are the subspaces stable under dρ.
• TauCeti.IsRationalRep.isIrreducible_differential: an irreducible rational representation is irreducible for 𝔤𝔩ₙ.
• TauCeti.IsRationalRep.mem_invariants_iff_forall_differential_apply_eq_zero: the invariants of ρ are the vectors killed by dρ.
• TauCeti.IsRationalRep.isIntertwiningMap_iff_forall_map_differential: the intertwiners of two rational representations are the intertwiners of their differentials.
• TauCeti.IsRationalRep.map_lift_differential_apply: they also intertwine the actions of the universal enveloping algebra U(𝔤𝔩ₙ).
• TauCeti.IsRationalRep.lieModuleEquivOfEquiv: an equivalence of rational representations is an isomorphism of the differentiated 𝔤𝔩ₙ-modules.
• TauCeti.IsRationalRep.differential_tprod: the differential of a tensor product of rational representations is the tensor product of their differentials, dρ X ⊗ 1 + 1 ⊗ dσ X.
• TauCeti.IsRationalRep.tprodLieModuleEquiv: isomorphisms of 𝔤𝔩ₙ-modules out of two differentiated rational representations tensor to one out of their differentiated tensor product.
• TauCeti.IsRationalRep.differential_directSum and TauCeti.IsRationalRep.directSumLieModuleEquiv: the same for finite direct sums.

References

• J. C. Jantzen, Representations of Algebraic Groups, Part I, Chapters 2 and 7.
• J. S. Milne, Algebraic Groups (2017), Chapters 4 and 10.
• J. E. Humphreys, Linear Algebraic Groups, §13.

@[instance_reducible]

noncomputable def TauCeti.IsRationalRep.comodule {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) : Comodule ℂ (↑(GeneralLinear.coordinateHopfAlgebra ℂ n)) W

The comodule of a rational representation. A rational representation ρ of GL n ℂ is a right comodule over the coordinate Hopf algebra O(GLₙ): for a basis b of W, a vector w coacts by ∑ᵢ bᵢ ⊗ cᵢ(w), where cᵢ(w) ∈ O(GLₙ) is the coordinate function g ↦ bᵢ*(ρ g w). This is the representation of the algebraic group GLₙ on which each invertible matrix g acts by ρ g (TauCeti.IsRationalRep.basePointsRepresentation_comodule), and it does not depend on the basis (TauCeti.IsRationalRep.eq_comodule).

@[simp]

theorem TauCeti.IsRationalRep.basePointsRepresentation_comodule {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (g : GL (Fin n) ℂ) : (Comodule.basePointsRepresentation W) (GeneralLinear.generalLinearToPoint n g) = ρ g

The comodule of a rational representation integrates it: the complex point of GLₙ attached to g acts on TauCeti.IsRationalRep.comodule by ρ g.

theorem TauCeti.IsRationalRep.basePointsRepresentation_comodule_eq_pointsMulEquiv {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (p : WithConv (↑(GeneralLinear.coordinateHopfAlgebra ℂ n) →ₐ[ℂ] ℂ)) : (Comodule.basePointsRepresentation W) p = ρ ((GeneralLinear.pointsMulEquiv n) p)

Every complex point p of GLₙ acts on TauCeti.IsRationalRep.comodule by ρ of the invertible matrix p names.

theorem TauCeti.IsRationalRep.eq_comodule {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (c : Comodule ℂ (↑(GeneralLinear.coordinateHopfAlgebra ℂ n)) W) (hc : ∀ (g : GL (Fin n) ℂ), (Comodule.basePointsRepresentation W) (GeneralLinear.generalLinearToPoint n g) = ρ g) : c = hρ.comodule

TauCeti.IsRationalRep.comodule is the only comodule integrating ρ: every comodule structure on W on which each complex point g of GLₙ acts by ρ g is TauCeti.IsRationalRep.comodule.

noncomputable def TauCeti.IsRationalRep.differential {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) : Matrix (Fin n) (Fin n) ℂ →ₗ⁅ℂ⁆ Module.End ℂ W

The differential of a rational representation: the representation dρ of the matrix Lie algebra 𝔤𝔩ₙ(ℂ) on W obtained by differentiating TauCeti.IsRationalRep.comodule at the identity, through the identification TauCeti.GeneralLinear.tangentLieEquivMatrix of the tangent Lie algebra of GLₙ with n × n matrices. In a basis, the matrix entries of dρ X are the derivatives along X at the identity of the matrix coefficients of ρ.

theorem TauCeti.IsRationalRep.differential_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (X : Matrix (Fin n) (Fin n) ℂ) : hρ.differential X = Comodule.differential ((GeneralLinear.tangentLieEquivMatrix n).symm X)

A matrix acts through the differential as the tangent vector it names acts on the comodule of the representation.

@[simp]

theorem TauCeti.IsRationalRep.differential_stdRep {n : ℕ} (h : IsRationalRep (stdRep ℂ n)) (X : Matrix (Fin n) (Fin n) ℂ) : h.differential X = X.mulVecLin

The standard representation differentiates to matrix multiplication: a matrix X acts on ℂⁿ through the differential of TauCeti.stdRep by v ↦ X *ᵥ v.

theorem TauCeti.IsRationalRep.mem_invtSubmodule_iff_forall_mem_invtSubmodule_differential {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (U : Submodule ℂ W) : U ∈ ρ.invtSubmodule ↔ ∀ (X : Matrix (Fin n) (Fin n) ℂ), U ∈ (hρ.differential X).invtSubmodule

The invariant subspaces of a rational representation are the 𝔤𝔩ₙ-stable subspaces: a subspace is preserved by every ρ g exactly when it is preserved by every dρ X.

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

An irreducible rational representation is irreducible for 𝔤𝔩ₙ: through its differential, an irreducible rational representation is an irreducible module over the matrix Lie algebra 𝔤𝔩ₙ(ℂ).

theorem TauCeti.IsRationalRep.mem_invariants_iff_forall_differential_apply_eq_zero {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} (hρ : IsRationalRep ρ) (w : W) : w ∈ ρ.invariants ↔ ∀ (X : Matrix (Fin n) (Fin n) ℂ), (hρ.differential X) w = 0

The invariants of a rational representation are the vectors killed by 𝔤𝔩ₙ: a vector is fixed by every ρ g exactly when every dρ X sends it to zero.

theorem TauCeti.IsRationalRep.isIntertwiningMap_iff_forall_map_differential {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (f : W →ₗ[ℂ] V) : ρ.IsIntertwiningMap σ f ↔ ∀ (X : Matrix (Fin n) (Fin n) ℂ) (w : W), f ((hρ.differential X) w) = (hσ.differential X) (f w)

Intertwiners of rational representations are the 𝔤𝔩ₙ-intertwiners. A linear map between rational representations of GL n ℂ commutes with the group actions exactly when it commutes with their differentials.

theorem TauCeti.IsRationalRep.map_lift_differential_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) {f : W →ₗ[ℂ] V} (hf : ρ.IsIntertwiningMap σ f) (u : UniversalEnvelopingAlgebra ℂ (Matrix (Fin n) (Fin n) ℂ)) (w : W) : f ((((UniversalEnvelopingAlgebra.lift ℂ) hρ.differential) u) w) = (((UniversalEnvelopingAlgebra.lift ℂ) hσ.differential) u) (f w)

Intertwiners of rational representations intertwine the enveloping-algebra actions of their differentials: a linear map commuting with the actions of GL n ℂ commutes with the action of every element of U(𝔤𝔩ₙ).

noncomputable def TauCeti.IsRationalRep.lieModuleEquivOfEquiv {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (φ : ρ.Equiv σ) : W ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ V

Equivalent rational representations have isomorphic differentials: an equivalence of rational representations of GL n ℂ is an isomorphism between the 𝔤𝔩ₙ-modules given by their differentials.

@[simp]

theorem TauCeti.IsRationalRep.lieModuleEquivOfEquiv_apply {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (φ : ρ.Equiv σ) (w : W) : (hρ.lieModuleEquivOfEquiv hσ φ) w = φ w

TauCeti.IsRationalRep.lieModuleEquivOfEquiv is the given equivalence.

theorem TauCeti.IsRationalRep.comodule_tprod {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) : ⋯.comodule = Comodule.tensor ℂ (↑(GeneralLinear.coordinateHopfAlgebra ℂ n)) W V

The comodule of a tensor product of rational representations is the diagonal tensor product (TauCeti.Comodule.tensor) of their comodules.

theorem TauCeti.IsRationalRep.differential_tprod_tmul {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (X : Matrix (Fin n) (Fin n) ℂ) (w : W) (v : V) : (⋯.differential X) (w ⊗ₜ[ℂ] v) = (hρ.differential X) w ⊗ₜ[ℂ] v + w ⊗ₜ[ℂ] (hσ.differential X) v

The differential of a tensor product of rational representations acts by the Leibniz rule: d(ρ ⊗ σ) X (w ⊗ v) = dρ X w ⊗ v + w ⊗ dσ X v.

theorem TauCeti.IsRationalRep.differential_tprod {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (X : Matrix (Fin n) (Fin n) ℂ) : ⋯.differential X = LinearMap.rTensor V (hρ.differential X) + LinearMap.lTensor W (hσ.differential X)

The differential of a tensor product of rational representations is the tensor product of their differentials, d(ρ ⊗ σ) X = dρ X ⊗ 1 + 1 ⊗ dσ X: differentiating carries the tensor product of representations of GL n ℂ to the tensor product of representations of 𝔤𝔩ₙ(ℂ).

noncomputable def TauCeti.IsRationalRep.tprodLieModuleEquiv {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module ℂ M] [LieRingModule (Matrix (Fin n) (Fin n) ℂ) M] [LieModule ℂ (Matrix (Fin n) (Fin n) ℂ) M] [AddCommGroup N] [Module ℂ N] [LieRingModule (Matrix (Fin n) (Fin n) ℂ) N] [LieModule ℂ (Matrix (Fin n) (Fin n) ℂ) N] (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (e₁ : W ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ M) (e₂ : V ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ N) : TensorProduct ℂ W V ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ TensorProduct ℂ M N

Differentiation preserves tensor products of 𝔤𝔩ₙ-modules: isomorphisms of 𝔤𝔩ₙ-modules e₁ : W ≅ M and e₂ : V ≅ N, the sources carrying the differentials of rational representations ρ and σ, tensor to an isomorphism W ⊗ V ≅ M ⊗ N whose source carries the differential of ρ ⊗ σ and whose target carries the tensor product 𝔤𝔩ₙ-module structure.

@[simp]

theorem TauCeti.IsRationalRep.tprodLieModuleEquiv_tmul {n : ℕ} {W : Type u_1} [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ (GL (Fin n) ℂ) W} {V : Type u_2} [AddCommGroup V] [Module ℂ V] {σ : Representation ℂ (GL (Fin n) ℂ) V} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [Module ℂ M] [LieRingModule (Matrix (Fin n) (Fin n) ℂ) M] [LieModule ℂ (Matrix (Fin n) (Fin n) ℂ) M] [AddCommGroup N] [Module ℂ N] [LieRingModule (Matrix (Fin n) (Fin n) ℂ) N] [LieModule ℂ (Matrix (Fin n) (Fin n) ℂ) N] (hρ : IsRationalRep ρ) (hσ : IsRationalRep σ) (e₁ : W ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ M) (e₂ : V ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ N) (w : W) (v : V) : (hρ.tprodLieModuleEquiv hσ e₁ e₂) (w ⊗ₜ[ℂ] v) = e₁ w ⊗ₜ[ℂ] e₂ v

TauCeti.IsRationalRep.tprodLieModuleEquiv acts on pure tensors factorwise.

theorem TauCeti.IsRationalRep.differential_directSum {n : ℕ} {ι : Type u_2} [Finite ι] {V : ι → Type u_3} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℂ (V i)] {σ : (i : ι) → Representation ℂ (GL (Fin n) ℂ) (V i)} (h : ∀ (i : ι), IsRationalRep (σ i)) (X : Matrix (Fin n) (Fin n) ℂ) : ⋯.differential X = DirectSum.lmap fun (i : ι) => ⋯.differential X

The differential of a finite direct sum of rational representations is the direct sum of their differentials: differentiating carries direct sums of representations of GL n ℂ to direct sums of representations of 𝔤𝔩ₙ(ℂ).

noncomputable def TauCeti.IsRationalRep.directSumLieModuleEquiv {n : ℕ} {ι : Type u_2} [Finite ι] {V : ι → Type u_3} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℂ (V i)] {σ : (i : ι) → Representation ℂ (GL (Fin n) ℂ) (V i)} {M : ι → Type u_4} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module ℂ (M i)] [(i : ι) → LieRingModule (Matrix (Fin n) (Fin n) ℂ) (M i)] (h : ∀ (i : ι), IsRationalRep (σ i)) (e : (i : ι) → V i ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ M i) : (DirectSum ι fun (i : ι) => V i) ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ DirectSum ι fun (i : ι) => M i

Differentiation preserves finite direct sums of 𝔤𝔩ₙ-modules: isomorphisms of 𝔤𝔩ₙ-modules e i : V i ≅ M i, each source carrying the differential of a rational representation σ i, sum to an isomorphism ⨁ i, V i ≅ ⨁ i, M i whose source carries the differential of the direct sum of the σ i and whose target carries the direct sum 𝔤𝔩ₙ-module structure.

@[simp]

theorem TauCeti.IsRationalRep.directSumLieModuleEquiv_apply {n : ℕ} {ι : Type u_2} [Finite ι] {V : ι → Type u_3} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module ℂ (V i)] {σ : (i : ι) → Representation ℂ (GL (Fin n) ℂ) (V i)} {M : ι → Type u_4} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module ℂ (M i)] [(i : ι) → LieRingModule (Matrix (Fin n) (Fin n) ℂ) (M i)] (h : ∀ (i : ι), IsRationalRep (σ i)) (e : (i : ι) → V i ≃ₗ⁅ℂ,Matrix (Fin n) (Fin n) ℂ⁆ M i) (t : DirectSum ι fun (i : ι) => V i) (i : ι) : ((directSumLieModuleEquiv h e) t) i = (e i) (t i)

TauCeti.IsRationalRep.directSumLieModuleEquiv acts componentwise.