The pre-Lie algebra of rooted trees

This file defines ChapotonLivernet R α, the free R-module on nonplanar rooted trees labelled by α, with the grafting product: of T * of S sums the trees obtained by grafting S onto one vertex of T. Chapoton and Livernet show that this is the free pre-Lie algebra on α. This file proves that it is a right pre-Lie algebra, from the symmetry of the associator UnorderedTree.insertSum_assoc_symm; freeness is not proved.

Main definitions

• ChapotonLivernet R α: the free module on the trees, a structure over its coefficients coeff : UnorderedTree α →₀ R, as for MonoidAlgebra.
• ChapotonLivernet.of: the basis vector of a tree.
• ChapotonLivernet.graft: the product of two basis vectors.

Main results

• ChapotonLivernet.instRightPreLieRing, ChapotonLivernet.instRightPreLieAlgebra: the grafting product is right pre-Lie, and so its commutator is a Lie bracket.
• ChapotonLivernet.of_mul_of: of T * of S = graft T S.

Implementation notes

The host comes first, as in Chapoton and Livernet and in Foissy: of T * of S grafts S onto T, and the associator is symmetric in its last two arguments. The convention that grafts the first factor onto the second gives a left pre-Lie algebra, (ChapotonLivernet R α)ᵐᵒᵖ.

References

• [CL01]
• [Foi21]

structure ChapotonLivernet (R : Type u_1) [Semiring R] (α : Type u_2) : Type (max u_1 u_2)

The free module on the nonplanar rooted trees labelled by α, which the grafting product makes a pre-Lie algebra.

• ofCoeff :: (
• coeff : UnorderedTree α →₀ R

  The coefficient of each tree.

• )

def ChapotonLivernet.coeffEquiv {R : Type u_1} {α : Type u_2} [Semiring R] : ChapotonLivernet R α ≃ (UnorderedTree α →₀ R)

coeff as an equivalence with the finitely supported functions on trees.

Equations

• ChapotonLivernet.coeffEquiv = { toFun := ChapotonLivernet.coeff, invFun := ChapotonLivernet.ofCoeff, left_inv := ⋯, right_inv := ⋯ }

theorem ChapotonLivernet.ext {R : Type u_1} {α : Type u_2} [Semiring R] {x y : ChapotonLivernet R α} (h : x.coeff = y.coeff) : x = y

theorem ChapotonLivernet.ext_iff {R : Type u_1} {α : Type u_2} [Semiring R] {x y : ChapotonLivernet R α} : x = y ↔ x.coeff = y.coeff

@[instance_reducible]

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

Equations

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

noncomputable def ChapotonLivernet.coeffAddEquiv {R : Type u_1} {α : Type u_2} [Semiring R] : ChapotonLivernet R α ≃+ (UnorderedTree α →₀ R)

coeff as an additive equivalence.

Equations

• ChapotonLivernet.coeffAddEquiv = ChapotonLivernet.coeffEquiv.addEquiv

@[instance_reducible]

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

Equations

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

@[simp]

theorem ChapotonLivernet.coeff_zero {R : Type u_1} {α : Type u_2} [Semiring R] : coeff 0 = 0

@[simp]

theorem ChapotonLivernet.coeff_add {R : Type u_1} {α : Type u_2} [Semiring R] (x y : ChapotonLivernet R α) : (x + y).coeff = x.coeff + y.coeff

@[simp]

theorem ChapotonLivernet.coeff_smul {R : Type u_1} {α : Type u_2} [Semiring R] (r : R) (x : ChapotonLivernet R α) : (r • x).coeff = r • x.coeff

noncomputable def ChapotonLivernet.coeffLinearEquiv {R : Type u_1} {α : Type u_2} [Semiring R] : ChapotonLivernet R α ≃ₗ[R] UnorderedTree α →₀ R

coeff as a linear equivalence.

Equations

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

noncomputable def ChapotonLivernet.single {R : Type u_1} {α : Type u_2} [Semiring R] (T : UnorderedTree α) (r : R) : ChapotonLivernet R α

single T r is r times the tree T.

Equations

• ChapotonLivernet.single T r = { coeff := Finsupp.single T r }

@[simp]

theorem ChapotonLivernet.coeff_single {R : Type u_1} {α : Type u_2} [Semiring R] (T : UnorderedTree α) (r : R) : (single T r).coeff = Finsupp.single T r

@[reducible, inline]

noncomputable abbrev ChapotonLivernet.of {R : Type u_1} {α : Type u_2} [Semiring R] (T : UnorderedTree α) : ChapotonLivernet R α

of T is the basis vector of the tree T.

Equations

• ChapotonLivernet.of T = ChapotonLivernet.single T 1

noncomputable def ChapotonLivernet.graft {R : Type u_1} {α : Type u_2} [Semiring R] (T S : UnorderedTree α) : ChapotonLivernet R α

graft T S sums the basis vectors of the trees in T ◁ S.

Equations

• ChapotonLivernet.graft T S = (Multiset.map ChapotonLivernet.of (T.insertSum S)).sum

@[instance_reducible]

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

The grafting product extends graft bilinearly.

Equations

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

theorem ChapotonLivernet.mul_def {R : Type u_1} {α : Type u_2} [Semiring R] (x y : ChapotonLivernet R α) : x * y = x.coeff.sum fun (T : UnorderedTree α) (a : R) => y.coeff.sum fun (S : UnorderedTree α) (b : R) => (a * b) • graft T S

@[instance_reducible]

noncomputable instance ChapotonLivernet.instNonUnitalNonAssocSemiring {R : Type u_1} {α : Type u_2} [Semiring R] : NonUnitalNonAssocSemiring (ChapotonLivernet R α)

Equations

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

theorem ChapotonLivernet.single_mul_single {R : Type u_1} {α : Type u_2} [Semiring R] (T S : UnorderedTree α) (a b : R) : single T a * single S b = (a * b) • graft T S

theorem ChapotonLivernet.induction_linear {R : Type u_1} {α : Type u_2} [Semiring R] {motive : ChapotonLivernet R α → Prop} (x : ChapotonLivernet R α) (zero : motive 0) (add : ∀ (x y : ChapotonLivernet R α), motive x → motive y → motive (x + y)) (single : ∀ (T : UnorderedTree α) (r : R), motive (single T r)) : motive x

theorem ChapotonLivernet.single_eq_smul_of {R : Type u_1} {α : Type u_2} [CommSemiring R] (T : UnorderedTree α) (r : R) : single T r = r • of T

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

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

theorem ChapotonLivernet.of_mul_of {R : Type u_1} {α : Type u_2} [CommSemiring R] (T S : UnorderedTree α) : of T * of S = graft T S

theorem ChapotonLivernet.graft_mul_of {R : Type u_1} {α : Type u_2} [CommSemiring R] (T S U : UnorderedTree α) : graft T S * of U = (Multiset.map of ((T.insertSum S).bind fun (x : UnorderedTree α) => x.insertSum U)).sum

theorem ChapotonLivernet.of_mul_graft {R : Type u_1} {α : Type u_2} [CommSemiring R] (T S U : UnorderedTree α) : of T * graft S U = (Multiset.map of ((S.insertSum U).bind fun (x : UnorderedTree α) => T.insertSum x)).sum

theorem ChapotonLivernet.of_leaf_mul_of_leaf {R : Type u_1} {α : Type u_2} [CommSemiring R] (a b : α) : of (UnorderedTree.leaf a) * of (UnorderedTree.leaf b) = of (UnorderedTree.mk (RoseTree.node a [RoseTree.leaf b]))

Grafting a leaf onto a leaf gives the two-vertex tree.

@[instance_reducible]

noncomputable instance ChapotonLivernet.instAddCommGroup {R : Type u_1} {α : Type u_2} [CommRing R] : AddCommGroup (ChapotonLivernet R α)

Equations

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

@[instance_reducible]

noncomputable instance ChapotonLivernet.instNonUnitalNonAssocRing {R : Type u_1} {α : Type u_2} [CommRing R] : NonUnitalNonAssocRing (ChapotonLivernet R α)

Equations

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

@[instance_reducible]

noncomputable instance ChapotonLivernet.instRightPreLieRing {R : Type u_1} {α : Type u_2} [CommRing R] : RightPreLieRing (ChapotonLivernet R α)

Equations

• ChapotonLivernet.instRightPreLieRing = { toNonUnitalNonAssocRing := ChapotonLivernet.instNonUnitalNonAssocRing, assoc_symm' := ⋯ }

@[instance_reducible]

noncomputable instance ChapotonLivernet.instRightPreLieAlgebra {R : Type u_1} {α : Type u_2} [CommRing R] : RightPreLieAlgebra R (ChapotonLivernet R α)

Equations

• ChapotonLivernet.instRightPreLieAlgebra = { toModule := ChapotonLivernet.instModule, toIsScalarTower := ⋯, toSMulCommClass := ⋯ }