Differential of a matrix root subgroup

The differential of the root subgroup xᵢⱼ : 𝔾ₐ → GLₙ at the additive identity sends the tangent vector c to c Eᵢⱼ. In particular, it sends the unit tangent vector to the matrix unit which spans the corresponding adjoint root space. The statement works over an arbitrary commutative base ring and after extension to any commutative coefficient algebra. It identifies the differential of the represented group-scheme morphism, rather than only the derivative of an informal matrix formula.

The calculation supplies the root vector attached to the standard pinning of GLₙ.

Reference

J. S. Milne, Algebraic Groups (2017), §21.

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_derivationComp_rootSubgroup {R : Type u} [CommRing R] {B : Type v} [CommRing B] [Algebra R B] {n : ℕ} {i j : Fin n} (hij : i ≠ j) (d : Derivation R (↑(AdditiveGroup.coordinateHopfAlgebra R)) (Bialgebra.CounitAlgebra R (↑(AdditiveGroup.coordinateHopfAlgebra R)) B)) : (tangentMatrix n) ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) d) = Matrix.single i j (AdditiveGroup.gaTangentLinearEquiv d)

The differential of the matrix root subgroup sends an additive tangent vector c to c Eᵢⱼ. This holds over every commutative base ring and coefficient algebra.

@[simp]

theorem TauCeti.GeneralLinear.cotangentDual_rootSubgroup_unit {k : Type u} [Field k] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Derivation.cotangentLinearEquiv.symm ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) (AdditiveGroup.gaTangentLinearEquiv.symm 1)) = matrixUnitTangent i j

The unit tangent vector of 𝔾ₐ maps to the matrix unit Eᵢⱼ in the fixed cotangent-dual model of the Lie algebra of GLₙ.

theorem TauCeti.GeneralLinear.cotangentDual_rootSubgroup_unit_mem_adjointWeightSpace {k : Type u} [Field k] {n : ℕ} {i j : Fin n} (hij : i ≠ j) : Derivation.cotangentLinearEquiv.symm ((derivationComp (CommHopfAlgCat.Hom.hom (rootSubgroupCoordinateMap hij))) (AdditiveGroup.gaTangentLinearEquiv.symm 1)) ∈ Derivation.adjointWeightSpace (CommHopfAlgCat.Hom.hom diagonalTorusCoordinateMap) (matrixUnitWeight i j)

The derivative of a root subgroup at the identity lies in the adjoint weight space of weight eᵢ - eⱼ for the diagonal torus.