Documentation

BSeries.Series.Scaling

Grading scalings and integer rescalings of the exact flow #

The scaling c_q : τ ↦ q^{|τ|} τ of the forest algebra and the induced rescaling of characters (arXiv:2507.21006, Proposition 7.1(2)). The exact flow is invariant under substepping: the n-fold convolution power of the exact character is the time-n flow, and rescaling it back by 1/n recovers the exact character — the identity a_n = a of the paper.

source
noncomputable def BSeries.ForestAlgebra.scalingHom {R : Type u} [CommSemiring R] (c : R) :
HopfAlgebras.ForestAlgebra R →ₐ[R] HopfAlgebras.ForestAlgebra R

The grading scaling τ ↦ c^{|τ|} τ of the forest algebra (the map c_q of arXiv:2507.21006, Proposition 7.1).

Equations
Instances For
    source
    @[simp]
    theorem BSeries.ForestAlgebra.scalingHom_ofForest {R : Type u} [CommSemiring R] (c : R) (φ : HopfAlgebras.RootedForest) :
    (scalingHom c) (HopfAlgebras.ForestAlgebra.ofForest φ) = c ^ φ.order • HopfAlgebras.ForestAlgebra.ofForest φ
    source
    noncomputable def BSeries.ForestAlgebra.Character.scaling {R : Type u} [CommSemiring R] (c : R) (χ : HopfAlgebras.ForestAlgebra.Character R) :
    HopfAlgebras.ForestAlgebra.Character R

    Rescaling a character along the grading: (χ_c)(τ) = c^{|τ|} χ(τ).

    Equations
    Instances For
      source
      @[simp]
      theorem BSeries.ForestAlgebra.Character.scaling_evalForest {R : Type u} [CommSemiring R] (c : R) (χ : HopfAlgebras.ForestAlgebra.Character R) (φ : HopfAlgebras.RootedForest) :
      (scaling c χ).evalForest φ = c ^ φ.order * χ.evalForest φ
      source
      theorem BSeries.Series.convolutionPower_exact {R : Type u} [Field R] [CharZero R] (n : ℕ) :
      (HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter (exact R).toCharacter).convolutionPower n = HopfAlgebras.ForestAlgebra.LinearFunctional.ofCharacter (scaledExact ↑n).toCharacter

      The convolution powers of the exact flow are its time-n flows: a^{⋆n} = a(nh) (arXiv:2507.21006, Proposition 7.1(2), via the flow property).

      source
      theorem BSeries.Series.scaling_inv_toCharacter_scaledExact {R : Type u} [Field R] [CharZero R] {n : ℕ} (hn : n ≠ 0) :
      ForestAlgebra.Character.scaling (↑n)⁻¹ (scaledExact ↑n).toCharacter = (exact R).toCharacter

      The exact flow is invariant under substepping (a_n = a, arXiv:2507.21006, Proposition 7.1(2)): rescaling the time-n flow by 1/n recovers the exact character.