Differentials of represented weight-torus cocharacters

Suppose a weight representation factors through a commutative bialgebra H. A cocharacter of its weight torus differentiates to the diagonal matrix of character–cocharacter pairings, multiplied by its tangent parameter. The formula holds over every coefficient algebra and requires no smoothness or projectivity assumption.

This gives the matrix calculation for identifying simple-coroot differentials with Cartan vectors in a group defined by generators inside a general linear group.

The weight cocharacter t ↦ diag(t ^ w a) of GL_N itself, weightCocharacter w, is the special case read directly off the generic matrix entries: it differentiates to the diagonal matrix of its weights. For w = Pi.single i 1 this is the matrix unit Eᵢᵢ, which is how a weight vector of a rational representation is seen to be an eigenvector of Eᵢᵢ.

Main declarations

• tangentMatrix_derivationComp_cocharacter_of_weightTorus: the matrix of a represented weight-torus cocharacter differential over any coefficient algebra.
• weightCocharacter_apply_X: the coordinate morphism of the weight cocharacter t ↦ diag(t ^ w a) of GL_N on the generic matrix entries.
• tangentMatrix_derivationComp_weightCocharacter: its differential, the diagonal matrix of the weights w a times the tangent parameter.

@[simp]

theorem TauCeti.GeneralLinear.weightCocharacter_apply_X {R : Type u} [CommRing R] {N : ℕ} (w : Fin N → ℤ) (a b : Fin N) : (weightCocharacter w) ((coordinateHopfAlgebraAlgEquiv R N) ((coordinateRingMap R N) (MvPolynomial.X (a, b)))) = if a = b then LaurentPolynomial.T (w a) else 0

The weight cocharacter on the generic matrix entries: its coordinate morphism sends the generic diagonal entry xₐₐ to the Laurent monomial T ^ w a and every off-diagonal entry to zero. This is the coordinate form of t ↦ diag(t ^ w a), read off at the universal point.

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_derivationComp_weightCocharacter {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {N : ℕ} (w : Fin N → ℤ) (d : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)) : (tangentMatrix N) ((derivationComp (weightCocharacter w)) d) = Matrix.diagonal fun (a : Fin N) => w a • MultiplicativeGroup.tangentLinearEquiv d

The differential of the weight cocharacter t ↦ diag(t ^ w a) is the diagonal matrix of its weights, multiplied by the tangent parameter.

theorem TauCeti.GeneralLinear.tangentMatrix_derivationComp_cocharacter_of_weightTorus {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {sigma : Type w} [Finite sigma] {H : Type x} [CommRing H] [Bialgebra R H] {N : ℕ} (q : ↑(coordinateHopfAlgebra R N) →ₐc[R] H) (π : H →ₐc[R] MonoidAlgebra R (Multiplicative (sigma →₀ ℤ))) (wt : Fin N → sigma → ℤ) (hπ : π.comp q = weightTorusCoordinateBialgHom wt) (ψ : Multiplicative (sigma →₀ ℤ) →* Multiplicative ℤ) (d : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)) : (tangentMatrix N) ((derivationComp q) ((derivationComp (π.cocharacter ψ)) d)) = Matrix.diagonal fun (a : Fin N) => Multiplicative.toAdd (ψ (Multiplicative.ofAdd (Finsupp.equivFunOnFinite.symm (wt a)))) • MultiplicativeGroup.tangentLinearEquiv d

The differential of a weight-torus cocharacter is diagonal, with entries the integer character–cocharacter pairings times its tangent parameter. The weight representation may factor through any commutative bialgebra, and coefficients may lie in any commutative algebra.