n-th roots of characters

The general convolution roots of arXiv:2507.21006, Theorem 6.1: for every character ψ and n with n invertible, there is a normalized functional ρ with ρ^{⋆n} = ψ. The construction avoids iterated coproducts by a single recursion on the pair (forest order, convolution power): unrolling ρ^{⋆(k+1)} = ρ ⋆ ρ^{⋆k} through the boundary cuts gives

ρ^{⋆m}(φ) = m ρ(φ) + Σ_{k=2}^{m} Σ_{proper} ρ(P) ρ^{⋆(k-1)}(T),

so ρ(φ) is determined at level m = n by division, with all remaining data of strictly smaller order.

@[irreducible]

noncomputable def BSeries.RootedForest.rootData {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] : ℕ → HopfAlgebras.RootedForest → R

The joint data of an n-th root and its convolution powers: rootData ψ n k φ = ρ^{⋆k}(φ) for the n-th root ρ of ψ.

Equations

• One or more equations did not get rendered due to their size.
• BSeries.RootedForest.rootData ψ n 0 φ = if hφ : φ = 0 then 1 else 0

@[simp]

theorem BSeries.RootedForest.rootData_zero_forest {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (k : ℕ) : rootData ψ n k 0 = 1

theorem BSeries.RootedForest.rootData_zero_of_ne {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] {φ : HopfAlgebras.RootedForest} (hφ : φ ≠ 0) : rootData ψ n 0 φ = 0

theorem BSeries.RootedForest.rootData_one_of_ne {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] {φ : HopfAlgebras.RootedForest} (hφ : φ ≠ 0) : rootData ψ n 1 φ = ⅟↑n * (ψ.evalForest φ - ∑ j ∈ Finset.range (n - 1), (List.map (fun (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => rootData ψ n 1 term.1 * rootData ψ n (j + 1) term.2) φ.properCoproductTerms).sum)

theorem BSeries.RootedForest.rootData_succ_succ_of_ne {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (k : ℕ) {φ : HopfAlgebras.RootedForest} (hφ : φ ≠ 0) : rootData ψ n (k + 2) φ = rootData ψ n 1 φ + rootData ψ n (k + 1) φ + (List.map (fun (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => rootData ψ n 1 term.1 * rootData ψ n (k + 1) term.2) φ.properCoproductTerms).sum

theorem BSeries.RootedForest.rootData_eq_smul_add {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (m : ℕ) {φ : HopfAlgebras.RootedForest} (hφ : φ ≠ 0) : rootData ψ n (m + 1) φ = (m + 1) • rootData ψ n 1 φ + ∑ j ∈ Finset.range m, (List.map (fun (term : HopfAlgebras.RootedForest × HopfAlgebras.RootedForest) => rootData ψ n 1 term.1 * rootData ψ n (j + 1) term.2) φ.properCoproductTerms).sum

The unrolled power identity: ρ^{⋆m}(φ) = m ρ(φ) + Σ_{k=2}^{m} S_k(φ) on non-empty forests.

theorem BSeries.RootedForest.rootData_top {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (hn : n ≠ 0) {φ : HopfAlgebras.RootedForest} (hφ : φ ≠ 0) : rootData ψ n n φ = ψ.evalForest φ

The defining property of the n-th root data: at level n, the recursion inverts to ρ^{⋆n}(φ) = ψ(φ) (arXiv:2507.21006, Theorem 6.1, the recursion step).

noncomputable def BSeries.ForestAlgebra.Character.nthRootFunctional {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] : HopfAlgebras.ForestAlgebra.LinearFunctional R

The n-th root of a character, as a linear functional (arXiv:2507.21006, Theorem 6.1).

Equations

• BSeries.ForestAlgebra.Character.nthRootFunctional ψ n = Finsupp.linearCombination R (BSeries.RootedForest.rootData ψ n 1)

@[simp]

theorem BSeries.ForestAlgebra.Character.nthRootFunctional_ofForest {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (φ : HopfAlgebras.RootedForest) : (nthRootFunctional ψ n) (HopfAlgebras.ForestAlgebra.ofForest φ) = RootedForest.rootData ψ n 1 φ

theorem BSeries.ForestAlgebra.Character.evalForest_convolutionPower_nthRootFunctional {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (k : ℕ) (φ : HopfAlgebras.RootedForest) : ((nthRootFunctional ψ n).convolutionPower (k + 1)).evalForest φ = RootedForest.rootData ψ n (k + 1) φ

The convolution powers of the n-th root functional realize the joint root data.

theorem BSeries.ForestAlgebra.Character.convolutionPower_nthRootFunctional {R : Type u} [CommRing R] (ψ : HopfAlgebras.ForestAlgebra.Character R) (n : ℕ) [Invertible ↑n] (hn : n ≠ 0) : (nthRootFunctional ψ n).convolutionPower n = HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter ψ

Existence of n-th convolution roots (arXiv:2507.21006, Theorem 6.1): the n-th power of the root functional is the character.