Dual-primitive functionals on a bialgebra

A linear functional f on a bialgebra A is primitive in the dual if f 1 = 0 and f (a * b) = f a * ε b + ε a * f b, where ε is the counit. The product of A transposes to a comultiplication on functionals, for which ε is the unit, and the two conditions say that f is a primitive element for it. Radford calls such an f an ε:ε-derivation of A and identifies these with the primitive elements of the finite dual. Under the commutator of the convolution product they form a Lie algebra, which Connes and Kreimer attach to the Hopf algebra of rooted trees.

Main definitions

• Bialgebra.IsDualPrimitive R f: the functional f is primitive in the dual.
• Bialgebra.dualPrimitives R A: the dual primitives, as a Lie subalgebra of the convolution algebra WithConv (A →ₗ[R] R).

Main results

• Bialgebra.IsDualPrimitive.convMul_apply_mul: the convolution product of two dual primitives obeys a second-order product rule, whose cross terms are symmetric in the two functionals.
• Bialgebra.IsDualPrimitive.lie: the commutator of two dual primitives is a dual primitive.
• Bialgebra.IsPrimitiveElem.isDualPrimitive: a pairing of bialgebras sends primitive elements to dual primitives.

Implementation notes

f 1 = 0 is a field, as in Derivation and as the counit condition is in Coalgebra.IsSkewPrimitiveElem. It follows from the product rule when addition on R cancels (Bialgebra.isDualPrimitive_iff_leibniz), but not over every semiring.

[UPSTREAM] Belongs beside Mathlib/RingTheory/Bialgebra/Primitive.lean, as the dual of Bialgebra.IsPrimitiveElem.

References

• [Rad12]
• [CK98]

structure Bialgebra.IsDualPrimitive (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (f : A →ₗ[R] R) : Prop

A linear functional f on a bialgebra is primitive in the dual if f 1 = 0 and f (a * b) = f a * ε b + ε a * f b, where ε is the counit.

• map_one_eq_zero : f 1 = 0

  A dual primitive vanishes at 1.

• leibniz (a b : A) : f (a * b) = f a * CoalgebraStruct.counit b + CoalgebraStruct.counit a * f b

  A dual primitive obeys the product rule of a derivation at the counit.

theorem Bialgebra.isDualPrimitive_iff (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (f : A →ₗ[R] R) : IsDualPrimitive R f ↔ f 1 = 0 ∧ ∀ (a b : A), f (a * b) = f a * CoalgebraStruct.counit b + CoalgebraStruct.counit a * f b

@[simp]

theorem Bialgebra.IsDualPrimitive.zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : IsDualPrimitive R 0

theorem Bialgebra.IsDualPrimitive.add {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f g : A →ₗ[R] R} (hf : IsDualPrimitive R f) (hg : IsDualPrimitive R g) : IsDualPrimitive R (f + g)

theorem Bialgebra.IsDualPrimitive.smul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f : A →ₗ[R] R} (hf : IsDualPrimitive R f) (r : R) : IsDualPrimitive R (r • f)

theorem Bialgebra.IsDualPrimitive.map_mul_eq_zero {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f : A →ₗ[R] R} {a b : A} (hf : IsDualPrimitive R f) (ha : CoalgebraStruct.counit a = 0) (hb : CoalgebraStruct.counit b = 0) : f (a * b) = 0

A dual primitive vanishes on the product of two elements of counit zero.

theorem Bialgebra.IsDualPrimitive.convMul_apply_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f g : A →ₗ[R] R} (hf : IsDualPrimitive R f) (hg : IsDualPrimitive R g) (a b : A) : (WithConv.toConv f * WithConv.toConv g).ofConv (a * b) = (WithConv.toConv f * WithConv.toConv g).ofConv a * CoalgebraStruct.counit b + f a * g b + g a * f b + CoalgebraStruct.counit a * (WithConv.toConv f * WithConv.toConv g).ofConv b

The convolution product of two dual primitives obeys a second-order product rule. Its cross terms f a * g b + g a * f b are symmetric in f and g, so they cancel in the commutator.

theorem Bialgebra.isDualPrimitive_iff_leibniz {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {f : A →ₗ[R] R} [IsCancelAdd R] : IsDualPrimitive R f ↔ ∀ (a b : A), f (a * b) = f a * CoalgebraStruct.counit b + CoalgebraStruct.counit a * f b

When addition on R cancels, the product rule alone makes a functional a dual primitive.

theorem Bialgebra.IsPrimitiveElem.isDualPrimitive {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {B : Type u_3} [Semiring B] [Bialgebra R B] {b : B} (hb : IsPrimitiveElem R b) {p : B →ₗ[R] A →ₗ[R] R} (h_one : ∀ (a : A), (p 1) a = CoalgebraStruct.counit a) (h_counit : ∀ (b : B), (p b) 1 = CoalgebraStruct.counit b) (h_mul : ∀ (a a' : A), WithConv.toConv (p.flip (a * a')) = WithConv.toConv (p.flip a) * WithConv.toConv (p.flip a')) : IsDualPrimitive R (p b)

A pairing of bialgebras that transposes the product of A to the comultiplication of B, and the units to the counits, sends the primitive elements of B to dual primitives of A.

theorem Bialgebra.IsDualPrimitive.lie {R : Type u_1} {A : Type u_2} [CommRing R] [Semiring A] [Bialgebra R A] {f g : A →ₗ[R] R} (hf : IsDualPrimitive R f) (hg : IsDualPrimitive R g) : IsDualPrimitive R ⁅WithConv.toConv f, WithConv.toConv g⁆.ofConv

The commutator of two dual primitives under the convolution product is a dual primitive.

def Bialgebra.dualPrimitives (R : Type u_1) (A : Type u_2) [CommRing R] [Semiring A] [Bialgebra R A] : LieSubalgebra R (WithConv (A →ₗ[R] R))

The dual primitives of a bialgebra, as a Lie subalgebra of its convolution algebra of linear functionals under the commutator bracket.

Equations

• Bialgebra.dualPrimitives R A = { carrier := {f : WithConv (A →ₗ[R] R) | Bialgebra.IsDualPrimitive R f.ofConv}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem Bialgebra.mem_dualPrimitives {R : Type u_1} {A : Type u_2} [CommRing R] [Semiring A] [Bialgebra R A] {f : WithConv (A →ₗ[R] R)} : f ∈ dualPrimitives R A ↔ IsDualPrimitive R f.ofConv