Birkhoff factorization on the Connes–Kreimer Hopf algebra [UPSTREAM] #
[MCB25]'s renormalization of a character (Prop. 3.1.7): given a character
φ : H → ℛ from the Hopf algebra H of nonplanar rooted trees into a commutative algebra ℛ
carrying a weight--1 Rota–Baxter operator R, the Bogolyubov recursion splits φ into a
"meaningless part" φ₋ and a renormalized, consistency-checked part φ₊. This is the algebraic
core of the "single map that recursively modifies an assignment of semantic values so as to
incorporate the consistency checking over all substructures."
The negative part φ₋ is built by the same cutSummandsN/depth recursion as the Hopf antipode
antipodeTreeN, with two substitutions: the canonical embedding ofTree rem becomes the character
value φ (ofTree rem) ∈ ℛ, and the bare negation becomes −R. Indeed antipodeTreeN is the
R = id, canonical-character specialization of this recursion (S(x) = −x − Σ S(x′)·x″),
proved here as birkhoffMinusTree_id_eq_antipodeTreeN.
For a genuine character φ : H →ₐ[R] ℛ (a multiplicative assignment, Def. 3.1.3) the two parts
satisfy the full factorization φ = (φ₋ ∘ S) ⋆ φ₊ (Def. 3.1.5), proved in birkhoffFactorization.
We work in the character convolution monoid WithConv (H →ₐ[R] ℛ); per Rem. 3.1.4 the target ℛ
carries no coproduct, so this is not mathlib's AlgHom.convGroup (target-bialgebra) — the
convolution inverse φ₋ ∘ S of the character φ₋ is read off directly from the antipode law
(antipodeComp_convMul_self).
Main definitions #
birkhoffMinusTree φ R T/birkhoffMinus φ R: the Bogolyubov negative partφ₋on a tree, and as an algebra homH →ₐ[R] ℛintorange R = ℛ₋.birkhoffPlusTree φ R T/birkhoffPlus φ R: the renormalized partφ₊ = (1 − R)(φ̃)on a tree, and as an algebra homH →ₐ[R] ℛintorange (1 − R) = ℛ₊.
Main results #
birkhoffFactorization_ofTree:φ₊ = φ₋ ⋆ φon generators (Def. 3.1.6), for any linearφ.birkhoffPlus_eq_convMul:φ₊ = φ₋ ⋆ φon all ofH, for a characterφ(Def. 3.1.6).birkhoffFactorization:φ = (φ₋ ∘ S) ⋆ φ₊for a characterφ(Def. 3.1.5, eq. (3.1.4)).birkhoffMinusTree_id_eq_antipodeTreeN: theR = idcounterterm is the Hopf antipode.
References #
[MCB25] (Def. 3.1.1, Def. 3.1.3, Rem. 3.1.4, Def. 3.1.5, Def. 3.1.6, Prop. 3.1.7, Rem. 3.1.8)
The Bogolyubov negative part φ₋ on a single tree ([MCB25]
Prop. 3.1.7): φ₋(T) = −R(Σ_{(cf,rem) ∈ cutSummandsN T} (Π_{Tᵢ ∈ cf} φ₋(Tᵢ)) · φ(ofTree rem)).
Models antipodeTreeN with the character value φ(ofTree rem) in place of ofTree rem and
the Rota–Baxter −R in place of bare negation; well-founded on T.depth.
Equations
- One or more equations did not get rendered due to their size.
Instances For
φ₋ extended multiplicatively to forests, as a MonoidHom on Multiplicative (Forest …).
Mirrors antipodeMonoidHomN.
Equations
- One or more equations did not get rendered due to their size.
Instances For
φ₋ as an algebra hom H →ₐ[R] ℛ, lifting birkhoffMinusMonoidHom via
ConnesKreimer.lift. Mirrors antipodeAlgHomN.
Equations
Instances For
φ₋ on a forest basis element is the product of φ₋ over its trees. Mirrors
antipodeAlgHomN_apply_of'.
φ₋ on a single tree generator agrees with birkhoffMinusTree. Mirrors
antipodeAlgHomN_apply_ofTree.
The Bogolyubov preparation and the renormalized part #
The Bogolyubov preparation φ̃ ([MCB25] Rem. 3.1.8):
φ̃(T) = Σ_{(cf,rem) ∈ cutSummandsN T} (Π_{Tᵢ ∈ cf} φ₋(Tᵢ)) · φ(ofTree rem), of which the
negative part is φ₋(T) = −R(φ̃(T)) and the renormalized part is φ₊(T) = (1−R)(φ̃(T)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Bogolyubov preparation in non-attach-decorated form: the attach def keeps the
membership info for well-foundedness, this strips it for downstream proofs. Mirrors
antipodeTreeN_unfold.
φ₋(T) = −R(φ̃(T)): the negative part is −R applied to the Bogolyubov preparation.
The renormalized part φ₊ on a single tree ([MCB25] Prop. 3.1.7):
φ₊(T) = (1−R)(φ̃(T)) = φ̃(T) − R(φ̃(T)) — the consistency-checked value.
Equations
- RootedTree.ConnesKreimer.birkhoffPlusTree φ RB T = RootedTree.ConnesKreimer.birkhoffPrepTree φ RB T - RB.op (RootedTree.ConnesKreimer.birkhoffPrepTree φ RB T)
Instances For
φ₊(T) = φ̃(T) + φ₋(T): the renormalized and negative parts recover the preparation.
φ₊ as an algebra hom (the renormalized character) #
φ₊ extended multiplicatively to forests, as a MonoidHom. Mirrors
birkhoffMinusMonoidHom; the renormalized character φ₊ : H → R₊ of
[MCB25] Prop. 3.1.7 is an algebra hom into range (1 − R).
Equations
- One or more equations did not get rendered due to their size.
Instances For
φ₊ as an algebra hom H →ₐ[R] ℛ, lifting birkhoffPlusMonoidHom. Mirrors
birkhoffMinus; the multiplicative extension of birkhoffPlusTree is automatically an
algebra hom, so this is the renormalized character φ₊.
Equations
Instances For
φ₊ on a forest basis element is the product of φ₊ over its trees. Mirrors
birkhoffMinus_apply_of'.
φ₊ on a single tree generator agrees with birkhoffPlusTree. Mirrors
birkhoffMinus_apply_ofTree.
The Birkhoff factorization φ₊ = φ₋ ⋆ φ #
Birkhoff factorization on generators ([MCB25] Def. 3.1.6,
φ₊ = φ₋ ⋆ φ): on each tree generator the convolution φ₋ ⋆ φ — written explicitly as
mul' ∘ (φ₋ ⊗ φ) ∘ comul (LinearMap.convMul_apply) — recovers the renormalized part φ₊.
Needs φ unital (φ 1 = 1), as characters are.
Proof route: comulAlgHomN (ofTree T) = comulTreeN T = ofTree T ⊗ 1 + Σ_{(cf,rem) ∈ cutSummandsN T} of' cf ⊗ ofTree rem. Pushing mul' ∘ map φ₋ φ through that sum (via
map_multiset_sum / TensorProduct.map_tmul / LinearMap.mul'_apply, with birkhoffMinus
on ofTree/of' from the AddMonoidAlgebra.lift) gives φ₋(ofTree T)·φ(1) + Σ φ₋(of' cf)· φ(ofTree rem) = birkhoffMinusTree T + birkhoffPrepTree T, which is birkhoffPlusTree T by
birkhoffPlusTree_eq_prep_add_minus.
The R = id specialization recovers the Hopf antipode #
[MCB25] Prop. 3.1.7 builds φ₋ by the same cutSummandsN/depth
recursion as the Hopf antipode antipodeTreeN (the inductive antipode of §1.2), with two
substitutions: the character value φ (ofTree rem) in place of the canonical embedding
ofTree rem, and the Rota–Baxter −R in place of bare negation. Taking the trivial
regularization R = id (RotaBaxter.id, weight -1) together with the canonical character
φ = id (the identity H →ₗ[R] H, which fixes ofTree rem) collapses both substitutions, so
the Bogolyubov negative part of the identity character is exactly the antipode. This is the
algebraic content of the book's remark that the antipode "is like a group inverse": S = id⁻¹
in the convolution group, recovered here as the R = id Birkhoff counterterm.
R = id, φ = id recovers the antipode on a tree. The Bogolyubov negative part φ₋
(Prop. 3.1.7) of the identity character id : H →ₗ[R] H under the trivial weight--1
Rota–Baxter operator RotaBaxter.id coincides with the Hopf antipode antipodeTreeN.
R = id, φ = id recovers the antipode as an algebra hom. The forest-level Bogolyubov
negative part φ₋ of the identity character under RotaBaxter.id is the Hopf antipode
antipodeAlgHomN. Lifts birkhoffMinusTree_id_eq_antipodeTreeN through the shared
ConnesKreimer.lift.
The full Birkhoff factorization φ = (φ₋ ∘ S) ⋆ φ₊ (MCB Def. 3.1.5) #
[MCB25] Def. 3.1.5 calls φ = (φ₋ ∘ S) ⋆ φ₊ the Birkhoff factorization
of a character φ : H → R (S the antipode, ⋆ the convolution). The keystone above proves the
semiring-form φ₊ = φ₋ ⋆ φ (Def. 3.1.6) on generators; over a ring the two forms are equivalent,
because the antipode-composite φ₋ ∘ S is the convolution inverse of the character φ₋. We work in
the convolution monoid WithConv (H →ₐ[R] R) of characters. Per Rem. 3.1.4 the target R carries
no coproduct, so this is not mathlib's AlgHom.convGroup (which requires the target to be a
bialgebra) — the inverse of a single character is read off directly from the antipode law. The
factorization needs H to be a Hopf algebra, hence CharZero R and NoZeroDivisors R.
The convolution inverse of a character is character ∘ S. For a character
ψ : H →ₐ[R] R, the antipode-composite ψ ∘ S is its left convolution inverse in the
character monoid WithConv (H →ₐ[R] R). The one-character specialization of the antipode law
(AlgHom.antipode_id_cancel), transported along ψ by comp_convMul_distrib. Per Rem. 3.1.4
it needs only H Hopf and R a commutative algebra — R carries no coproduct.
The convolution φ₋ ⋆ φ on a tree generator is the renormalized value φ₊(T). Restates
the keystone birkhoffFactorization_ofTree as a value in the character monoid, for a character
φ : H →ₐ[R] R (unital via map_one).
The full Birkhoff factorization φ₊ = φ₋ ⋆ φ ([MCB25] Def. 3.1.6)
on all of H for a character φ : H →ₐ[R] R: the renormalized character φ₊ (the
multiplicative (1 − R)(φ̃)) is the convolution φ₋ ⋆ φ. Lifts the keystone (which holds on
generators for any linear φ) to all forests via the multiplicativity of a character.
The Birkhoff factorization φ = (φ₋ ∘ S) ⋆ φ₊ ([MCB25] Def. 3.1.5,
eq. (3.1.4)): every character φ : H →ₐ[R] R factors through its Bogolyubov counterterm φ₋
(via the antipode S) and renormalized part φ₊ = birkhoffPlus. The "meaningless" φ₋ and
"meaningful" φ₊ of [MCB25]'s syntax–semantics interface. Derived from
birkhoffPlus_eq_convMul (Def. 3.1.6 on all H) and the character-inverse law
antipodeComp_convMul_self, by associativity in the character monoid.