The Minimal-Yield character ϕt : H → Laurent series (MCB Prop. 3.5.3, Lemma 3.5.5) #

[MCB25] §3.5.2.2

The character ϕt of MCB Prop. 3.5.3 (eq. 3.5.6) as an algebra homomorphism from the Hopf algebra H = ConnesKreimer R (Nonplanar α) of nonplanar rooted forests to the Laurent-series ring, in the lean t-grading model: rather than coefficients in the full algebra DM of free Merge derivations (Def. 3.5.1), we record only the grading tᵟ. With δ = δα, the grading of the canonical construction L(F) → F is exactly α(F) = Forest.alpha F (the leaves carry α = 0), so

ϕt(F) = t^{α(F)}.

Since α(F) ≥ 0, ϕt lands entirely in the nonpolar subring DM[[t]] = (1 − R)·DM[t⁻¹][[t]] (MCB Lemma 3.5.5): R·ϕt(F) = 0 for every forest F. This is exactly why ϕt alone cannot detect Sideward Merge — the intermediate-derivation character ψt (Cor. 3.5.4) and the full Birkhoff factorization (Prop. 3.5.6) are needed to separate Internal/External from Sideward Merge.

Main definitions #

Minimalist.Merge.gradingChar: the algebra hom ϕt : H →ₐ[R] LaurentSeries R.

References #

[MCB25] (Prop. 3.5.3, eq. 3.5.6, Lemma 3.5.5)

`gradeMonomial` is a multiplicative grading #

source

@[simp]

theorem Minimalist.Merge.gradeMonomial_zero {R : Type u_2} [CommRing R] :

gradeMonomial 0 = 1

source

theorem Minimalist.Merge.gradeMonomial_mul {R : Type u_2} [CommRing R] (a b : ℤ) :

gradeMonomial a * gradeMonomial b = gradeMonomial (a + b)

tᵃ · tᵇ = tᵃ⁺ᵇ: the grading monomials multiply by adding exponents.

The character ϕt (MCB Prop. 3.5.3, `δα` grading) #

source

noncomputable def Minimalist.Merge.gradingMonomialTree {α : Type u_1} {R : Type u_2} [CommRing R] (T : RootedTree.Nonplanar α) :

LaurentSeries R

The per-tree value of ϕt: t^{α(T)} = t^{accCount T} (the δα grading of L(T) → T).

Equations

Minimalist.Merge.gradingMonomialTree T = Minimalist.Merge.gradeMonomial ↑T.accCount

Instances For

source

noncomputable def Minimalist.Merge.gradingMonoidHom {α : Type u_1} {R : Type u_2} [CommRing R] :

Multiplicative (RootedTree.Forest (RootedTree.Nonplanar α)) →* LaurentSeries R

ϕt extended multiplicatively to forests (ϕt(F ⊔ F') = ϕt(F)·ϕt(F')); mirrors antipodeMonoidHomN.

Equations

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

Instances For

source

noncomputable def Minimalist.Merge.gradingChar {α : Type u_1} {R : Type u_2} [CommRing R] :

RootedTree.ConnesKreimer R (RootedTree.Nonplanar α) →ₐ[R] LaurentSeries R

The Minimal-Yield character ϕt : H →ₐ[R] DM[t⁻¹][[t]] (MCB Prop. 3.5.3, eq. 3.5.6) in the lean t-grading model.

Equations

Minimalist.Merge.gradingChar = RootedTree.ConnesKreimer.lift Minimalist.Merge.gradingMonoidHom

Instances For

source

@[simp]

theorem Minimalist.Merge.gradingChar_apply_of' {α : Type u_1} {R : Type u_2} [CommRing R] (F : RootedTree.Forest (RootedTree.Nonplanar α)) :

gradingChar (RootedTree.ConnesKreimer.of' F) = (Multiset.map gradingMonomialTree F).prod

source

theorem Minimalist.Merge.prod_gradingMonomialTree {α : Type u_1} {R : Type u_2} [CommRing R] (F : RootedTree.Forest (RootedTree.Nonplanar α)) :

(Multiset.map gradingMonomialTree F).prod = gradeMonomial ↑(RootedTree.Forest.alpha F)

ϕt(F) = t^{α(F)}: the forest value is the single grading monomial at the accessible-term count (the product of per-tree monomials collapses since α is additive).

source

theorem Minimalist.Merge.gradingChar_apply_of'_eq {α : Type u_1} {R : Type u_2} [CommRing R] (F : RootedTree.Forest (RootedTree.Nonplanar α)) :

gradingChar (RootedTree.ConnesKreimer.of' F) = gradeMonomial ↑(RootedTree.Forest.alpha F)

source

@[simp]

theorem Minimalist.Merge.gradingChar_apply_ofTree {α : Type u_1} {R : Type u_2} [CommRing R] (T : RootedTree.Nonplanar α) :

gradingChar (RootedTree.ConnesKreimer.ofTree T) = gradeMonomial ↑T.accCount

MCB Lemma 3.5.5: ϕt is entirely nonpolar #

source

theorem Minimalist.Merge.polarHahn_gradingChar_of' {α : Type u_1} {R : Type u_2} [CommRing R] (F : RootedTree.Forest (RootedTree.Nonplanar α)) :

(gradingChar (RootedTree.ConnesKreimer.of' F)).polarHahn = 0

MCB Lemma 3.5.5: ϕt(F) always lies in the nonpolar subring — R·ϕt(F) = 0 — because the δα-grading α(F) ≥ 0. Hence ϕt cannot detect Sideward Merge (regardless of which Merge operations build F), motivating the intermediate-derivation character ψt.

source