Birkhoff factorization of Connes–Kreimer characters

Let φ : H → ℛ be a linear map from the Connes–Kreimer algebra of rooted forests into a commutative algebra and P an additive operator on ℛ. The Bogolyubov recursion over the cuts (F, T') of a tree defines the preparation φ̃(T) = Σ (Π_{t ∈ F} φ₋(t)) · φ(T'), the negative part φ₋(T) = P (φ̃(T)) and the renormalized part φ₊(T) = φ̃(T) + φ₋(T), each extended multiplicatively to forests. Connes and Kreimer's construction over a ring, with a Rota–Baxter operator R of weight -1, is the case P = -R, where φ₋ = -R(φ̃) and φ₊ = (1 - R)(φ̃); over a semiring, as in Marcolli and Tedeschi, P is itself the operator, of weight +1. Either way P has weight +1.

For a unital φ, φ₊ = φ₋ ⋆ φ holds on trees for every P, and on all of H when φ is a character. The Rota–Baxter identity puts the two parts in subalgebras: if P has weight +1, then φ₋ sends every nonempty forest into the range of P and φ₊ into the range of id + P. At P = -id the renormalized part vanishes on trees, so φ₋ is a left convolution inverse of φ; at φ = id this is the antipode ConnesKreimer.antipodeAlgHomN, which turns φ₊ = φ₋ ⋆ φ into the factorization φ = (φ₋ ∘ S) ⋆ φ₊ (ConnesKreimer.birkhoffFactorization).

Main definitions

• ConnesKreimer.birkhoffMinus: the negative part φ₋.
• ConnesKreimer.birkhoffPrepTree: the Bogolyubov preparation φ̃ on a tree.
• ConnesKreimer.birkhoffPlus: the renormalized part φ₊.

Main results

• ConnesKreimer.convMul_birkhoffMinus_apply_ofTree, ConnesKreimer.birkhoffPlus_eq_convMul: φ₊ = φ₋ ⋆ φ, on trees and for characters.
• ConnesKreimer.birkhoffMinus_of'_mem_range, ConnesKreimer.birkhoffPlus_of'_mem_range: for P of weight +1, the two parts land in the ranges of P and of id + P.
• ConnesKreimer.birkhoffPlus_eq_self: a character that P kills on every tree is its own renormalized part.
• ConnesKreimer.birkhoffMinus_neg_id_convMul: at P = -id, φ₋ ⋆ φ = 1.

Implementation notes

The weight of P is stated in ℕ, which acts canonically on every semiring. On Laurent series the base ring also acts through HahnSeries.powerSeriesAlgebra, an action not definitionally equal to the coefficientwise one.

References

• [CK00]
• [EFGK04]
• [MT15]

@[irreducible]

noncomputable def ConnesKreimer.birkhoffMinusTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : ℛ

The negative part on a tree, φ₋(T) = P (Σ_{(F, T') ∈ cutSummandsN T} (Π_{t ∈ F} φ₋(t)) · φ(T')), by recursion on the number of vertices.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ConnesKreimer.birkhoffMinus {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) : ConnesKreimer R (UnorderedTree α) →ₐ[R] ℛ

The negative part φ₋, the multiplicative extension of birkhoffMinusTree to forests.

Equations

• ConnesKreimer.birkhoffMinus φ P = ConnesKreimer.aeval (ConnesKreimer.birkhoffMinusTree φ P)

@[simp]

theorem ConnesKreimer.birkhoffMinus_apply_of' {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (F : UnorderedTree.Forest (UnorderedTree α)) : (birkhoffMinus φ P) (of' F) = (Multiset.map (birkhoffMinusTree φ P) F).prod

@[simp]

theorem ConnesKreimer.birkhoffMinus_apply_ofTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : (birkhoffMinus φ P) (ofTree T) = birkhoffMinusTree φ P T

noncomputable def ConnesKreimer.birkhoffPrepTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : ℛ

The Bogolyubov preparation on a tree, φ̃(T) = Σ_{(F, T') ∈ cutSummandsN T} (Π_{t ∈ F} φ₋(t)) · φ(T').

Equations

• One or more equations did not get rendered due to their size.

theorem ConnesKreimer.birkhoffMinusTree_eq {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : birkhoffMinusTree φ P T = P (birkhoffPrepTree φ P T)

noncomputable def ConnesKreimer.birkhoffPlusTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : ℛ

The renormalized part on a tree, φ₊(T) = φ̃(T) + φ₋(T).

Equations

• ConnesKreimer.birkhoffPlusTree φ P T = ConnesKreimer.birkhoffPrepTree φ P T + ConnesKreimer.birkhoffMinusTree φ P T

noncomputable def ConnesKreimer.birkhoffPlus {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) : ConnesKreimer R (UnorderedTree α) →ₐ[R] ℛ

The renormalized part φ₊, the multiplicative extension of birkhoffPlusTree to forests.

Equations

• ConnesKreimer.birkhoffPlus φ P = ConnesKreimer.aeval (ConnesKreimer.birkhoffPlusTree φ P)

@[simp]

theorem ConnesKreimer.birkhoffPlus_apply_of' {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (F : UnorderedTree.Forest (UnorderedTree α)) : (birkhoffPlus φ P) (of' F) = (Multiset.map (birkhoffPlusTree φ P) F).prod

@[simp]

theorem ConnesKreimer.birkhoffPlus_apply_ofTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (T : UnorderedTree α) : (birkhoffPlus φ P) (ofTree T) = birkhoffPlusTree φ P T

The factorization φ₊ = φ₋ ⋆ φ

theorem ConnesKreimer.convMul_birkhoffMinus_apply_ofTree {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (P : ℛ →+ ℛ) (hφ : φ 1 = 1) (T : UnorderedTree α) : (WithConv.toConv (birkhoffMinus φ P).toLinearMap * WithConv.toConv φ).ofConv (ofTree T) = birkhoffPlusTree φ P T

For a unital φ, φ₊ = φ₋ ⋆ φ on trees, since the term T ⊗ 1 of the coproduct contributes φ₋(T) and the cuts contribute the preparation φ̃(T).

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

φ₊ = φ₋ ⋆ φ for a character φ, both sides being characters that agree on trees.

The subalgebras of the factorization

theorem ConnesKreimer.birkhoffMinus_of'_mem_range {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} {φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ} {P : ℛ →+ ℛ} (hP : IsRotaBaxter 1 ⇑P) {F : UnorderedTree.Forest (UnorderedTree α)} (hF : F ≠ 0) : (birkhoffMinus φ P) (of' F) ∈ Set.range ⇑P

For P of weight +1, the negative part sends every nonempty forest into the range of P.

theorem ConnesKreimer.birkhoffPlus_of'_mem_range {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} {φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ} {P : ℛ →+ ℛ} (hP : IsRotaBaxter 1 ⇑P) {F : UnorderedTree.Forest (UnorderedTree α)} (hF : F ≠ 0) : (birkhoffPlus φ P) (of' F) ∈ Set.range fun (x : ℛ) => x + P x

For P of weight +1, the renormalized part sends every nonempty forest into the range of id + P.

theorem ConnesKreimer.birkhoffMinusTree_eq_zero {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} {φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ} {P : ℛ →+ ℛ} (h : ∀ (T : UnorderedTree α), P (φ (ofTree T)) = 0) (T : UnorderedTree α) : birkhoffMinusTree φ P T = 0

If P kills φ on every tree, the negative part vanishes: the empty cut contributes P (φ T) = 0, and every other cut has a crown tree, where φ₋ vanishes by recursion.

theorem ConnesKreimer.birkhoffPlusTree_eq_of_forall {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} {φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ} {P : ℛ →+ ℛ} (h : ∀ (T : UnorderedTree α), P (φ (ofTree T)) = 0) (T : UnorderedTree α) : birkhoffPlusTree φ P T = φ (ofTree T)

If P kills φ on every tree, the renormalized part on a tree is the value of φ.

theorem ConnesKreimer.birkhoffPlus_eq_self {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommSemiring ℛ] [Algebra R ℛ] {α : Type u_3} {P : ℛ →+ ℛ} {φ : ConnesKreimer R (UnorderedTree α) →ₐ[R] ℛ} (h : ∀ (T : UnorderedTree α), P (φ (ofTree T)) = 0) : birkhoffPlus φ.toLinearMap P = φ

A character that P kills on every tree is its own renormalized part.

The operator -id

theorem ConnesKreimer.birkhoffPlusTree_neg_id {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommRing ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₗ[R] ℛ) (T : UnorderedTree α) : birkhoffPlusTree φ (-AddMonoidHom.id ℛ) T = 0

At P = -id the renormalized part vanishes on every tree, φ₊(T) = φ̃(T) - φ̃(T).

theorem ConnesKreimer.birkhoffMinus_neg_id_convMul {R : Type u_1} {ℛ : Type u_2} [CommSemiring R] [CommRing ℛ] [Algebra R ℛ] {α : Type u_3} (φ : ConnesKreimer R (UnorderedTree α) →ₐ[R] ℛ) : WithConv.toConv (birkhoffMinus φ.toLinearMap (-AddMonoidHom.id ℛ)) * WithConv.toConv φ = 1

At P = -id the negative part of a character is its left convolution inverse.