The tangent Lie algebra of the general linear group

The tangent space at the identity of GLₙ is the full matrix algebra. A tangent vector is a counit-valued derivation of the coordinate Hopf algebra O(GLₙ); its matrix is obtained by evaluating the derivation on the generic coordinate entries. We prove that this is a linear equivalence and that it identifies the convolution Lie bracket with the matrix commutator.

The proof uses the functor-of-points description of GLₙ. Over the dual numbers, the matrices reducing to the identity are exactly 1 + εX, with inverse 1 - εX. The existing equivalences between derivations, tangent-kernel points, and invertible matrices therefore give both injectivity and surjectivity without choosing a presentation of derivations on the determinant localization.

Main declarations

• TauCeti.GeneralLinear.tangentMatrix: evaluate a tangent derivation on the generic entries.
• TauCeti.GeneralLinear.trace_tangentMatrix: the derivative of the determinant is matrix trace.
• TauCeti.GeneralLinear.tangentLinearEquivMatrix: the tangent space of GLₙ is linearly equivalent to n × n matrices.
• TauCeti.GeneralLinear.cotangentDualMatrixEquiv: the cotangent-dual Lie algebra of GLₙ identified with matrices.
• TauCeti.GeneralLinear.tangentLieEquivMatrix: the same equivalence as an equivalence of Lie algebras, carrying the tangent bracket to the matrix commutator.

References

• J. S. Milne, Algebraic Groups (2017), §§10, 14.
• The first-order determinant computation uses Mathlib's Matrix.det_one_add_smul.

noncomputable def TauCeti.GeneralLinear.tangentMatrix {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) →ₗ[B] Matrix (Fin n) (Fin n) B

The matrix of a tangent vector to GLₙ, obtained by evaluating the derivation on the generic coordinate entries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_apply {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) (i j : Fin n) : (tangentMatrix n) d i j = (Bialgebra.CounitAlgebra.algEquivSelf R (↑(coordinateHopfAlgebra R n)) B) (d ((coordinateHopfAlgebraAlgEquiv R n) ((coordinateRingMap R n) (MvPolynomial.X (i, j)))))

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_mapValue {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) {C : Type u_1} [CommRing C] [Algebra R C] (φ : B →ₐ[R] C) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentMatrix n) ((Derivation.mapValue φ) d) = ((tangentMatrix n) d).map ⇑φ

Extending coefficients of a general-linear tangent vector maps its matrix entrywise.

@[simp]

theorem TauCeti.GeneralLinear.trace_tangentMatrix {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : ((tangentMatrix n) d).trace = d ↑(determinantGroupLike R n)

The differential of the determinant on GLₙ is matrix trace. Evaluating a tangent derivation on the generic determinant, then identifying its counit-valued coefficient with B, equals the trace of its tangent matrix.

noncomputable def TauCeti.GeneralLinear.tangentLinearEquivMatrix {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) ≃ₗ[B] Matrix (Fin n) (Fin n) B

The tangent space at the identity of GLₙ is the full matrix algebra. The equivalence sends a counit-valued derivation to its values on the generic matrix entries.

Equations

• TauCeti.GeneralLinear.tangentLinearEquivMatrix n = LinearEquiv.ofBijective (TauCeti.GeneralLinear.tangentMatrix n) ⋯

@[simp]

theorem TauCeti.GeneralLinear.tangentLinearEquivMatrix_apply {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentLinearEquivMatrix n) d = (tangentMatrix n) d

@[simp]

theorem TauCeti.GeneralLinear.tangentMatrix_lie {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d e : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentMatrix n) ⁅d, e⁆ = ⁅(tangentMatrix n) d, (tangentMatrix n) e⁆

The tangent-matrix equivalence identifies the convolution Lie bracket with the matrix commutator.

noncomputable def TauCeti.GeneralLinear.tangentLieEquivMatrix {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) ≃ₗ⁅B⁆ Matrix (Fin n) (Fin n) B

The tangent Lie algebra of GLₙ is the matrix Lie algebra. The underlying linear equivalence evaluates tangent derivations on the generic coordinate entries, and the bracket on matrices is the commutator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.GeneralLinear.tangentLieEquivMatrix_apply {R : Type u} [CommRing R] {B : Type w} [CommRing B] [Algebra R B] (n : ℕ) (d : Derivation R (↑(coordinateHopfAlgebra R n)) (Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (tangentLieEquivMatrix n) d = (tangentMatrix n) d

noncomputable def TauCeti.GeneralLinear.cotangentDualMatrixEquiv {k : Type u} [Field k] {n : ℕ} : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n)) ≃ₗ[k] Matrix (Fin n) (Fin n) k

The cotangent-dual Lie algebra of GL_n identified linearly with n × n matrices.

Equations

• TauCeti.GeneralLinear.cotangentDualMatrixEquiv = Derivation.cotangentLinearEquiv.trans (TauCeti.GeneralLinear.tangentLinearEquivMatrix n)

theorem TauCeti.GeneralLinear.cotangentDualMatrixEquiv_apply {k : Type u} [Field k] {n : ℕ} (x : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))) : cotangentDualMatrixEquiv x = (tangentMatrix n) (Derivation.cotangentLinearEquiv x)

The cotangent-dual matrix equivalence evaluates a functional through the corresponding tangent derivation.

theorem TauCeti.GeneralLinear.tangentMatrix_tangentScalarExtensionEquiv_one_tmul {k : Type u} [Field k] {n : ℕ} {A : Type u} [CommRing A] [Algebra k A] (x : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))) : (tangentMatrix n) (Derivation.tangentScalarExtensionEquiv (1 ⊗ₜ[k] x)) = (cotangentDualMatrixEquiv x).map ⇑(algebraMap k A)

Scalar extension of a cotangent-dual tangent vector applies the scalar map entrywise to its matrix. This is the compatibility that lets computations on coefficient-valued derivations be read back in the fixed cotangent-dual Lie algebra.

theorem TauCeti.GeneralLinear.tangentMatrix_tangentScalarExtensionEquiv_tmul {k : Type u} [Field k] {n : ℕ} {A : Type u} [CommRing A] [Algebra k A] (a : A) (x : Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))) : (tangentMatrix n) (Derivation.tangentScalarExtensionEquiv (a ⊗ₜ[k] x)) = a • (cotangentDualMatrixEquiv x).map ⇑(algebraMap k A)

The matrix form of scalar extension on a pure tensor.