The adjoint representation on the base Lie algebra

For a commutative Hopf algebra H over a commutative ring R, the adjoint action is initially defined on the coefficient-dependent tangent modules

Derivation R H (Bialgebra.CounitAlgebra R H A).

When the augmentation cotangent space is finite projective, these tangent modules are scalar extensions of the single R-module dual to the cotangent space. This file transports the coefficient-natural adjoint action across that equivalence. The result is a point representation, its corresponding comodule, and, after choosing a finite basis, the coordinate morphism O(GL_n) ⟶ H opposite to Ad : Spec H ⟶ GL_n.

Main declarations

• Derivation.mapValue_tangentScalarExtensionEquiv: scalar extension of tangent vectors is natural in the coefficient algebra.
• Derivation.adjointPointRepresentation: the adjoint action on the base Lie algebra as a natural point representation.
• Derivation.adjointComodule: the corresponding right H-comodule.
• Derivation.adjointCoordinateBialgHom: the coordinate morphism of the adjoint representation in a finite basis.

References

• J. S. Milne, Algebraic Groups (2017), §14.

This is the fixed-module packaging of the adjoint representation requested in Layer 2 of the ReductiveGroups roadmap.

@[simp]

theorem Derivation.mapValue_tangentScalarExtensionEquiv {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Bialgebra R H] [Module.Finite R (TauCeti.Bialgebra.CotangentSpace R H)] [Module.Projective R (TauCeti.Bialgebra.CotangentSpace R H)] {A : Type w} {B : Type x} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (phi : A →ₐ[R] B) (x : TensorProduct R A (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : (mapValue phi) (tangentScalarExtensionEquiv x) = tangentScalarExtensionEquiv ((LinearMap.rTensor (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) phi.toLinearMap) x)

Scalar extension of tangent vectors commutes with a coefficient-algebra morphism even when the source and target algebras live in different universes.

noncomputable def Derivation.pointInCounitAlgebra {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (A : Type w) [CommRing A] [Algebra R A] : WithConv (H →ₐ[R] A) →* WithConv (H →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R H A)

Regard a point with values in A as one with values in the indexed copy of A carrying the counit-induced H-algebra structure.

Equations

• Derivation.pointInCounitAlgebra A = TauCeti.AlgHom.mapValue ↑(TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H A).symm

@[simp]

theorem Derivation.pointInCounitAlgebra_apply {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] (A : Type w) [CommRing A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (h : H) : ((pointInCounitAlgebra A) g).ofConv h = g.ofConv h

Regarding a point as counit-algebra-valued does not change its values.

@[simp]

theorem Derivation.pointInCounitAlgebra_mapPoints {R : Type u} {H : Type v} [CommRing R] [CommRing H] [HopfAlgebra R H] {A B : CommAlgCat R} (phi : A ⟶ B) (g : ↑(TauCeti.HopfAlgebra.points A)) : (pointInCounitAlgebra ↑B) ((CategoryTheory.ConcreteCategory.hom (TauCeti.HopfAlgebra.mapPoints phi)) g) = (TauCeti.AlgHom.mapValue (TauCeti.Bialgebra.CounitAlgebra.mapAlgHom (CommAlgCat.Hom.hom phi))) ((pointInCounitAlgebra ↑A) g)

Changing the value algebra of a point commutes with regarding it as a point valued in the counit-indexed copy of that algebra.

noncomputable def Derivation.adjointAction {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) : TauCeti.HopfAlgebra.points A ⟶ TauCeti.GeneralLinear.scalarExtensionAutomorphisms A

The adjoint action at a coefficient algebra, transported from coefficient-valued derivations to the scalar extension of the dual cotangent space.

Equations

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

theorem Derivation.adjointAction_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)) : (CategoryTheory.ConcreteCategory.hom (adjointAction A)) g = (LinearMap.GeneralLinearGroup.congrLinearEquiv tangentScalarExtensionEquiv.symm) ((adRepresentation ↑A).asGroupHom ((pointInCounitAlgebra ↑A) g))

The transported adjoint action is conjugation of the coefficient-valued adjoint operator by the tangent scalar-extension equivalence.

@[simp]

theorem Derivation.tangentScalarExtensionEquiv_adjointAction {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))) : tangentScalarExtensionEquiv (↑((CategoryTheory.ConcreteCategory.hom (adjointAction A)) g) x) = adDerivation (↑A) ((pointInCounitAlgebra ↑A) g) (tangentScalarExtensionEquiv x)

Transporting the fixed-module adjoint action to coefficient-valued derivations recovers convolution conjugation.

noncomputable def Derivation.adjointPointRepresentation {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)] : TauCeti.HopfAlgebra.PointRepresentation

The adjoint action on the base Lie algebra, expressed as a natural point representation on the dual of the augmentation cotangent space.

Equations

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

@[simp]

theorem Derivation.adjointPointRepresentation_action {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)) : (CategoryTheory.ConcreteCategory.hom (adjointPointRepresentation.action A)) g = (CategoryTheory.ConcreteCategory.hom (adjointAction A)) g

The concrete action of the adjoint point representation is the transported convolution adjoint action.

@[irreducible]

noncomputable def Derivation.adjointComodule {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)] : TauCeti.Comodule R H (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))

The adjoint comodule on the dual of the augmentation cotangent space.

Equations

• Derivation.adjointComodule = Derivation.adjointPointRepresentation.toComodule

@[simp]

theorem Derivation.adjointComodule_coact_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)] (x : Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) : TauCeti.Comodule.coact x = (TensorProduct.comm R H (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) ((TensorProduct.map ULift.algEquiv.{u, v, max u v}.toLinearMap LinearMap.id) (↑((CategoryTheory.ConcreteCategory.hom (adjointPointRepresentation.action ↧(ULift.{max u v, v} H))) (WithConv.toConv ↑ULift.algEquiv.{u, v, max u v}.symm)) (1 ⊗ₜ[R] x)))

The adjoint coaction is the flipped action of the universal point.

theorem Derivation.tangentScalarExtensionEquiv_adjointComodule_endOfPoint {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))) : tangentScalarExtensionEquiv ((TauCeti.Comodule.endOfPoint (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H)) g.ofConv) x) = adDerivation (↑A) ((pointInCounitAlgebra ↑A) g) (tangentScalarExtensionEquiv x)

The point action of the adjoint comodule is convolution conjugation after the canonical scalar-extension identification of tangent vectors.

noncomputable def Derivation.adjointCoordinateBialgHom {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)] {n : ℕ} (b : Module.Basis (Fin n) R (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) : ↑(TauCeti.GeneralLinear.coordinateHopfAlgebra R n) →ₐc[R] H

The coordinate Hopf-algebra morphism opposite to the adjoint representation in a basis indexed by Fin n.

Equations

• Derivation.adjointCoordinateBialgHom b = TauCeti.Comodule.coordinateBialgHom b

@[simp]

theorem Derivation.adjointCoordinateBialgHom_X {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)] {n : ℕ} (b : Module.Basis (Fin n) R (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) (i j : Fin n) : (adjointCoordinateBialgHom b) ((TauCeti.GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((TauCeti.GeneralLinear.coordinateRingMap R n) (MvPolynomial.X (i, j)))) = have x := adjointComodule; TauCeti.Comodule.coefficientMatrix b i j

The adjoint coordinate morphism sends a generic matrix entry to the corresponding matrix coefficient of the adjoint comodule.

@[simp]

theorem Derivation.adjointCoordinateBialgHom_antipode_X {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)] {n : ℕ} (b : Module.Basis (Fin n) R (Module.Dual R (TauCeti.Bialgebra.CotangentSpace R H))) (i j : Fin n) : (adjointCoordinateBialgHom b) ((TauCeti.GeneralLinear.coordinateHopfAlgebraAlgEquiv R n) ((TauCeti.GeneralLinear.localizedGenericMatrix R n)⁻¹ i j)) = have x := adjointComodule; (HopfAlgebraStruct.antipode R) (TauCeti.Comodule.coefficientMatrix b i j)

The adjoint coordinate morphism sends an antipode generator to the antipode of the corresponding matrix coefficient.