The Connes–Kreimer Hopf algebra of nonplanar rooted trees

The pruning bialgebra on ConnesKreimer R (UnorderedTree α) (Coproduct/Pruning.lean) is a Hopf algebra over any commutative ring: the Connes–Kreimer Hopf algebra of nonplanar, not necessarily binary, rooted trees.

The antipode is the inductive formula S(x) = −x − Σ S(x′) · x″ of a graded connected bialgebra (Foissy's notes, §1.3, Lemma 2). As the algebra is commutative, the antipode is an algebra map, so it is determined by its values on trees. Summing over every admissible cut (F, T') of a tree T (crown forest F, trunk T'), including the empty cut (0, T) that supplies the −T term,

S(T) = −Σ_{(F, T')} (Π_{t ∈ F} S(t)) · T'.

This is the Bogolyubov recursion of ConnesKreimer.birkhoffMinus for the identity character and the operator P = -id, so the antipode is defined as that negative part, and S ⋆ id = 1 is the statement that at P = -id the negative part is a convolution inverse. With the antipode in hand, φ₊ = φ₋ ⋆ φ becomes the Birkhoff factorization φ = (φ₋ ∘ S) ⋆ φ₊ of a character.

Main definitions

• ConnesKreimer.antipodeAlgHomN: the antipode, the negative part of the identity at P = -id.

Main results

• ConnesKreimer.antipodeAlgHomN_convMul_id, ConnesKreimer.id_convMul_antipodeAlgHomN: S ⋆ id = 1 = id ⋆ S in the convolution monoid of algebra endomorphisms.
• The HopfAlgebra R (ConnesKreimer R (UnorderedTree α)) instance, over any commutative ring.
• ConnesKreimer.antipode_ofTree: the inductive formula for the antipode on a tree.
• ConnesKreimer.birkhoffFactorization: φ = (φ₋ ∘ S) ⋆ φ₊ for a character φ.

Implementation notes

The construction needs only a commutative ring (for the negation), and the bialgebra only a commutative semiring.

The recursion descends on UnorderedTree.numNodes, the grading by weight: every crown tree has fewer vertices than T (cutSummandsN_crown_numNodes_lt). The recursion makes S a left convolution inverse of the identity. Foissy's proof also takes a right antipode, realized here by the recursion R(T) = −T − Σ_{F ≠ 0} F · R(T') on the trunk; the two agree by left_inv_eq_right_inv in the convolution monoid WithConv (H →ₐ[R] H).

TODO

• State the Bogolyubov recursion, and with it the antipode, for any connected graded bialgebra once mathlib has one (mathlib4#39849).
• Foissy's closed form S(t) = Σ (−1)^(n_c + 1) W^c(t) over the non-total cuts c of t ([Foi] §1.3, Theorem 2).

References

• [CK98]
• [CK00]
• [Foi]

noncomputable def ConnesKreimer.antipodeAlgHomN {R : Type u_1} [CommRing R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₐ[R] ConnesKreimer R (UnorderedTree α)

The antipode, the Bogolyubov negative part of the identity character at P = -id.

Equations

• ConnesKreimer.antipodeAlgHomN = ConnesKreimer.birkhoffMinus LinearMap.id (-AddMonoidHom.id (ConnesKreimer R (UnorderedTree α)))

theorem ConnesKreimer.antipodeAlgHomN_convMul_id {R : Type u_1} [CommRing R] {α : Type u_2} : WithConv.toConv antipodeAlgHomN * WithConv.toConv (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) = 1

S ⋆ id = 1, the left inverse law of the negative part at P = -id. An input to the instance; afterwards this is AlgHom.antipode_id_cancel.

theorem ConnesKreimer.id_convMul_antipodeAlgHomN {R : Type u_1} [CommRing R] {α : Type u_2} : WithConv.toConv (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) * WithConv.toConv antipodeAlgHomN = 1

id ⋆ S = 1, since S equals the right antipode. An input to the instance; afterwards this is LinearMap.id_mul_antipode.

@[instance_reducible]

noncomputable instance ConnesKreimer.instHopfAlgebraUnorderedTree {R : Type u_1} [CommRing R] {α : Type u_2} : HopfAlgebra R (ConnesKreimer R (UnorderedTree α))

Equations

• ConnesKreimer.instHopfAlgebraUnorderedTree = HopfAlgebra.ofConvInverse ConnesKreimer.antipodeAlgHomN.toLinearMap ⋯ ⋯

theorem ConnesKreimer.antipodeAlgHom_eq_antipodeAlgHomN {R : Type u_1} [CommRing R] {α : Type u_2} : HopfAlgebra.antipodeAlgHom R (ConnesKreimer R (UnorderedTree α)) = antipodeAlgHomN

theorem ConnesKreimer.antipode_ofTree {R : Type u_1} [CommRing R] {α : Type u_2} (T : UnorderedTree α) : (HopfAlgebraStruct.antipode R) (ofTree T) = -(Multiset.map (fun (p : Multiset (UnorderedTree α) × UnorderedTree α) => (Multiset.map (fun (t : UnorderedTree α) => (HopfAlgebraStruct.antipode R) (ofTree t)) p.1).prod * ofTree p.2) (cutSummandsN T)).sum

The antipode on a tree, S(T) = −Σ_{(F, T') ∈ cutSummandsN T} (Π_{t ∈ F} S(t)) · T'.

Birkhoff factorization through the antipode

theorem ConnesKreimer.birkhoffFactorization {R : Type u_1} [CommRing R] {α : Type u_2} {ℛ : Type u_3} [CommSemiring ℛ] [Algebra R ℛ] (P : ℛ →+ ℛ) (φ : ConnesKreimer R (UnorderedTree α) →ₐ[R] ℛ) : WithConv.toConv φ = WithConv.toConv ((birkhoffMinus φ.toLinearMap P).comp (HopfAlgebra.antipodeAlgHom R (ConnesKreimer R (UnorderedTree α)))) * WithConv.toConv (birkhoffPlus φ.toLinearMap P)

The Birkhoff factorization φ = (φ₋ ∘ S) ⋆ φ₊ of a character, from φ₊ = φ₋ ⋆ φ and the left inverse φ₋ ∘ S of φ₋.