The Grossman–Larson product

This file defines the Grossman–Larson product on the free module of forests of nonplanar rooted trees. The product F ⋆ G sums, over the splits G = G₁ + G₂, the forests obtained by grafting the trees of G₂ onto vertices of F in all ways, with the trees of G₁ placed alongside. Grossman and Larson introduce the product; the closed form used here is Foissy's Theorem 5.1, through the Guin–Oudom extension of the grafting product.

The module of forests is ConnesKreimer R (UnorderedTree α), which Oudom and Guin read as the symmetric algebra on the trees: its own product is the disjoint union of forests. The insertion x ∘ y and the product x ⋆ y are bilinear maps on it, and the algebra GrossmanLarson R α is that module with ⋆ as its multiplication.

Main definitions

• UnorderedTree.productMultiset F G: the forests in the product F ⋆ G, with multiplicity.
• GrossmanLarson.insertion: the Guin–Oudom extension x ∘ y of the grafting product, grafting every tree of y onto a vertex of x.
• GrossmanLarson.product: the Grossman–Larson product x ⋆ y.
• GrossmanLarson R α: the forests with the product ⋆.
• GrossmanLarson.ι: the pre-Lie algebra of trees as the one-tree forests.

Main results

• GrossmanLarson.insertion_one_left, GrossmanLarson.insertion_of'_add, GrossmanLarson.counit_insertion: Oudom and Guin's rules 1 ∘ x = ε(x), AB ∘ C = Σ (A ∘ C₍₁₎)(B ∘ C₍₂₎) and ε(x ∘ y) = ε(x) ε(y), on basis forests for the second.
• GrossmanLarson.product_of': x ⋆ G = Σ_{G = G₁ + G₂} (x ∘ G₂) G₁.
• GrossmanLarson.counit_product: the counit is multiplicative for ⋆.
• GrossmanLarson.instNonAssocSemiring: the empty forest is a two-sided unit; associativity and the Semiring and Algebra instances are in GrossmanLarson/Algebra.lean.
• GrossmanLarson.toConnesKreimer_ι_mul, GrossmanLarson.toConnesKreimer_ι_mul_ι: on one-tree forests, ∘ is the grafting product and x ⋆ y = x y + x ∘ y.

Implementation notes

GrossmanLarson R α is a one-field structure over the Connes–Kreimer module, as WithConv is over a module of linear maps: the forests already carry the disjoint-union product, and the structure keeps the two multiplications on different types. insertion and product are stated on the underlying module, where the disjoint-union product is available to state their rules.

The insertion x ∘ y grafts every tree of y onto the original x. It is not iterated one-tree insertion, which would also graft later trees onto earlier ones.

References

• [GL89]
• [OG08]
• [Foi21]

Insertion and the product on the module of forests

noncomputable def GrossmanLarson.insertion {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α)

The Guin–Oudom extension x ∘ y of the grafting product sums, on basis forests, the graftings of every tree of G onto a vertex of F.

Equations

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

@[simp]

theorem GrossmanLarson.insertion_of'_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : UnorderedTree.Forest (UnorderedTree α)) : (insertion (ConnesKreimer.of' F)) (ConnesKreimer.of' G) = (Multiset.map ConnesKreimer.of' (UnorderedTree.insertionMultiset F G)).sum

@[simp]

theorem GrossmanLarson.insertion_one_right {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : (insertion x) 1 = x

Inserting no trees leaves the host unchanged.

theorem GrossmanLarson.insertion_one_left {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : (insertion 1) x = ConnesKreimer.counit x • 1

The empty forest has no vertices to graft onto: 1 ∘ x = ε(x).

@[simp]

theorem GrossmanLarson.insertion_ofTree_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T S : UnorderedTree α) : (insertion (ConnesKreimer.ofTree T)) (ConnesKreimer.ofTree S) = (Multiset.map ConnesKreimer.ofTree (T.insertSum S)).sum

On two trees the insertion is the grafting product.

theorem GrossmanLarson.insertion_of'_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (A B C : UnorderedTree.Forest (UnorderedTree α)) : (insertion (ConnesKreimer.of' (A + B))) (ConnesKreimer.of' C) = (Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (insertion (ConnesKreimer.of' A)) (ConnesKreimer.of' p.1) * (insertion (ConnesKreimer.of' B)) (ConnesKreimer.of' p.2)) (Multiset.antidiagonal C)).sum

Grafting into a disjoint union splits the guests between the two parts: AB ∘ C = Σ (A ∘ C₍₁₎)(B ∘ C₍₂₎).

theorem GrossmanLarson.counit_insertion {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ConnesKreimer R (UnorderedTree α)) : ConnesKreimer.counit ((insertion x) y) = ConnesKreimer.counit x * ConnesKreimer.counit y

The counit is multiplicative for the insertion.

noncomputable def GrossmanLarson.product {R : Type u_1} [CommSemiring R] {α : Type u_2} : ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α) →ₗ[R] ConnesKreimer R (UnorderedTree α)

The Grossman–Larson product x ⋆ y, on basis forests the sum over productMultiset.

Equations

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

@[simp]

theorem GrossmanLarson.product_of'_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : UnorderedTree.Forest (UnorderedTree α)) : (product (ConnesKreimer.of' F)) (ConnesKreimer.of' G) = (Multiset.map ConnesKreimer.of' (UnorderedTree.productMultiset F G)).sum

theorem GrossmanLarson.product_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) (G : UnorderedTree.Forest (UnorderedTree α)) : (product x) (ConnesKreimer.of' G) = (Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => (insertion x) (ConnesKreimer.of' p.2) * ConnesKreimer.of' p.1) (Multiset.antidiagonal G)).sum

x ⋆ G = Σ_{G = G₁ + G₂} (x ∘ G₂) G₁, the product of Oudom and Guin on a basis forest G.

theorem GrossmanLarson.product_one_right {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : (product x) 1 = x

theorem GrossmanLarson.product_one_left {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : (product 1) x = x

theorem GrossmanLarson.counit_product {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ConnesKreimer R (UnorderedTree α)) : ConnesKreimer.counit ((product x) y) = ConnesKreimer.counit x * ConnesKreimer.counit y

The counit is multiplicative for the Grossman–Larson product.

theorem GrossmanLarson.product_ofTree_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (T S : UnorderedTree α) : (product (ConnesKreimer.ofTree T)) (ConnesKreimer.ofTree S) = ConnesKreimer.ofTree T * ConnesKreimer.ofTree S + (insertion (ConnesKreimer.ofTree T)) (ConnesKreimer.ofTree S)

Two trees multiply to their disjoint union plus their graftings, T ⋆ S = T S + T ∘ S.

The Grossman–Larson algebra

structure GrossmanLarson (R : Type u_1) [CommSemiring R] (α : Type u_2) : Type (max u_1 u_2)

The forests of nonplanar rooted trees labelled by α, with the Grossman–Larson product.

• ofConnesKreimer :: (
• toConnesKreimer : ConnesKreimer R (UnorderedTree α)

  The underlying element of the module of forests.

• )

theorem GrossmanLarson.toConnesKreimer_injective {R : Type u_1} [CommSemiring R] {α : Type u_2} : Function.Injective toConnesKreimer

theorem GrossmanLarson.ext {R : Type u_1} [CommSemiring R] {α : Type u_2} {x y : GrossmanLarson R α} (h : x.toConnesKreimer = y.toConnesKreimer) : x = y

theorem GrossmanLarson.ext_iff {R : Type u_1} [CommSemiring R] {α : Type u_2} {x y : GrossmanLarson R α} : x = y ↔ x.toConnesKreimer = y.toConnesKreimer

@[instance_reducible]

noncomputable instance GrossmanLarson.instZero {R : Type u_1} [CommSemiring R] {α : Type u_2} : Zero (GrossmanLarson R α)

Equations

• GrossmanLarson.instZero = { zero := { toConnesKreimer := 0 } }

@[instance_reducible]

noncomputable instance GrossmanLarson.instAdd {R : Type u_1} [CommSemiring R] {α : Type u_2} : Add (GrossmanLarson R α)

Equations

• GrossmanLarson.instAdd = { add := fun (x y : GrossmanLarson R α) => { toConnesKreimer := x.toConnesKreimer + y.toConnesKreimer } }

@[instance_reducible]

instance GrossmanLarson.instSMul {R : Type u_1} [CommSemiring R] {α : Type u_2} {S : Type u_3} [SMul S (ConnesKreimer R (UnorderedTree α))] : SMul S (GrossmanLarson R α)

Equations

• GrossmanLarson.instSMul = { smul := fun (s : S) (x : GrossmanLarson R α) => { toConnesKreimer := s • x.toConnesKreimer } }

@[simp]

theorem GrossmanLarson.toConnesKreimer_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : toConnesKreimer 0 = 0

@[simp]

theorem GrossmanLarson.toConnesKreimer_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : GrossmanLarson R α) : (x + y).toConnesKreimer = x.toConnesKreimer + y.toConnesKreimer

@[simp]

theorem GrossmanLarson.toConnesKreimer_smul {R : Type u_1} [CommSemiring R] {α : Type u_2} {S : Type u_3} [SMul S (ConnesKreimer R (UnorderedTree α))] (s : S) (x : GrossmanLarson R α) : (s • x).toConnesKreimer = s • x.toConnesKreimer

@[instance_reducible]

noncomputable instance GrossmanLarson.instAddCommMonoid {R : Type u_1} [CommSemiring R] {α : Type u_2} : AddCommMonoid (GrossmanLarson R α)

Equations

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

noncomputable def GrossmanLarson.addEquiv {R : Type u_1} [CommSemiring R] {α : Type u_2} : GrossmanLarson R α ≃+ ConnesKreimer R (UnorderedTree α)

toConnesKreimer as an additive equivalence.

Equations

• GrossmanLarson.addEquiv = { toFun := GrossmanLarson.toConnesKreimer, invFun := GrossmanLarson.ofConnesKreimer, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }

@[instance_reducible]

noncomputable instance GrossmanLarson.instModule {R : Type u_1} [CommSemiring R] {α : Type u_2} : Module R (GrossmanLarson R α)

Equations

• GrossmanLarson.instModule = { toSMul := GrossmanLarson.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def GrossmanLarson.linearEquiv {R : Type u_1} [CommSemiring R] {α : Type u_2} : GrossmanLarson R α ≃ₗ[R] ConnesKreimer R (UnorderedTree α)

toConnesKreimer as a linear equivalence.

Equations

• GrossmanLarson.linearEquiv = { toFun := GrossmanLarson.addEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := GrossmanLarson.addEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem GrossmanLarson.linearEquiv_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : GrossmanLarson R α) : linearEquiv x = x.toConnesKreimer

@[simp]

theorem GrossmanLarson.linearEquiv_symm_apply {R : Type u_1} [CommSemiring R] {α : Type u_2} (x : ConnesKreimer R (UnorderedTree α)) : linearEquiv.symm x = { toConnesKreimer := x }

@[simp]

theorem GrossmanLarson.toConnesKreimer_multisetSum {R : Type u_1} [CommSemiring R] {α : Type u_2} (s : Multiset (GrossmanLarson R α)) : s.sum.toConnesKreimer = (Multiset.map toConnesKreimer s).sum

@[instance_reducible]

noncomputable instance GrossmanLarson.instOne {R : Type u_1} [CommSemiring R] {α : Type u_2} : One (GrossmanLarson R α)

Equations

• GrossmanLarson.instOne = { one := { toConnesKreimer := 1 } }

@[simp]

theorem GrossmanLarson.toConnesKreimer_one {R : Type u_1} [CommSemiring R] {α : Type u_2} : toConnesKreimer 1 = 1

@[instance_reducible]

noncomputable instance GrossmanLarson.instMul {R : Type u_1} [CommSemiring R] {α : Type u_2} : Mul (GrossmanLarson R α)

Equations

• GrossmanLarson.instMul = { mul := fun (x y : GrossmanLarson R α) => { toConnesKreimer := (GrossmanLarson.product x.toConnesKreimer) y.toConnesKreimer } }

@[simp]

theorem GrossmanLarson.toConnesKreimer_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : GrossmanLarson R α) : (x * y).toConnesKreimer = (product x.toConnesKreimer) y.toConnesKreimer

@[instance_reducible]

noncomputable instance GrossmanLarson.instNonAssocSemiring {R : Type u_1} [CommSemiring R] {α : Type u_2} : NonAssocSemiring (GrossmanLarson R α)

Equations

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

instance GrossmanLarson.instIsScalarTower {R : Type u_1} [CommSemiring R] {α : Type u_2} : IsScalarTower R (GrossmanLarson R α) (GrossmanLarson R α)

instance GrossmanLarson.instSMulCommClass {R : Type u_1} [CommSemiring R] {α : Type u_2} : SMulCommClass R (GrossmanLarson R α) (GrossmanLarson R α)

The basis

noncomputable def GrossmanLarson.of {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : UnorderedTree.Forest (UnorderedTree α)) : GrossmanLarson R α

of F is the basis vector of the forest F.

Equations

• GrossmanLarson.of F = { toConnesKreimer := ConnesKreimer.of' F }

@[simp]

theorem GrossmanLarson.toConnesKreimer_of {R : Type u_1} [CommSemiring R] {α : Type u_2} (F : UnorderedTree.Forest (UnorderedTree α)) : (of F).toConnesKreimer = ConnesKreimer.of' F

@[simp]

theorem GrossmanLarson.of_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} : of 0 = 1

theorem GrossmanLarson.of_mul_of {R : Type u_1} [CommSemiring R] {α : Type u_2} (F G : UnorderedTree.Forest (UnorderedTree α)) : of F * of G = (Multiset.map of (UnorderedTree.productMultiset F G)).sum

theorem GrossmanLarson.lhom_ext {R : Type u_1} [CommSemiring R] {α : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] {f g : GrossmanLarson R α →ₗ[R] M} (h : ∀ (F : UnorderedTree.Forest (UnorderedTree α)), f (of F) = g (of F)) : f = g

Linear maps off GrossmanLarson R α agree if they agree on the basis.

Trees as one-tree forests

noncomputable def GrossmanLarson.ι {R : Type u_1} [CommSemiring R] {α : Type u_2} : ChapotonLivernet R α →ₗ[R] GrossmanLarson R α

ι sends each tree to its one-tree forest.

Equations

• GrossmanLarson.ι = ↑GrossmanLarson.linearEquiv.symm ∘ₗ Finsupp.linearCombination R ConnesKreimer.ofTree ∘ₗ ↑ChapotonLivernet.coeffLinearEquiv

@[simp]

theorem GrossmanLarson.ι_of {R : Type u_1} [CommSemiring R] {α : Type u_2} (T : UnorderedTree α) : ι (ChapotonLivernet.of T) = of {T}

theorem GrossmanLarson.ι_injective {R : Type u_1} [CommSemiring R] {α : Type u_2} : Function.Injective ⇑ι

theorem GrossmanLarson.toConnesKreimer_ι_mul {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ChapotonLivernet R α) : (ι (x * y)).toConnesKreimer = (insertion (ι x).toConnesKreimer) (ι y).toConnesKreimer

The grafting product of trees is the insertion of their one-tree forests.

theorem GrossmanLarson.toConnesKreimer_ι_mul_ι {R : Type u_1} [CommSemiring R] {α : Type u_2} (x y : ChapotonLivernet R α) : (ι x * ι y).toConnesKreimer = (ι x).toConnesKreimer * (ι y).toConnesKreimer + (insertion (ι x).toConnesKreimer) (ι y).toConnesKreimer

The product of one-tree forests is their disjoint union plus their insertion, x ⋆ y = x y + x ∘ y.