The adjoint action on the cotangent-dual Lie algebra

For a Hopf algebra with finite projective cotangent space, the adjoint point representation acts on scalar extensions of the cotangent dual. After the scalar-extension comparison, this action is convolution conjugation, so it preserves the Lie bracket.

Main declarations

• Derivation.adjointLieEquiv: every algebra-valued point acts by Lie algebra automorphisms on the scalar-extended tangent space.
• Derivation.adjointAction_bracket: the established adjoint action preserves brackets.

References

• J. S. Milne, Algebraic Groups (2017), §10.a and item 10.20.

@[simp]

theorem Derivation.adjointAction_bracket {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) (x y : TensorProduct R (↑A) (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : ↑((CategoryTheory.ConcreteCategory.hom (adjointAction A)) g) ⁅x, y⁆ = ⁅↑((CategoryTheory.ConcreteCategory.hom (adjointAction A)) g) x, ↑((CategoryTheory.ConcreteCategory.hom (adjointAction A)) g) y⁆

The adjoint point action preserves the bracket on the scalar-extended tangent space.

noncomputable def Derivation.adjointLieEquiv {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) : TensorProduct R (↑A) (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) ≃ₗ⁅↑A⁆ TensorProduct R (↑A) (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))

Every algebra-valued point acts on the scalar-extended tangent space by a Lie algebra automorphism.

Equations

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

@[simp]

theorem Derivation.adjointLieEquiv_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) (x : TensorProduct R (↑A) (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : (adjointLieEquiv A g) x = ↑((CategoryTheory.ConcreteCategory.hom (adjointAction A)) g) x

The adjoint Lie automorphism acts by the existing adjoint point representation.

@[simp]

theorem Derivation.adjointLieEquiv_one {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) : adjointLieEquiv A 1 = 1

The identity point acts as the identity Lie automorphism.

@[simp]

theorem Derivation.adjointLieEquiv_mul {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) (g h : ↑(TauCeti.HopfAlgebra.points A)) : adjointLieEquiv A (g * h) = (adjointLieEquiv A h).trans (adjointLieEquiv A g)

The adjoint Lie automorphism of a product is the composite of the two adjoint Lie automorphisms.

@[simp]

theorem Derivation.adjointLieEquiv_symm {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] (A : CommAlgCat R) (g : ↑(TauCeti.HopfAlgebra.points A)) : (adjointLieEquiv A g).symm = adjointLieEquiv A g⁻¹

The inverse adjoint Lie automorphism is the automorphism of the inverse point.