Dual-primitive functionals on a bialgebra

A linear functional L : H →ₗ[R] R on a bialgebra is primitive in the dual if L 1 = 0 and L (x * y) = L x * ε y + ε x * L y. This is the pairing form of Bialgebra.IsPrimitiveElem (mathlib4#39841) for the dual of H: the unit of the convolution algebra is ε, and the coproduct of the dual is dual to the product on H, so the two conditions read ε_∨ L = 0 and Δ_∨ L = 1 ⊗ L + L ⊗ 1 after pairing against x ⊗ y. The full linear dual carries no coproduct, so the predicate is stated in pairing form; on the finite dual it coincides with IsPrimitiveElem.

Main declarations

• Bialgebra.IsDualPrimitive: the predicate, with L 1 = 0 as a field (mirroring IsSkewPrimitiveElem.counit_eq_zero, and for the same reason: over a semiring it is not derivable from the product rule).
• Bialgebra.IsDualPrimitive.lie: closure under the convolution commutator bracket — the dual form of IsPrimitiveElem.commutator.
• Bialgebra.dualPrimitives: the dual primitives as a Lie subalgebra of the convolution algebra WithConv (H →ₗ[R] R).

[UPSTREAM] target: Mathlib.RingTheory.Bialgebra.Primitive (created by mathlib4#39841), as the dual companion of IsPrimitiveElem.

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

A linear functional L : H →ₗ[R] R is primitive in the dual of a bialgebra H if L 1 = 0 and L (x * y) = L x * ε y + ε x * L y — the pairing form of Bialgebra.IsPrimitiveElem for the dual of H.

• map_one_eq_zero : L 1 = 0

  A dual primitive vanishes at 1 (the counit of the dual is evaluation at 1).

• map_mul (x y : H) : L (x * y) = L x * CoalgebraStruct.counit y + CoalgebraStruct.counit x * L y

  The derivation-like product rule (the dual comultiplication condition).

theorem Bialgebra.isDualPrimitive_iff (R : Type u_1) [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] (L : H →ₗ[R] R) : IsDualPrimitive R L ↔ L 1 = 0 ∧ ∀ (x y : H), L (x * y) = L x * CoalgebraStruct.counit y + CoalgebraStruct.counit x * L y

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

theorem Bialgebra.IsDualPrimitive.add {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] {L₁ L₂ : H →ₗ[R] R} (h₁ : IsDualPrimitive R L₁) (h₂ : IsDualPrimitive R L₂) : IsDualPrimitive R (L₁ + L₂)

theorem Bialgebra.IsDualPrimitive.smul {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] {L : H →ₗ[R] R} (hL : IsDualPrimitive R L) (c : R) : IsDualPrimitive R (c • L)

theorem Bialgebra.IsDualPrimitive.map_mul_eq_zero {R : Type u_1} [CommSemiring R] {H : Type u_2} [Semiring H] [Bialgebra R H] {L : H →ₗ[R] R} {x y : H} (hL : IsDualPrimitive R L) (hx : CoalgebraStruct.counit x = 0) (hy : CoalgebraStruct.counit y = 0) : L (x * y) = 0

A dual primitive vanishes on products of counit-less elements; in particular on decomposable basis elements of a graded bialgebra.

The Lie subalgebra of dual primitives

theorem Bialgebra.IsDualPrimitive.lie {R : Type u_1} [CommRing R] {H : Type u_2} [Semiring H] [Bialgebra R H] {L₁ L₂ : H →ₗ[R] R} (h₁ : IsDualPrimitive R L₁) (h₂ : IsDualPrimitive R L₂) : IsDualPrimitive R ⁅WithConv.toConv L₁, WithConv.toConv L₂⁆.ofConv

Dual primitives are closed under the convolution commutator bracket: the Sweedler expansion of ⁅L₁, L₂⁆ (x * y) produces cross terms symmetric in (L₁, L₂), which cancel in the commutator. The dual form of IsPrimitiveElem.commutator.

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

The dual primitives of a bialgebra H, as a Lie subalgebra of the convolution algebra WithConv (H →ₗ[R] R) under the ring commutator bracket — the dual-side form of the Lie algebra of primitive elements.

Equations

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

@[simp]

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