Shuffle coproduct on ConnesKreimer R T

@cite{oudom-guin-2008} @cite{foissy-typed-decorated-rooted-trees-2018}

The shuffle coproduct Δ on ConnesKreimer R T = R[Multiset T] makes each tree-singleton of' {t} primitive: Δ(of' {t}) = of' {t} ⊗ 1 + 1 ⊗ of' {t}. Extended multiplicatively over the commutative disjoint-union product, this gives Δ(of' F) = Σ_{F₁ ⊆ F} of' F₁ ⊗ of' (F - F₁) for any forest F.

This is the polynomial-algebra coproduct viewing R[Multiset T] = SymAlg(R[T]) with each generator of T primitive. It is DIFFERENT from mathlib's AddMonoidAlgebra.instBialgebra (which gives the group-like coproduct Δ(of' F) = of' F ⊗ of' F).

The shuffle Δ is the substrate for Oudom-Guin 2004's algebraic construction of the Grossman-Larson product on S(L) for any pre-Lie algebra L (specialized here to L = InsertionAlgebra α and S(L) = ConnesKreimer R (Nonplanar α)).

File scope

• §1: comulShuffle definition + basis form.
• §2: counit-like behavior (comulShuffle 1).
• §3: algebra-hom property (comulShuffle (x · y) = comulShuffle x · comulShuffle y).
• §4: cocommutativity.
• §5: coassociativity.

Status

[UPSTREAM] candidate. Substrate scaffold; proofs in flight.

§1: comulShuffle — the polynomial coproduct

noncomputable def RootedTree.ConnesKreimer.comulShuffle {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] : ConnesKreimer R T →ₗ[R] TensorProduct R (ConnesKreimer R T) (ConnesKreimer R T)

The shuffle coproduct on ConnesKreimer R T. On the basis element of' F for F : Forest T = Multiset T, gives Σ_{F₁ ⊆ F} of' F₁ ⊗ of' (F - F₁) via the powerset of F.

Each tree-singleton of' {t} = ofTree t is primitive: Δ(of' {t}) = of' {t} ⊗ 1 + 1 ⊗ of' {t}.

Extends linearly via Finsupp.lsum to the full algebra.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.comulShuffle_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (F : Forest T) : comulShuffle (of' F) = (Multiset.map (fun (F₁ : Forest T) => of' F₁ ⊗ₜ[R] of' (F - F₁)) (Multiset.powerset F)).sum

§2: Counit-like behavior on 1 = of' 0

@[simp]

theorem RootedTree.ConnesKreimer.comulShuffle_one {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] : comulShuffle 1 = 1 ⊗ₜ[R] 1

comulShuffle 1 = 1 ⊗ 1. Reflects that 1 ∈ ConnesKreimer R T is a grouplike element (or equivalently, the empty forest's only sub-multiset partition is (0, 0)).

§3: Algebra-hom property — Δ is multiplicative

The shuffle Δ is an R-algebra hom from ConnesKreimer R T to ConnesKreimer R T ⊗[R] ConnesKreimer R T (where the target has the tensor-product algebra structure). Equivalently: Δ(of' (F + G)) = Δ(of' F) · Δ(of' G).

Combinatorially: (F+G).powerset = F.powerset.bind (fun F₁ => G.powerset.map (fun G₁ => F₁ + G₁)) (via the bijection that splits each sub-multiset of F+G into its F-part and G-part).

theorem Multiset.powerset_add {T : Type u_2} (F G : Multiset T) : (F + G).powerset = F.powerset.bind fun (F₁ : Multiset T) => map (fun (G₁ : Multiset T) => F₁ + G₁) G.powerset

Helper: Multiset.powerset distributes over +. For F G : Multiset T, (F + G).powerset = F.powerset.bind (fun F₁ => G.powerset.map (fun G₁ => F₁ + G₁)) as multisets. Proved by induction on F via Multiset.powerset_cons.

theorem Multiset.antidiagonal_add {α : Type u_3} [DecidableEq α] (F G : Multiset α) : (F + G).antidiagonal = F.antidiagonal.bind fun (p : Multiset α × Multiset α) => map (fun (q : Multiset α × Multiset α) => (p.1 + q.1, p.2 + q.2)) G.antidiagonal

Δ-multiplicativity at the antidiagonal level: the antidiagonal of a sum decomposes as the bind/map product of the per-summand antidiagonals.

In Oudom-Guin §2 / Sweedler notation this is the multiplicativity Δ(FG) = Δ(F) · Δ(G) for the symmetric algebra Hopf coproduct (the symmetric-algebra special case of Prop 2.7.iii / Prop 2.8.iii).

Proven by transport from powerset_add through antidiagonal_eq_map_powerset, closed by the multiset identity (F + G) - (F₁ + G₁) = (F - F₁) + (G - G₁) (tsub_add_tsub_comm) for F₁ ≤ F, G₁ ≤ G.

[UPSTREAM] candidate for Mathlib.Data.Multiset.Antidiagonal. Mathlib has the cons form (antidiagonal_cons) but not this + form.

theorem RootedTree.ConnesKreimer.comulShuffle_mul_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (F G : Forest T) : comulShuffle (of' F * of' G) = comulShuffle (of' F) * comulShuffle (of' G)

Basis form of the algebra-hom property: Δ(of' F · of' G) = Δ(of' F) · Δ(of' G).

Uses Multiset.powerset_add to relate (F + G).powerset to the bind of F.powerset and G.powerset, and tsub_add_tsub_comm to factor (F + G) - (F₁ + G₁) = (F - F₁) + (G - G₁) for F₁ ≤ F, G₁ ≤ G.

theorem RootedTree.ConnesKreimer.comulShuffle_mul {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (F G : ConnesKreimer R T) : comulShuffle (F * G) = comulShuffle F * comulShuffle G

The shuffle coproduct is an algebra hom on ConnesKreimer R T: Δ(F · G) = Δ(F) · Δ(G) in the tensor algebra ConnesKreimer R T ⊗[R] ConnesKreimer R T. Bilinear lift of comulShuffle_mul_of' via two nested Finsupp.addHom_ext reductions to basis singletons (mirrors assoc_symm in PreLie/Basic.lean).

§4: Cocommutativity

The shuffle Δ is cocommutative: swapping the two tensor factors leaves Δ unchanged. This follows from the involution F₁ ↦ F - F₁ on F.powerset.

theorem Multiset.antidiagonal_swap {α : Type u_3} (s : Multiset α) : map Prod.swap s.antidiagonal = s.antidiagonal

Δ-cocommutativity at the antidiagonal level: s.antidiagonal is invariant under Prod.swap. Pairs (s₁, s₂) with s₁ + s₂ = s map bijectively to (s₂, s₁) with the same constraint, since + is commutative.

In Oudom-Guin §2 / Sweedler notation this is the cocommutativity (swap ∘ Δ) = Δ for the symmetric algebra coproduct.

Mathlib has the analogue Multiset.Nat.antidiagonal_map_swap for Nat antidiagonal but not (as of mathlib 4.30) for the general Multiset.antidiagonal. [UPSTREAM] candidate for Mathlib.Data.Multiset.Antidiagonal.

theorem Multiset.powerset_partition_swap {β : Type u_3} [AddCommMonoid β] {T' : Type u_4} [DecidableEq T'] (C : Multiset T') (f : Multiset T' → Multiset T' → β) : (map (fun (C₁ : Multiset T') => f C₁ (C - C₁)) C.powerset).sum = (map (fun (C₁ : Multiset T') => f (C - C₁) C₁) C.powerset).sum

Reindex a partition-sum over C.powerset using the involution C₁ ↦ C - C₁. Specialisation of antidiagonal_swap to a (C₁, C - C₁) parametrisation: summing f C₁ (C - C₁) over partitions equals summing f (C - C₁) C₁.

In Oudom-Guin terms: this is the basis-level statement that the symmetric Hopf coproduct's tensor-flip leaves a sum-with-f invariant. Used in cocommutativity proofs and Oudom-Guin Lemma 2.10's chain.

theorem RootedTree.ConnesKreimer.comulShuffle_comm_multiset {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (F : Forest T) : (Multiset.map (fun (F₁ : Forest T) => of' F₁ ⊗ₜ[R] of' (F - F₁)) (Multiset.powerset F)).sum = (Multiset.map (fun (F₁ : Forest T) => of' (F - F₁) ⊗ₜ[R] of' F₁) (Multiset.powerset F)).sum

Basis-level cocommutativity: the partition sum is invariant under tensor swap. Direct corollary of Multiset.powerset_partition_swap.

theorem RootedTree.ConnesKreimer.comulShuffle_comm {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] : ↑(TensorProduct.comm R (ConnesKreimer R T) (ConnesKreimer R T)) ∘ₗ comulShuffle = comulShuffle

Cocommutativity of comulShuffle: swap ∘ Δ = Δ where swap is the tensor-product flip. Lifted from basis form comulShuffle_comm_multiset via single-variable Finsupp.addHom_ext reduction.

§5: Coassociativity

(Δ ⊗ id) ∘ Δ = (id ⊗ Δ) ∘ Δ. Combinatorially: summing over partitions of F into 3 pieces (via nested powerset) gives the same result whether you split the first or the second piece in the inner step.

Stated below pointwise on basis elements (avoiding tensor-LinearMap typeclass synthesis hazards). The full LinearMap form follows by linearity.

theorem Multiset.powerset_powerset_pair_swap {α : Type u_3} [DecidableEq α] (F : Multiset α) : (F.powerset.bind fun (F₁ : Multiset α) => map (fun (A : Multiset α) => (A, F₁ - A)) F₁.powerset) = F.powerset.bind fun (A : Multiset α) => map (fun (B : Multiset α) => (A, B)) (F - A).powerset

Substrate: nested-powerset reparameterization. The two iteration orders over (F₁, F₁_a) with F₁_a ⊆ F₁ ⊆ F vs (G₁, G₂_a) with G₁ ⊆ F, G₂_a ⊆ F - G₁ enumerate the same multiset of pairs, where the bijection is (F₁, F₁_a) ↦ (G₁ = F₁_a, G₂_a = F₁ - F₁_a).

[UPSTREAM] candidate.

theorem RootedTree.ConnesKreimer.comulShuffle_coassoc_basis {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (F : Forest T) : (Multiset.map (fun (F₁ : Forest T) => (Multiset.map (fun (F₁_a : Forest T) => of' F₁_a ⊗ₜ[R] of' (F₁ - F₁_a) ⊗ₜ[R] of' (F - F₁)) (Multiset.powerset F₁)).sum) (Multiset.powerset F)).sum = (Multiset.map (fun (G₁ : Forest T) => (Multiset.map (fun (G₂_a : Forest T) => of' G₁ ⊗ₜ[R] of' G₂_a ⊗ₜ[R] of' (F - G₁ - G₂_a)) (Multiset.powerset (F - G₁))).sum) (Multiset.powerset F)).sum

Coassociativity on basis: applied to of' F, summing over double partitions gives the same triple tensor whether we partition the left or right side first.

Σ_{F₁ + F₂ = F, F₁_a + F₁_b = F₁} of' F₁_a ⊗ of' F₁_b ⊗ of' F₂ = Σ_{G₁ + G₂ = F, G₂_a + G₂_b = G₂} of' G₁ ⊗ of' G₂_a ⊗ of' G₂_b

Both equal Σ_{F_a + F_b + F_c = F} of' F_a ⊗ of' F_b ⊗ of' F_c. Direct corollary of Multiset.powerset_powerset_pair_swap.

§6: Coalgebra and Bialgebra structure on ConnesKreimer R T

With Δ = comulShuffle and ε = counit (extracts coefficient of empty forest), ConnesKreimer R T becomes a coalgebra and a bialgebra over R. The shuffle Δ is cocommutative (comulShuffle_comm) but the bialgebra laws are independent of cocommutativity.

theorem RootedTree.ConnesKreimer.comulShuffle_coassoc {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] : ↑(TensorProduct.assoc R (ConnesKreimer R T) (ConnesKreimer R T) (ConnesKreimer R T)) ∘ₗ LinearMap.rTensor (ConnesKreimer R T) comulShuffle ∘ₗ comulShuffle = LinearMap.lTensor (ConnesKreimer R T) comulShuffle ∘ₗ comulShuffle

LinearMap form of comulShuffle coassociativity, as required by the Coalgebra typeclass: (Δ ⊗ id) ∘ Δ = (id ⊗ Δ) ∘ Δ (up to associator). Lifted from basis form comulShuffle_coassoc_basis via single-variable Finsupp.addHom_ext reduction; the powerset sum is pushed through assoc/rTensor/lTensor via AddMonoidHom.map_multiset_sum.