Lax Lean Archive

Coproduct and shuffle identities

Lax825748.ShuffleIdentities · concepts/Lax825748/ShuffleIdentities.lean · lax-825748

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Lemmas 1–5. The pp-fold coproduct assigns each position of a word to one of pp tensor factors. Tensor polynomials are represented by finite linear combinations of pp-tuples of words. Its value on a letter is the sum of the pp placements of that letter, and Lie polynomials are primitive.

    Pairing with this coproduct computes the shuffle product. Letter residuals are derivations. A shuffle product of ii zero-constant series vanishes on a product of fewer than ii Lie polynomials. For equal numbers of factors, the pairing is the sum over permutations of pairwise evaluations.

    For normalized coordinate series, equal-degree monomials have diagonal pairing I!=∏iIi!I!=\prod_i I_i! and off-diagonal pairing zero. This corrects the printed ∣I∣!|I|! in Lemma 5(ii).

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.
    Evidence

    This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

    1 coproduct_multiplicative proven

    2 lie_primitive proven

    3 pairing_coproduct proven

    4 permutation_pairing proven

    5 residual_derivation proven

    6 triangular_pairing proven

    7 vanishing proven

    In the paper

    • page 5 of this submission's paper

    Lean source view on GitHub

    1import Lax825748.Shuffle
    2import Lax825748.LieRank
    3import Lax825748.Monomials
    4import Mathlib.Data.Fintype.Perm
    5
    6/-!
    7---
    8title: Coproduct and shuffle identities
    9type: theorem
    10---
    11Lemmas 1–5. The pp-fold coproduct assigns each position of a word to one
    12of pp tensor factors. Tensor polynomials are represented by finite linear
    13combinations of pp-tuples of words. Its value on a letter is the sum of the
    14pp placements of that letter, and Lie polynomials are primitive.
    15
    16Pairing with this coproduct computes the shuffle product. Letter residuals
    17are derivations. A shuffle product of ii zero-constant series vanishes on
    18a product of fewer than ii Lie polynomials. For equal numbers of factors,
    19the pairing is the sum over permutations of pairwise evaluations.
    20
    21For normalized coordinate series, equal-degree monomials have diagonal
    22pairing I!=∏iIi!I!=\prod_i I_i! and off-diagonal pairing zero. This corrects
    23the printed ∣I∣!|I|! in Lemma 5(ii).
    24-/
    25
    26noncomputable section
    27
    28namespace Lax825748.ShuffleIdentities
    29
    30open Series Shuffle LieRank Monomials
    31open scoped BigOperators
    32
    33abbrev TensorPolynomial (X : Type) (p : ℕ) :=
    34 MonoidAlgebra ℝ (Fin p → Word X)
    35
    36def distributions {X : Type} (p : ℕ) : List X → List (Fin p → List X)
    37 | [] => [fun _ => []]
    38 | x :: w => (distributions p w).flatMap fun v =>
    39 List.ofFn fun i : Fin p => Function.update v i (x :: v i)
    40
    41noncomputable def coproduct {X : Type} (p : ℕ) (P : NCPolynomial X) :
    42 TensorPolynomial X p :=
    43 P.coeff.sum fun w a => ((distributions p w.toList).map fun v =>
    44 MonoidAlgebra.single (fun i => FreeMonoid.ofList (v i)) a).sum
    45
    46noncomputable def tensorPairing {X : Type} {p : ℕ} (S : Fin p → NCSeries X)
    47 (P : TensorPolynomial X p) : ℝ :=
    48 P.coeff.sum fun v a => a * ∏ i, S i (v i)
    49
    50noncomputable def insertFactor {X : Type} {p : ℕ} (i : Fin p)
    51 (P : NCPolynomial X) : TensorPolynomial X p :=
    52 P.coeff.sum fun w a => MonoidAlgebra.single (fun j => if j = i then w else 1) a
    53
    54axiom coproduct_multiplicative {X : Type} (p : ℕ) (P Q : NCPolynomial X) :
    55 coproduct p (P * Q) = coproduct p P * coproduct p Q
    56
    57axiom pairing_coproduct {X : Type} {p : ℕ} (S : Fin p → NCSeries X)
    58 (P : NCPolynomial X) :
    59 pairing (shuffleList (List.ofFn S)) P = tensorPairing S (coproduct p P)
    60
    61axiom lie_primitive {X : Type} (p : ℕ) (P : LiePolynomial X) :
    62 coproduct p P.val = ∑ i : Fin p, insertFactor i P.val
    63
    64axiom residual_derivation {X : Type} (x : X) (S T : NCSeries X) :
    65 rightResidual (shuffle S T) (letter x) =
    66 shuffle (rightResidual S (letter x)) T + shuffle S (rightResidual T (letter x))
    67
    68axiom vanishing {X : Type} {i j : ℕ} (hji : j < i)
    69 (T : Fin i → NCSeries X) (hT : ∀ k, T k 1 = 0)
    70 (Q : Fin j → LiePolynomial X) :
    71 pairing (shuffleList (List.ofFn T)) ((List.ofFn fun k => (Q k).val).prod) = 0
    72
    73axiom permutation_pairing {X : Type} {n : ℕ}
    74 (T : Fin n → NCSeries X) (hT : ∀ k, T k 1 = 0)
    75 (Q : Fin n → LiePolynomial X) :
    76 pairing (shuffleList (List.ofFn T)) ((List.ofFn fun k => (Q k).val).prod) =
    77 ∑ σ : Equiv.Perm (Fin n), ∏ k, pairing (T k) (Q (σ k)).val
    78
    79noncomputable def shuffleMonomial {X : Type} {d : ℕ} (S : Fin d → NCSeries X)
    80 (I : Fin d → ℕ) : NCSeries X :=
    81 shuffleList (List.ofFn fun i => shufflePow (S i) (I i))
    82
    83axiom triangular_pairing {X : Type} {d : ℕ} (S : Fin d → NCSeries X)
    84 (P : Fin d → LiePolynomial X) (hS : ∀ i, S i 1 = 0)
    85 (hSP : ∀ i j, pairing (S i) (P j).val = if i = j then 1 else 0)
    86 (I J : Fin d → ℕ) :
    87 (totalDegree J < totalDegree I →
    88 pairing (shuffleMonomial S I) (orderedPowers (fun i => (P i).val) J) = 0) ∧
    89 (totalDegree I = totalDegree J →
    90 pairing (shuffleMonomial S I) (orderedPowers (fun i => (P i).val) J) =
    91 if I = J then (multiFactorial I : ℝ) else 0)
    92
    93end Lax825748.ShuffleIdentities
    94
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…