Naturality of the tangent and adjoint actions in the coefficient algebra

For a bialgebra A over R, the tangent space is naturally a functor of the coefficient algebra:

B ↦ Derivation R A (Bialgebra.CounitAlgebra R A B).

An R-algebra homomorphism φ : B →ₐ[R] C postcomposes a counit-valued derivation. The underlying maps of counit algebras are defined in Tangent.Basic; this file packages postcomposition as Derivation.mapValue, proves its functoriality, and, when A is a Hopf algebra, shows that it intertwines the adjoint actions at B and C. Together, these statements make the valuewise representations in Tangent.Adjoint into a natural action on the Lie functor.

Main declarations

• TauCeti.Bialgebra.CounitAlgebra.mapAlgHom: the coefficient algebra map.
• TauCeti.Bialgebra.CounitAlgebra.map: the same map, linear over the bialgebra through the counit actions.
• Derivation.mapValue: postcomposition of counit-valued derivations.
• Derivation.mapValue_adDerivation: the adjoint action commutes with change of coefficient algebra.

The Lie-bracket compatibility, which requires additive inverses, is in Tangent.Lie.Naturality.

References

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

noncomputable def Derivation.mapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B) →ₗ[R] Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A C)

Postcomposition of a counit-valued derivation along an algebra homomorphism of coefficients. This is the functorial map on tangent vectors.

Equations

• Derivation.mapValue phi = ↑R (TauCeti.Bialgebra.CounitAlgebra.map phi).compDer

@[simp]

theorem Derivation.mapValue_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) (a : A) : ((mapValue phi) d) a = phi (d a)

Postcomposition of a counit-valued derivation acts pointwise.

@[simp]

theorem Derivation.coe_mapValue_linearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (phi : B →ₐ[R] C) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : ↑((mapValue phi) d) = (TauCeti.Bialgebra.CounitAlgebra.mapAlgHom phi).toLinearMap ∘ₗ ↑d

On underlying linear maps, change of coefficients is postcomposition by the coefficient algebra map.

@[simp]

theorem Derivation.mapValue_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] : mapValue (AlgHom.id R B) = LinearMap.id

Postcomposition by the identity is the identity on counit-valued derivations.

@[simp]

theorem Derivation.mapValue_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [Bialgebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] {D : Type u_5} [Semiring D] [Algebra R D] (psi : C →ₐ[R] D) (phi : B →ₐ[R] C) : mapValue (psi.comp phi) = mapValue psi ∘ₗ mapValue phi

Postcomposition of counit-valued derivations preserves composition.

@[simp]

theorem Derivation.mapValue_adDerivation {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] [CommSemiring B] [Algebra R B] [CommSemiring C] [Algebra R C] (phi : B →ₐ[R] C) (g : WithConv (A →ₐ[R] TauCeti.Bialgebra.CounitAlgebra R A B)) (d : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : (mapValue phi) (adDerivation B g d) = adDerivation C ((TauCeti.AlgHom.mapValue (TauCeti.Bialgebra.CounitAlgebra.mapAlgHom phi)) g) ((mapValue phi) d)

The adjoint action is natural in the coefficient algebra. Mapping a point and a tangent vector along phi and then applying the adjoint action gives the same result as applying the action first and postcomposing the resulting derivation.