Primitive elements in a bialgebra

This file collects facts about primitive elements in a bialgebra.

Main declarations

• Bialgebra.IsPrimitiveElem R a: a is primitive, i.e. ε a = 0 and Δ a = 1 ⊗ₜ a + a ⊗ₜ 1.

TODO

• Primitive elements form a LieSubalgebra with bracket [a, b] = a * b - b * a. (IsPrimitiveElem.commutator avoids ⁅a, b⁆ so as not to import Lie theory here.)
• In characteristic 0 over a field, the primitive elements of a cocommutative connected bialgebra generate it as the universal enveloping of a Lie algebra. (Milnor–Moore)

References

• D. Grinberg, V. Reiner, Hopf algebras in combinatorics

@[reducible, inline]

abbrev Bialgebra.IsPrimitiveElem (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) : Prop

A primitive element of a bialgebra is a (1, 1)-skew-primitive element, i.e. an element a such that ε a = 0 and Δ a = 1 ⊗ₜ a + a ⊗ₜ 1.

Equations

• Bialgebra.IsPrimitiveElem R a = Coalgebra.IsSkewPrimitiveElem R 1 1 a

theorem Bialgebra.IsPrimitiveElem.ne_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a : A} [Nontrivial R] (ha : IsPrimitiveElem R a) : a ≠ 1

theorem Bialgebra.counit_eq_zero_of_comul_eq_tmul_add_tmul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a : A} [IsCancelAdd A] (ha : CoalgebraStruct.comul a = 1 ⊗ₜ[R] a + a ⊗ₜ[R] 1) : CoalgebraStruct.counit a = 0

See Proposition 1.4.17 in [GR20].

theorem Bialgebra.isPrimitiveElem_iff_comul_eq_tmul_add_tmul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a : A} [IsCancelAdd A] : IsPrimitiveElem R a ↔ CoalgebraStruct.comul a = 1 ⊗ₜ[R] a + a ⊗ₜ[R] 1

theorem Bialgebra.IsPrimitiveElem.commutator {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Bialgebra R A] {a b : A} (ha : IsPrimitiveElem R a) (hb : IsPrimitiveElem R b) : IsPrimitiveElem R (a * b - b * a)

The commutator [a, b] = a * b - b * a of two primitive elements is primitive.