Primitive elements in a bialgebra

This file records integral-coefficient formulas for the comultiplication of powers, divided powers, and binomial coefficients of a primitive element. The two tensor factors commute even when the bialgebra itself is noncommutative. It also computes the counit of the latter two families when the underlying element has counit zero.

Main results

• TauCeti.Bialgebra.comul_pow_of_primitive: the comultiplication of a power of a primitive element is its binomial expansion.
• TauCeti.Bialgebra.comul_dividedPower_of_primitive: the comultiplication of a divided power has coefficient one on every antidiagonal term.
• TauCeti.Bialgebra.comul_choose_of_primitive: the comultiplication of a binomial coefficient has the same coefficient-one formula.

theorem TauCeti.Bialgebra.comul_pow_of_primitive {R : Type u} {A : Type w} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : A) (h : CoalgebraStruct.comul a = a ⊗ₜ[R] 1 + 1 ⊗ₜ[R] a) (n : ℕ) : CoalgebraStruct.comul (a ^ n) = ∑ mn ∈ Finset.antidiagonal n, n.choose mn.1 • (a ^ mn.1) ⊗ₜ[R] (a ^ mn.2)

The comultiplication of a power of a primitive element is its binomial expansion.

theorem TauCeti.Bialgebra.comul_dividedPower_of_primitive {A : Type w} [Semiring A] [Bialgebra ℚ A] (a : A) (h : CoalgebraStruct.comul a = a ⊗ₜ[ℚ] 1 + 1 ⊗ₜ[ℚ] a) (n : ℕ) : CoalgebraStruct.comul (Associative.dividedPower n a) = ∑ ij ∈ Finset.antidiagonal n, Associative.dividedPower ij.1 a ⊗ₜ[ℚ] Associative.dividedPower ij.2 a

The comultiplication of a divided power of a primitive element has integral structure constants: Δ(a⁽ⁿ⁾) = ∑ i+j=n, a⁽ⁱ⁾ ⊗ a⁽ʲ⁾.

This is the formula used for the divided-power generators of a Kostant integral form.

theorem TauCeti.Bialgebra.counit_dividedPower_of_counit_eq_zero {A : Type w} [Semiring A] [Bialgebra ℚ A] (a : A) (h : CoalgebraStruct.counit a = 0) (n : ℕ) : CoalgebraStruct.counit (Associative.dividedPower (n + 1) a) = 0

A counit that kills an element also kills all its positive divided powers.

theorem TauCeti.Bialgebra.comul_choose_of_primitive {A : Type w} [Ring A] [Bialgebra ℚ A] (a : A) (h : CoalgebraStruct.comul a = a ⊗ₜ[ℚ] 1 + 1 ⊗ₜ[ℚ] a) (n : ℕ) : CoalgebraStruct.comul (Ring.choose a n) = ∑ ij ∈ Finset.antidiagonal n, Ring.choose a ij.1 ⊗ₜ[ℚ] Ring.choose a ij.2

The comultiplication of a binomial coefficient in a primitive element has integral structure constants: Δ((a choose n)) = ∑ i+j=n, (a choose i) ⊗ (a choose j).

This is the formula used for the Cartan generators of a Kostant integral form.

theorem TauCeti.Bialgebra.counit_choose_of_counit_eq_zero {A : Type w} [Ring A] [Bialgebra ℚ A] (a : A) (h : CoalgebraStruct.counit a = 0) (n : ℕ) : CoalgebraStruct.counit (Ring.choose a (n + 1)) = 0

A counit that kills an element also kills all its positive binomial coefficients.