The tangent Lie algebra of the additive group

The vector group represented by SymmetricAlgebra R M has B-valued tangent module M →ₗ[R] B. Concretely, a counit-valued derivation is determined by its values on the generators SymmetricAlgebra.ι R M x, and every linear assignment of generator values extends uniquely to such a derivation. AdditiveGroup.tangentLinearEquiv packages this as an R-linear equivalence. Specializing to M = R gives AdditiveGroup.gaTangentLinearEquiv, the identification of the tangent module of 𝔾ₐ with B.

Over commutative rings, the convolution bracket of two tangent derivations is zero. It is enough to calculate on a generator: the generator is primitive, so both convolution products vanish there. Thus the tangent Lie algebra of every additive vector group is abelian.

The inverse tangent construction uses SymmetricAlgebra.mkDerivation: a linear map f : M →ₗ[R] B extends uniquely from the canonical generators. No choice of basis or finiteness hypothesis on M is needed.

Main declarations

• TauCeti.AdditiveGroup.tangentLinearEquiv: tangent derivations of a vector group are linear maps from its coordinate module.
• TauCeti.AdditiveGroup.gaTangentLinearEquiv: the tangent module of 𝔾ₐ is the coefficient algebra B.
• TauCeti.AdditiveGroup.tangent_bracket_eq_zero: the tangent Lie bracket is zero.

noncomputable def TauCeti.AdditiveGroup.tangentLinearEquiv {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {B : Type w} [CommSemiring B] [Algebra R B] : Derivation R (SymmetricAlgebra R M) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R M) B) ≃ₗ[R] M →ₗ[R] B

The tangent module of the additive vector group represented by SymmetricAlgebra R M is the module M →ₗ[R] B of possible generator values.

The equivalence sends a derivation d to x ↦ d (SymmetricAlgebra.ι R M x), transported from the counit coefficient synonym back to B. Its inverse sends f : M →ₗ[R] B to the unique derivation taking each generator to f x.

Equations

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

@[simp]

theorem TauCeti.AdditiveGroup.tangentLinearEquiv_apply {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {B : Type w} [CommSemiring B] [Algebra R B] (d : Derivation R (SymmetricAlgebra R M) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R M) B)) (x : M) : (tangentLinearEquiv d) x = (Bialgebra.CounitAlgebra.algEquivSelf R (SymmetricAlgebra R M) B) (d ((SymmetricAlgebra.ι R M) x))

The vector-group tangent equivalence evaluates a derivation on the symmetric-algebra generator.

@[simp]

theorem TauCeti.AdditiveGroup.tangentLinearEquiv_symm_apply_ι {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {B : Type w} [CommSemiring B] [Algebra R B] (f : M →ₗ[R] B) (x : M) : (tangentLinearEquiv.symm f) ((SymmetricAlgebra.ι R M) x) = f x

The inverse vector-group tangent equivalence has the prescribed value on every generator.

noncomputable def TauCeti.AdditiveGroup.gaTangentLinearEquiv {R : Type u} [CommSemiring R] {B : Type w} [CommSemiring B] [Algebra R B] : Derivation R (SymmetricAlgebra R R) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R R) B) ≃ₗ[R] B

The tangent module of the one-dimensional additive group 𝔾ₐ is the value algebra B.

This is the specialization of tangentLinearEquiv to the rank-one coordinate module M = R; it sends a derivation to its value on the coordinate SymmetricAlgebra.ι R R 1.

Equations

• TauCeti.AdditiveGroup.gaTangentLinearEquiv = TauCeti.AdditiveGroup.tangentLinearEquiv.trans (LinearMap.ringLmapEquivSelf R R B)

@[simp]

theorem TauCeti.AdditiveGroup.gaTangentLinearEquiv_apply {R : Type u} [CommSemiring R] {B : Type w} [CommSemiring B] [Algebra R B] (d : Derivation R (SymmetricAlgebra R R) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R R) B)) : gaTangentLinearEquiv d = (Bialgebra.CounitAlgebra.algEquivSelf R (SymmetricAlgebra R R) B) (d ((SymmetricAlgebra.ι R R) 1))

The 𝔾ₐ tangent equivalence reads a derivation on the coordinate ι(1).

theorem TauCeti.AdditiveGroup.tangent_ι_pow_eq_zero {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {B : Type w} [CommSemiring B] [Algebra R B] (d : Derivation R (SymmetricAlgebra R M) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R M) B)) (x : M) {k : ℕ} (hk : k ≠ 1) : d ((SymmetricAlgebra.ι R M) x ^ k) = 0

A tangent derivation annihilates every power other than the first of a coordinate generator.

The generator of a vector group is primitive, so its counit vanishes; the Leibniz rule then leaves the factor ι(x) ^ (k - 1), which acts on the counit coefficient algebra through that vanishing counit. Only the linear term of a coordinate function survives differentiation at the identity, which is what makes a differential read off a linear coefficient.

@[simp]

theorem TauCeti.AdditiveGroup.gaTangentLinearEquiv_symm_apply_ι {R : Type u} [CommSemiring R] {B : Type w} [CommSemiring B] [Algebra R B] (b : B) : (gaTangentLinearEquiv.symm b) ((SymmetricAlgebra.ι R R) 1) = b

The derivation corresponding to b : B under the 𝔾ₐ tangent equivalence takes the coordinate ι(1) to b.

@[simp]

theorem TauCeti.AdditiveGroup.tangent_bracket_eq_zero {R : Type u} [CommSemiring R] {M : Type v} [AddCommMonoid M] [Module R M] {B : Type w} [CommRing B] [Algebra R B] (d e : Derivation R (SymmetricAlgebra R M) (Bialgebra.CounitAlgebra R (SymmetricAlgebra R M) B)) : ⁅d, e⁆ = 0

The convolution Lie bracket on the tangent space of an additive vector group is zero.

Indeed, every symmetric-algebra generator is primitive. Both convolution products of two counit-valued derivations vanish on primitive elements, and derivations are determined by their values on the generators.