The tangent Lie algebra of the multiplicative group

The tangent space at the identity of the multiplicative group is one-dimensional. A tangent derivation of the Laurent polynomial Hopf algebra R[T;T⁻¹] is determined by its value on T, and every value occurs. The resulting linear equivalence with the coefficient algebra B identifies the tangent Lie bracket with the zero bracket.

Main declarations

• TauCeti.MultiplicativeGroup.tangentLinearEquiv: the tangent space of 𝔾ₘ is linearly equivalent to B.
• TauCeti.MultiplicativeGroup.tangent_bracket_eq_zero: the tangent Lie bracket of 𝔾ₘ vanishes.

References

The construction follows the formal pattern of TauCeti.Algebra.AlgebraicGroup.AdditiveGroup.Tangent. Laurent-polynomial induction and the formulas for the counit and comultiplication of T come from Mathlib's Mathlib.Algebra.Polynomial.Laurent and Mathlib.RingTheory.Bialgebra.MonoidAlgebra.

This realizes the 𝔾ₘ item in the ReductiveGroups roadmap's "Worked examples" section using its Layer 2 tangent/Lie algebra infrastructure.

theorem TauCeti.MultiplicativeGroup.derivation_ext {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] {d e : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)} (h : d (LaurentPolynomial.T 1) = e (LaurentPolynomial.T 1)) : d = e

Two tangent derivations of the Laurent polynomial algebra are equal if they agree on T.

theorem TauCeti.MultiplicativeGroup.derivation_ext_iff {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] {d e : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)} : d = e ↔ d (LaurentPolynomial.T 1) = e (LaurentPolynomial.T 1)

noncomputable def TauCeti.MultiplicativeGroup.tangentLinearEquiv {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B) ≃ₗ[B] B

The tangent space at the identity of 𝔾ₘ is one-dimensional. The equivalence sends a counit-valued derivation to its value on the Laurent generator T.

Equations

• TauCeti.MultiplicativeGroup.tangentLinearEquiv = LinearEquiv.ofBijective TauCeti.MultiplicativeGroup.tangentCoordinate✝ ⋯

@[simp]

theorem TauCeti.MultiplicativeGroup.tangentLinearEquiv_apply {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] (d : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)) : tangentLinearEquiv d = (Bialgebra.CounitAlgebra.algEquivSelf R (LaurentPolynomial R) B) (d (LaurentPolynomial.T 1))

The tangent equivalence evaluates a derivation on the Laurent generator T.

@[simp]

theorem TauCeti.MultiplicativeGroup.tangentLinearEquiv_symm_apply_T {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] (b : B) : (tangentLinearEquiv.symm b) (LaurentPolynomial.T 1) = b

The derivation corresponding to b : B takes the Laurent generator T to b.

@[simp]

theorem TauCeti.MultiplicativeGroup.tangent_bracket_eq_zero {R : Type u} [CommSemiring R] {B : Type w} [CommRing B] [Algebra R B] (d e : Derivation R (LaurentPolynomial R) (Bialgebra.CounitAlgebra R (LaurentPolynomial R) B)) : ⁅d, e⁆ = 0

The tangent Lie algebra of 𝔾ₘ is abelian.