Documentation

Linglib.Core.Algebra.RootedTree.BirkhoffFactorizationSemiring

Semiring Birkhoff factorization on the Connes–Kreimer Hopf algebra [UPSTREAM] #

The semiring form of [MCB25]'s renormalization (Def. 3.1.2, Prop. 3.1.9): the linguistically operative case, where the target is a commutative semiring whose addition is not invertible — tropical (ℝ ∪ {−∞}, max, +), Viterbi, and Boolean parsing semirings (§3.5, "Birkhoff Factorization and (Semi)ring Parsing"; §3.5.2, "Minimal Yield as Birkhoff Factorization").

The Hopf algebra H = ConnesKreimer R (Nonplanar α) of nonplanar rooted forests is unchanged (base R only a commutative semiring — the antipode-free factorization needs no negation, so this works over R = ℕ, the base for a Boolean-semiring target), so the entire coproduct/cut infrastructure is reused. Only the character target is a semiring, with a weight-+1 RotaBaxterSemiring operator R. The Bogolyubov recursion (Prop. 3.1.9, eq. (3.1.7)) reads

φ̃(x) = φ(x) ⊡ Σ φ₋(x′) ⊙ φ(x″), φ₋(x) = R(φ̃(x)), φ₊(x) = φ₋(x) ⊡ φ̃(x),

with ⊡, ⊙ the semiring addition/multiplication and R the positive projection (contrast the ring case φ₋ = −R(φ̃), φ₊ = (1−R)(φ̃)). Because a semiring has no antipode, only the form φ₊ = φ₋ ⋆ φ (Def. 3.1.6) is available — there is no φ = (φ₋ ∘ S) ⋆ φ₊ (Def. 3.1.5).

Main definitions #

Main results #

References #

[MCB25] (Def. 3.1.2, Def. 3.1.6, Prop. 3.1.9, Rem. 3.1.10)

@[irreducible]
noncomputable def RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinusTree {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :

The Bogolyubov negative part φ₋ on a single tree (semiring, weight +1; [MCB25] Prop. 3.1.9): φ₋(T) = R(Σ_{(cf,rem) ∈ cutSummandsN T} (Π_{Tᵢ ∈ cf} φ₋(Tᵢ)) · φ(ofTree rem)). The semiring analogue of the ring birkhoffMinusTree, with the positive projection R in place of −R; well-founded on T.depth.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinusMonoidHom {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) :
    Multiplicative (Forest (Nonplanar α)) →*

    φ₋ extended multiplicatively to forests, as a MonoidHom. Mirrors the ring birkhoffMinusMonoidHom.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinus {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) :
      ConnesKreimer R (Nonplanar α) →ₐ[R]

      φ₋ as an algebra hom H →ₐ[R] ℛ, lifting birkhoffMinusMonoidHom. Mirrors the ring birkhoffMinus.

      Equations
      Instances For
        @[simp]
        theorem RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinus_apply_of' {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (F : Forest (Nonplanar α)) :
        (birkhoffMinus φ RB) (of' F) = (Multiset.map (birkhoffMinusTree φ RB) F).prod
        @[simp]
        theorem RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinus_apply_ofTree {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :
        (birkhoffMinus φ RB) (ofTree T) = birkhoffMinusTree φ RB T
        noncomputable def RootedTree.ConnesKreimer.SemiringRenorm.birkhoffPrepTree {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :

        The Bogolyubov preparation φ̃ ([MCB25] Prop. 3.1.9): φ̃(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) = φ̃(T) + φ₋(T).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          theorem RootedTree.ConnesKreimer.SemiringRenorm.birkhoffPrepTree_unfold {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :
          birkhoffPrepTree φ RB T = (Multiset.map (fun (p : Forest (Nonplanar α) × Nonplanar α) => (Multiset.map (birkhoffMinusTree φ RB) p.1).prod * φ (ofTree p.2)) (cutSummandsN T)).sum

          The Bogolyubov preparation in non-attach-decorated form. Mirrors the ring birkhoffPrepTree_unfold.

          theorem RootedTree.ConnesKreimer.SemiringRenorm.birkhoffMinusTree_eq_op_prep {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :
          birkhoffMinusTree φ RB T = RB.op (birkhoffPrepTree φ RB T)

          φ₋(T) = R(φ̃(T)): the negative part is the positive projection R of the preparation.

          noncomputable def RootedTree.ConnesKreimer.SemiringRenorm.birkhoffPlusTree {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) (T : Nonplanar α) :

          The renormalized part φ₊ on a single tree ([MCB25] Prop. 3.1.9): φ₊(T) = φ̃(T) + φ₋(T) (the semiring φ₋ ⊡ φ̃) — the consistency-checked value.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem RootedTree.ConnesKreimer.SemiringRenorm.birkhoffFactorization_ofTree {R : Type u_1} { : Type u_2} [CommSemiring R] [CommSemiring ] [Algebra R ] {α : Type u_3} (φ : ConnesKreimer R (Nonplanar α) →ₗ[R] ) (RB : RotaBaxterSemiring ) ( : φ 1 = 1) (T : Nonplanar α) :
            (LinearMap.mul' R ) ((TensorProduct.map (birkhoffMinus φ RB).toLinearMap φ) (comulAlgHomN (ofTree T))) = birkhoffPlusTree φ RB T

            Semiring Birkhoff factorization on generators ([MCB25] Def. 3.1.6, Prop. 3.1.9 eq. (3.1.7), φ₊ = φ₋ ⋆ φ): on each tree generator the convolution φ₋ ⋆ φmul' ∘ (φ₋ ⊗ φ) ∘ comul — recovers the renormalized part φ₊. Needs φ unital (φ 1 = 1). Same proof as the ring keystone (the identity is pure coproduct bookkeeping, sign-agnostic).