The tangent Lie algebra is natural in the coefficient algebra

Postcomposition along a homomorphism of coefficient rings preserves the convolution commutator bracket on counit-valued derivations. Thus the functorial linear map Derivation.mapValue upgrades to a Lie algebra homomorphism. This is the Lie-algebra layer of the natural adjoint action constructed in Tangent.Naturality.

Main declarations

• Derivation.mapValue_lie: postcomposition preserves the tangent bracket.
• Derivation.lieMapValue: change of coefficients as a Lie algebra homomorphism.

@[simp]

theorem Derivation.mapValue_lie {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] (phi : B →ₐ[R] C) (d e : Derivation R A (TauCeti.Bialgebra.CounitAlgebra R A B)) : (mapValue phi) ⁅d, e⁆ = ⁅(mapValue phi) d, (mapValue phi) e⁆

Postcomposition of counit-valued derivations preserves their convolution commutator bracket.

noncomputable def Derivation.lieMapValue {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [CommRing 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)

Change of coefficient algebra on the tangent Lie algebra.

Equations

• Derivation.lieMapValue phi = { toLinearMap := Derivation.mapValue phi, map_lie' := ⋯ }

@[simp]

theorem Derivation.lieMapValue_toLinearMap {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] (phi : B →ₐ[R] C) : ↑(lieMapValue phi) = mapValue phi

The underlying linear map of change of coefficients on the tangent Lie algebra is mapValue.

@[simp]

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

Change of coefficients on the tangent Lie algebra acts pointwise by postcomposition.

@[simp]

theorem Derivation.lieMapValue_id {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] : lieMapValue (AlgHom.id R B) = LieHom.id

Change of coefficients by the identity is the identity Lie algebra homomorphism.

@[simp]

theorem Derivation.lieMapValue_comp {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommRing R] [CommRing A] [Bialgebra R A] [CommRing B] [Algebra R B] [CommRing C] [Algebra R C] {D : Type u_5} [CommRing D] [Algebra R D] (psi : C →ₐ[R] D) (phi : B →ₐ[R] C) : lieMapValue (psi.comp phi) = (lieMapValue psi).comp (lieMapValue phi)

Change of coefficients on tangent Lie algebras preserves composition.