Linearised Pre-Lie Grafting

This file linearly extends planar pre-Lie grafting to finitely supported formal sums of planar rooted trees.

theorem BSeries.sum_single_apply_count {ι : Type u} {R : Type v} [DecidableEq ι] [Semiring R] (xs : List ι) (a : ι) : (List.map (fun (x : ι) => Finsupp.single x 1) xs).sum a = ↑(List.count a xs)

Coefficients of a formal sum of basis vectors count list occurrences.

theorem BSeries.sum_single_eq_of_perm {ι : Type u} {R : Type v} [DecidableEq ι] [Semiring R] {xs ys : List ι} (h : xs.Perm ys) : (List.map (fun (x : ι) => Finsupp.single x 1) xs).sum = (List.map (fun (x : ι) => Finsupp.single x 1) ys).sum

@[reducible, inline]

abbrev BSeries.PTree.FreeModule (R : Type u) [Zero R] : Type u

Finitely supported formal sums of planar rooted trees.

Equations

• BSeries.PTree.FreeModule R = (HopfAlgebras.PTree →₀ R)

def BSeries.PTree.HomogeneousOfOrder {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : Prop

A formal tree sum supported only on trees of order n.

Equations

• BSeries.PTree.HomogeneousOfOrder x n = ∀ u ∈ x.support, u.order = n

def BSeries.PTree.SupportedUpToOrder {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : Prop

A formal tree sum supported only on trees of order at most n.

Equations

• BSeries.PTree.SupportedUpToOrder x n = ∀ u ∈ x.support, u.order ≤ n

@[simp]

theorem BSeries.PTree.homogeneousOfOrder_zero (R : Type u) [Zero R] (n : ℕ) : HomogeneousOfOrder 0 n

theorem BSeries.PTree.homogeneousOfOrder_single (R : Type u) [Zero R] (s : HopfAlgebras.PTree) (a : R) : HomogeneousOfOrder (Finsupp.single s a) s.order

@[simp]

theorem BSeries.PTree.supportedUpToOrder_zero (R : Type u) [Zero R] (n : ℕ) : SupportedUpToOrder 0 n

theorem BSeries.PTree.HomogeneousOfOrder.supportedUpToOrder {R : Type u} [Zero R] {x : FreeModule R} {n : ℕ} (h : HomogeneousOfOrder x n) : SupportedUpToOrder x n

theorem BSeries.PTree.SupportedUpToOrder.mono {R : Type u} [Zero R] {x : FreeModule R} {m n : ℕ} (h : SupportedUpToOrder x m) (hmn : m ≤ n) : SupportedUpToOrder x n

def BSeries.PTree.AgreeUpToOrder {R : Type u} [Zero R] (x y : FreeModule R) (n : ℕ) : Prop

Two formal tree sums have equal coefficients through order n.

Equations

• BSeries.PTree.AgreeUpToOrder x y n = ∀ (u : HopfAlgebras.PTree), u.order ≤ n → x u = y u

theorem BSeries.PTree.agreeUpToOrder_refl {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : AgreeUpToOrder x x n

theorem BSeries.PTree.AgreeUpToOrder.symm {R : Type u} [Zero R] {x y : FreeModule R} {n : ℕ} (h : AgreeUpToOrder x y n) : AgreeUpToOrder y x n

theorem BSeries.PTree.AgreeUpToOrder.trans {R : Type u} [Zero R] {x y z : FreeModule R} {n : ℕ} (hxy : AgreeUpToOrder x y n) (hyz : AgreeUpToOrder y z n) : AgreeUpToOrder x z n

theorem BSeries.PTree.AgreeUpToOrder.mono {R : Type u} [Zero R] {x y : FreeModule R} {m n : ℕ} (h : AgreeUpToOrder x y n) (hmn : m ≤ n) : AgreeUpToOrder x y m

theorem BSeries.PTree.agreeUpToOrder_all_iff_eq {R : Type u} [Zero R] (x y : FreeModule R) : (∀ (n : ℕ), AgreeUpToOrder x y n) ↔ x = y

theorem BSeries.PTree.AgreeUpToOrder.eq_of_supportedUpToOrder {R : Type u} [Zero R] {x y : FreeModule R} {n : ℕ} (h : AgreeUpToOrder x y n) (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : x = y

theorem BSeries.PTree.HomogeneousOfOrder.add {R : Type u} [AddMonoid R] {x y : FreeModule R} {n : ℕ} (hx : HomogeneousOfOrder x n) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (x + y) n

theorem BSeries.PTree.SupportedUpToOrder.add {R : Type u} [AddMonoid R] {x y : FreeModule R} {n : ℕ} (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (x + y) n

theorem BSeries.PTree.HomogeneousOfOrder.smul {S : Type v} {R : Type u} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule R} {n : ℕ} (h : HomogeneousOfOrder x n) : HomogeneousOfOrder (c • x) n

theorem BSeries.PTree.SupportedUpToOrder.smul {S : Type v} {R : Type u} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule R} {n : ℕ} (h : SupportedUpToOrder x n) : SupportedUpToOrder (c • x) n

theorem BSeries.PTree.supportedUpToOrder_single_of_le (R : Type u) [Zero R] {s : HopfAlgebras.PTree} {n : ℕ} (a : R) (hs : s.order ≤ n) : SupportedUpToOrder (Finsupp.single s a) n

noncomputable def BSeries.PTree.preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : FreeModule R

The formal sum of all planar grafts of s at one vertex of t.

Equations

• BSeries.PTree.preLieVector R s t = (List.map (fun (u : HopfAlgebras.PTree) => Finsupp.single u 1) (BSeries.PTree.preLieGrafts s t)).sum

theorem BSeries.PTree.preLieVector_apply (R : Type u) [Semiring R] (s t u : HopfAlgebras.PTree) : (preLieVector R s t) u = ↑(List.count u (preLieGrafts s t))

theorem BSeries.PTree.preLieVector_apply_eq_zero_of_order_ne (R : Type u) [Semiring R] (s t u : HopfAlgebras.PTree) (h : ¬u.order = s.order + t.order) : (preLieVector R s t) u = 0

theorem BSeries.PTree.order_of_mem_support_preLieVector (R : Type u) [Semiring R] (s t u : HopfAlgebras.PTree) (hu : u ∈ (preLieVector R s t).support) : u.order = s.order + t.order

theorem BSeries.PTree.homogeneousOfOrder_preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : HomogeneousOfOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.PTree.supportedUpToOrder_preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : SupportedUpToOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.PTree.mapDomain_sum_single {β : Type v} (R : Type u) [Semiring R] (f : HopfAlgebras.PTree → β) (ts : List HopfAlgebras.PTree) : Finsupp.mapDomain f (List.map (fun (u : HopfAlgebras.PTree) => Finsupp.single u 1) ts).sum = (List.map (fun (u : HopfAlgebras.PTree) => Finsupp.single (f u) 1) ts).sum

noncomputable def BSeries.PTree.preLie (R : Type u) [Semiring R] (x y : FreeModule R) : FreeModule R

Bilinear extension of planar pre-Lie grafting to formal tree sums.

Equations

• BSeries.PTree.preLie R x y = Finsupp.sum x fun (s : HopfAlgebras.PTree) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PTree) (b : R) => (a * b) • BSeries.PTree.preLieVector R s t

theorem BSeries.PTree.preLie_apply (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) : (preLie R x y) u = Finsupp.sum x fun (s : HopfAlgebras.PTree) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PTree) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))

theorem BSeries.PTree.preLie_apply_eq_zero_of_forall_order_ne (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (preLie R x y) u = 0

theorem BSeries.PTree.exists_order_eq_of_mem_support_preLie (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) (hu : u ∈ (preLie R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.PTree.HomogeneousOfOrder.preLie (R : Type u) [Semiring R] {x y : FreeModule R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (PTree.preLie R x y) (m + n)

theorem BSeries.PTree.SupportedUpToOrder.preLie (R : Type u) [Semiring R] {x y : FreeModule R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (PTree.preLie R x y) (m + n)

@[simp]

theorem BSeries.PTree.preLie_zero_left (R : Type u) [Semiring R] (x : FreeModule R) : preLie R 0 x = 0

@[simp]

theorem BSeries.PTree.preLie_zero_right (R : Type u) [Semiring R] (x : FreeModule R) : preLie R x 0 = 0

theorem BSeries.PTree.preLie_add_left (R : Type u) [Semiring R] (x y z : FreeModule R) : preLie R (x + y) z = preLie R x z + preLie R y z

theorem BSeries.PTree.preLie_add_right (R : Type u) [Semiring R] (x y z : FreeModule R) : preLie R x (y + z) = preLie R x y + preLie R x z

theorem BSeries.PTree.preLie_smul_left (R : Type u) [Semiring R] (c : R) (x y : FreeModule R) : preLie R (c • x) y = c • preLie R x y

theorem BSeries.PTree.preLie_smul_right (R : Type u) [CommSemiring R] (c : R) (x y : FreeModule R) : preLie R x (c • y) = c • preLie R x y

theorem BSeries.PTree.preLie_single_single (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) (a b : R) : preLie R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t

@[simp]

theorem BSeries.PTree.preLie_single_single_one (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : preLie R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t

noncomputable def BSeries.PTree.lieBracket (R : Type u) [Ring R] (x y : FreeModule R) : FreeModule R

The commutator bracket induced by planar pre-Lie grafting.

Equations

• BSeries.PTree.lieBracket R x y = BSeries.PTree.preLie R x y - BSeries.PTree.preLie R y x

theorem BSeries.PTree.lieBracket_apply (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) : (lieBracket R x y) u = (Finsupp.sum x fun (s : HopfAlgebras.PTree) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PTree) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))) - Finsupp.sum y fun (s : HopfAlgebras.PTree) (a : R) => Finsupp.sum x fun (t : HopfAlgebras.PTree) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))

theorem BSeries.PTree.lieBracket_apply_eq_zero_of_forall_order_ne (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (lieBracket R x y) u = 0

theorem BSeries.PTree.exists_order_eq_of_mem_support_lieBracket (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.PTree) (hu : u ∈ (lieBracket R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.PTree.HomogeneousOfOrder.lieBracket (R : Type u) [Ring R] {x y : FreeModule R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (PTree.lieBracket R x y) (m + n)

theorem BSeries.PTree.SupportedUpToOrder.lieBracket (R : Type u) [Ring R] {x y : FreeModule R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (PTree.lieBracket R x y) (m + n)

@[simp]

theorem BSeries.PTree.lieBracket_zero_left (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R 0 x = 0

@[simp]

theorem BSeries.PTree.lieBracket_zero_right (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R x 0 = 0

@[simp]

theorem BSeries.PTree.lieBracket_self (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R x x = 0

theorem BSeries.PTree.lieBracket_skew (R : Type u) [Ring R] (x y : FreeModule R) : lieBracket R x y = -lieBracket R y x

theorem BSeries.PTree.lieBracket_add_left (R : Type u) [Ring R] (x y z : FreeModule R) : lieBracket R (x + y) z = lieBracket R x z + lieBracket R y z

theorem BSeries.PTree.lieBracket_add_right (R : Type u) [Ring R] (x y z : FreeModule R) : lieBracket R x (y + z) = lieBracket R x y + lieBracket R x z

theorem BSeries.PTree.lieBracket_smul_left (R : Type u) [CommRing R] (c : R) (x y : FreeModule R) : lieBracket R (c • x) y = c • lieBracket R x y

theorem BSeries.PTree.lieBracket_smul_right (R : Type u) [CommRing R] (c : R) (x y : FreeModule R) : lieBracket R x (c • y) = c • lieBracket R x y

theorem BSeries.PTree.lieBracket_single_single (R : Type u) [Ring R] (s t : HopfAlgebras.PTree) (a b : R) : lieBracket R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t - (b * a) • preLieVector R t s

@[simp]

theorem BSeries.PTree.lieBracket_single_single_one (R : Type u) [Ring R] (s t : HopfAlgebras.PTree) : lieBracket R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t - preLieVector R t s

@[simp]

theorem BSeries.PTree.preLieVector_bullet (R : Type u) [Semiring R] (s : HopfAlgebras.PTree) : preLieVector R s HopfAlgebras.PTree.bullet = Finsupp.single (HopfAlgebras.PTree.node [s]) 1

@[reducible, inline]

abbrev BSeries.RootedTree.FreeModule (R : Type u) [Zero R] : Type u

Finitely supported formal sums of non-planar rooted trees.

Equations

• BSeries.RootedTree.FreeModule R = (HopfAlgebras.RootedTree →₀ R)

def BSeries.RootedTree.HomogeneousOfOrder {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : Prop

A non-planar formal tree sum supported only on trees of order n.

Equations

• BSeries.RootedTree.HomogeneousOfOrder x n = ∀ u ∈ x.support, u.order = n

def BSeries.RootedTree.SupportedUpToOrder {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : Prop

A non-planar formal tree sum supported only on trees of order at most n.

Equations

• BSeries.RootedTree.SupportedUpToOrder x n = ∀ u ∈ x.support, u.order ≤ n

@[simp]

theorem BSeries.RootedTree.homogeneousOfOrder_zero (R : Type u) [Zero R] (n : ℕ) : HomogeneousOfOrder 0 n

theorem BSeries.RootedTree.homogeneousOfOrder_single (R : Type u) [Zero R] (s : HopfAlgebras.RootedTree) (a : R) : HomogeneousOfOrder (Finsupp.single s a) s.order

@[simp]

theorem BSeries.RootedTree.supportedUpToOrder_zero (R : Type u) [Zero R] (n : ℕ) : SupportedUpToOrder 0 n

theorem BSeries.RootedTree.HomogeneousOfOrder.supportedUpToOrder {R : Type u} [Zero R] {x : FreeModule R} {n : ℕ} (h : HomogeneousOfOrder x n) : SupportedUpToOrder x n

theorem BSeries.RootedTree.SupportedUpToOrder.mono {R : Type u} [Zero R] {x : FreeModule R} {m n : ℕ} (h : SupportedUpToOrder x m) (hmn : m ≤ n) : SupportedUpToOrder x n

def BSeries.RootedTree.AgreeUpToOrder {R : Type u} [Zero R] (x y : FreeModule R) (n : ℕ) : Prop

Two non-planar formal tree sums have equal coefficients through order n.

Equations

• BSeries.RootedTree.AgreeUpToOrder x y n = ∀ (u : HopfAlgebras.RootedTree), u.order ≤ n → x u = y u

theorem BSeries.RootedTree.agreeUpToOrder_refl {R : Type u} [Zero R] (x : FreeModule R) (n : ℕ) : AgreeUpToOrder x x n

theorem BSeries.RootedTree.AgreeUpToOrder.symm {R : Type u} [Zero R] {x y : FreeModule R} {n : ℕ} (h : AgreeUpToOrder x y n) : AgreeUpToOrder y x n

theorem BSeries.RootedTree.AgreeUpToOrder.trans {R : Type u} [Zero R] {x y z : FreeModule R} {n : ℕ} (hxy : AgreeUpToOrder x y n) (hyz : AgreeUpToOrder y z n) : AgreeUpToOrder x z n

theorem BSeries.RootedTree.AgreeUpToOrder.mono {R : Type u} [Zero R] {x y : FreeModule R} {m n : ℕ} (h : AgreeUpToOrder x y n) (hmn : m ≤ n) : AgreeUpToOrder x y m

theorem BSeries.RootedTree.agreeUpToOrder_all_iff_eq {R : Type u} [Zero R] (x y : FreeModule R) : (∀ (n : ℕ), AgreeUpToOrder x y n) ↔ x = y

theorem BSeries.RootedTree.AgreeUpToOrder.eq_of_supportedUpToOrder {R : Type u} [Zero R] {x y : FreeModule R} {n : ℕ} (h : AgreeUpToOrder x y n) (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : x = y

theorem BSeries.RootedTree.HomogeneousOfOrder.add {R : Type u} [AddMonoid R] {x y : FreeModule R} {n : ℕ} (hx : HomogeneousOfOrder x n) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (x + y) n

theorem BSeries.RootedTree.SupportedUpToOrder.add {R : Type u} [AddMonoid R] {x y : FreeModule R} {n : ℕ} (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (x + y) n

theorem BSeries.RootedTree.HomogeneousOfOrder.smul {S : Type w} {R : Type u} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule R} {n : ℕ} (h : HomogeneousOfOrder x n) : HomogeneousOfOrder (c • x) n

theorem BSeries.RootedTree.SupportedUpToOrder.smul {S : Type w} {R : Type u} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule R} {n : ℕ} (h : SupportedUpToOrder x n) : SupportedUpToOrder (c • x) n

theorem BSeries.RootedTree.supportedUpToOrder_single_of_le (R : Type u) [Zero R] {s : HopfAlgebras.RootedTree} {n : ℕ} (a : R) (hs : s.order ≤ n) : SupportedUpToOrder (Finsupp.single s a) n

noncomputable def BSeries.RootedTree.preLieVectorOfPTree (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : FreeModule R

Equations

• BSeries.RootedTree.preLieVectorOfPTree R s t = (List.map (fun (u : HopfAlgebras.PTree) => Finsupp.single (HopfAlgebras.RootedTree.ofPTree u) 1) (BSeries.PTree.preLieGrafts s t)).sum

theorem BSeries.RootedTree.preLieVectorOfPTree_apply (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) (u : HopfAlgebras.RootedTree) : (preLieVectorOfPTree R s t) u = ↑(List.count u (List.map HopfAlgebras.RootedTree.ofPTree (PTree.preLieGrafts s t)))

theorem BSeries.RootedTree.preLieVectorOfPTree_apply_eq_zero_of_order_ne (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) (u : HopfAlgebras.RootedTree) (h : ¬u.order = (HopfAlgebras.RootedTree.ofPTree s).order + (HopfAlgebras.RootedTree.ofPTree t).order) : (preLieVectorOfPTree R s t) u = 0

theorem BSeries.RootedTree.preLieVectorOfPTree_perm_left (R : Type u) [Semiring R] {s s' : HopfAlgebras.PTree} (hs : s.Perm s') (t : HopfAlgebras.PTree) : preLieVectorOfPTree R s t = preLieVectorOfPTree R s' t

theorem BSeries.RootedTree.preLieVectorOfPTree_perm_right (R : Type u) [Semiring R] (s : HopfAlgebras.PTree) {t t' : HopfAlgebras.PTree} (ht : t.Perm t') : preLieVectorOfPTree R s t = preLieVectorOfPTree R s t'

noncomputable def BSeries.RootedTree.preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.RootedTree) : FreeModule R

The formal sum of all non-planar grafts of one rooted tree at another.

Equations

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

@[simp]

theorem BSeries.RootedTree.preLieVector_ofPTree (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : preLieVector R (HopfAlgebras.RootedTree.ofPTree s) (HopfAlgebras.RootedTree.ofPTree t) = preLieVectorOfPTree R s t

@[simp]

theorem BSeries.RootedTree.mapDomain_ofPTree_preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.PTree) : Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree (PTree.preLieVector R s t) = preLieVector R (HopfAlgebras.RootedTree.ofPTree s) (HopfAlgebras.RootedTree.ofPTree t)

theorem BSeries.RootedTree.preLieVector_apply_eq_zero_of_order_ne (R : Type u) [Semiring R] (s t u : HopfAlgebras.RootedTree) (h : ¬u.order = s.order + t.order) : (preLieVector R s t) u = 0

theorem BSeries.RootedTree.order_of_mem_support_preLieVector (R : Type u) [Semiring R] (s t u : HopfAlgebras.RootedTree) (hu : u ∈ (preLieVector R s t).support) : u.order = s.order + t.order

theorem BSeries.RootedTree.homogeneousOfOrder_preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.RootedTree) : HomogeneousOfOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.RootedTree.supportedUpToOrder_preLieVector (R : Type u) [Semiring R] (s t : HopfAlgebras.RootedTree) : SupportedUpToOrder (preLieVector R s t) (s.order + t.order)

noncomputable def BSeries.RootedTree.preLie (R : Type u) [Semiring R] (x y : FreeModule R) : FreeModule R

Bilinear extension of non-planar pre-Lie grafting to formal tree sums.

Equations

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

theorem BSeries.RootedTree.preLie_apply (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) : (preLie R x y) u = Finsupp.sum x fun (s : HopfAlgebras.RootedTree) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.RootedTree) (b : R) => a * b * (preLieVector R s t) u

theorem BSeries.RootedTree.preLie_apply_eq_zero_of_forall_order_ne (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (preLie R x y) u = 0

theorem BSeries.RootedTree.exists_order_eq_of_mem_support_preLie (R : Type u) [Semiring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) (hu : u ∈ (preLie R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.RootedTree.HomogeneousOfOrder.preLie (R : Type u) [Semiring R] {x y : FreeModule R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (RootedTree.preLie R x y) (m + n)

theorem BSeries.RootedTree.SupportedUpToOrder.preLie (R : Type u) [Semiring R] {x y : FreeModule R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (RootedTree.preLie R x y) (m + n)

@[simp]

theorem BSeries.RootedTree.preLie_zero_left (R : Type u) [Semiring R] (x : FreeModule R) : preLie R 0 x = 0

@[simp]

theorem BSeries.RootedTree.preLie_zero_right (R : Type u) [Semiring R] (x : FreeModule R) : preLie R x 0 = 0

theorem BSeries.RootedTree.preLie_add_left (R : Type u) [Semiring R] (x y z : FreeModule R) : preLie R (x + y) z = preLie R x z + preLie R y z

theorem BSeries.RootedTree.preLie_add_right (R : Type u) [Semiring R] (x y z : FreeModule R) : preLie R x (y + z) = preLie R x y + preLie R x z

theorem BSeries.RootedTree.preLie_smul_left (R : Type u) [Semiring R] (c : R) (x y : FreeModule R) : preLie R (c • x) y = c • preLie R x y

theorem BSeries.RootedTree.preLie_smul_right (R : Type u) [CommSemiring R] (c : R) (x y : FreeModule R) : preLie R x (c • y) = c • preLie R x y

theorem BSeries.RootedTree.preLie_single_single (R : Type u) [Semiring R] (s t : HopfAlgebras.RootedTree) (a b : R) : preLie R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t

@[simp]

theorem BSeries.RootedTree.preLie_single_single_one (R : Type u) [Semiring R] (s t : HopfAlgebras.RootedTree) : preLie R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t

@[simp]

theorem BSeries.RootedTree.mapDomain_ofPTree_preLie (R : Type u) [Semiring R] (x y : PTree.FreeModule R) : Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree (PTree.preLie R x y) = preLie R (Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree x) (Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree y)

noncomputable def BSeries.RootedTree.lieBracket (R : Type u) [Ring R] (x y : FreeModule R) : FreeModule R

The commutator bracket induced by non-planar pre-Lie grafting.

Equations

• BSeries.RootedTree.lieBracket R x y = BSeries.RootedTree.preLie R x y - BSeries.RootedTree.preLie R y x

theorem BSeries.RootedTree.lieBracket_apply (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) : (lieBracket R x y) u = (Finsupp.sum x fun (s : HopfAlgebras.RootedTree) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.RootedTree) (b : R) => a * b * (preLieVector R s t) u) - Finsupp.sum y fun (s : HopfAlgebras.RootedTree) (a : R) => Finsupp.sum x fun (t : HopfAlgebras.RootedTree) (b : R) => a * b * (preLieVector R s t) u

theorem BSeries.RootedTree.lieBracket_apply_eq_zero_of_forall_order_ne (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (lieBracket R x y) u = 0

theorem BSeries.RootedTree.exists_order_eq_of_mem_support_lieBracket (R : Type u) [Ring R] (x y : FreeModule R) (u : HopfAlgebras.RootedTree) (hu : u ∈ (lieBracket R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.RootedTree.HomogeneousOfOrder.lieBracket (R : Type u) [Ring R] {x y : FreeModule R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (RootedTree.lieBracket R x y) (m + n)

theorem BSeries.RootedTree.SupportedUpToOrder.lieBracket (R : Type u) [Ring R] {x y : FreeModule R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (RootedTree.lieBracket R x y) (m + n)

@[simp]

theorem BSeries.RootedTree.lieBracket_zero_left (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R 0 x = 0

@[simp]

theorem BSeries.RootedTree.lieBracket_zero_right (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R x 0 = 0

@[simp]

theorem BSeries.RootedTree.lieBracket_self (R : Type u) [Ring R] (x : FreeModule R) : lieBracket R x x = 0

theorem BSeries.RootedTree.lieBracket_skew (R : Type u) [Ring R] (x y : FreeModule R) : lieBracket R x y = -lieBracket R y x

theorem BSeries.RootedTree.lieBracket_add_left (R : Type u) [Ring R] (x y z : FreeModule R) : lieBracket R (x + y) z = lieBracket R x z + lieBracket R y z

theorem BSeries.RootedTree.lieBracket_add_right (R : Type u) [Ring R] (x y z : FreeModule R) : lieBracket R x (y + z) = lieBracket R x y + lieBracket R x z

theorem BSeries.RootedTree.lieBracket_smul_left (R : Type u) [CommRing R] (c : R) (x y : FreeModule R) : lieBracket R (c • x) y = c • lieBracket R x y

theorem BSeries.RootedTree.lieBracket_smul_right (R : Type u) [CommRing R] (c : R) (x y : FreeModule R) : lieBracket R x (c • y) = c • lieBracket R x y

theorem BSeries.RootedTree.lieBracket_single_single (R : Type u) [Ring R] (s t : HopfAlgebras.RootedTree) (a b : R) : lieBracket R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t - (b * a) • preLieVector R t s

@[simp]

theorem BSeries.RootedTree.lieBracket_single_single_one (R : Type u) [Ring R] (s t : HopfAlgebras.RootedTree) : lieBracket R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t - preLieVector R t s

@[simp]

theorem BSeries.RootedTree.mapDomain_ofPTree_lieBracket (R : Type u) [Ring R] (x y : PTree.FreeModule R) : Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree (PTree.lieBracket R x y) = lieBracket R (Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree x) (Finsupp.mapDomain HopfAlgebras.RootedTree.ofPTree y)

@[reducible, inline]

abbrev BSeries.PLTree.FreeModule (α : Type u) (R : Type v) [Zero R] : Type (max u v)

Finitely supported formal sums of labelled planar rooted trees.

Equations

• BSeries.PLTree.FreeModule α R = (HopfAlgebras.PLTree α →₀ R)

def BSeries.PLTree.HomogeneousOfOrder {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : Prop

A labelled formal tree sum supported only on trees of order n.

Equations

• BSeries.PLTree.HomogeneousOfOrder x n = ∀ u ∈ x.support, u.order = n

def BSeries.PLTree.SupportedUpToOrder {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : Prop

A labelled formal tree sum supported only on trees of order at most n.

Equations

• BSeries.PLTree.SupportedUpToOrder x n = ∀ u ∈ x.support, u.order ≤ n

@[simp]

theorem BSeries.PLTree.homogeneousOfOrder_zero {α : Type u} (R : Type v) [Zero R] (n : ℕ) : HomogeneousOfOrder 0 n

theorem BSeries.PLTree.homogeneousOfOrder_single {α : Type u} (R : Type v) [Zero R] (s : HopfAlgebras.PLTree α) (a : R) : HomogeneousOfOrder (Finsupp.single s a) s.order

@[simp]

theorem BSeries.PLTree.supportedUpToOrder_zero {α : Type u} (R : Type v) [Zero R] (n : ℕ) : SupportedUpToOrder 0 n

theorem BSeries.PLTree.HomogeneousOfOrder.supportedUpToOrder {α : Type u} {R : Type v} [Zero R] {x : FreeModule α R} {n : ℕ} (h : HomogeneousOfOrder x n) : SupportedUpToOrder x n

theorem BSeries.PLTree.SupportedUpToOrder.mono {α : Type u} {R : Type v} [Zero R] {x : FreeModule α R} {m n : ℕ} (h : SupportedUpToOrder x m) (hmn : m ≤ n) : SupportedUpToOrder x n

def BSeries.PLTree.AgreeUpToOrder {α : Type u} {R : Type v} [Zero R] (x y : FreeModule α R) (n : ℕ) : Prop

Two labelled planar formal tree sums have equal coefficients through order n.

Equations

• BSeries.PLTree.AgreeUpToOrder x y n = ∀ (u : HopfAlgebras.PLTree α), u.order ≤ n → x u = y u

theorem BSeries.PLTree.agreeUpToOrder_refl {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : AgreeUpToOrder x x n

theorem BSeries.PLTree.AgreeUpToOrder.symm {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {n : ℕ} (h : AgreeUpToOrder x y n) : AgreeUpToOrder y x n

theorem BSeries.PLTree.AgreeUpToOrder.trans {α : Type u} {R : Type v} [Zero R] {x y z : FreeModule α R} {n : ℕ} (hxy : AgreeUpToOrder x y n) (hyz : AgreeUpToOrder y z n) : AgreeUpToOrder x z n

theorem BSeries.PLTree.AgreeUpToOrder.mono {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {m n : ℕ} (h : AgreeUpToOrder x y n) (hmn : m ≤ n) : AgreeUpToOrder x y m

theorem BSeries.PLTree.agreeUpToOrder_all_iff_eq {α : Type u} {R : Type v} [Zero R] (x y : FreeModule α R) : (∀ (n : ℕ), AgreeUpToOrder x y n) ↔ x = y

theorem BSeries.PLTree.AgreeUpToOrder.eq_of_supportedUpToOrder {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {n : ℕ} (h : AgreeUpToOrder x y n) (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : x = y

theorem BSeries.PLTree.HomogeneousOfOrder.add {α : Type u} {R : Type v} [AddMonoid R] {x y : FreeModule α R} {n : ℕ} (hx : HomogeneousOfOrder x n) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (x + y) n

theorem BSeries.PLTree.SupportedUpToOrder.add {α : Type u} {R : Type v} [AddMonoid R] {x y : FreeModule α R} {n : ℕ} (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (x + y) n

theorem BSeries.PLTree.HomogeneousOfOrder.smul {α : Type u} {S : Type w} {R : Type v} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule α R} {n : ℕ} (h : HomogeneousOfOrder x n) : HomogeneousOfOrder (c • x) n

theorem BSeries.PLTree.SupportedUpToOrder.smul {α : Type u} {S : Type w} {R : Type v} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule α R} {n : ℕ} (h : SupportedUpToOrder x n) : SupportedUpToOrder (c • x) n

theorem BSeries.PLTree.supportedUpToOrder_single_of_le {α : Type u} (R : Type v) [Zero R] {s : HopfAlgebras.PLTree α} {n : ℕ} (a : R) (hs : s.order ≤ n) : SupportedUpToOrder (Finsupp.single s a) n

noncomputable def BSeries.PLTree.preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : FreeModule α R

The formal sum of all labelled planar grafts of s at one vertex of t.

Equations

• BSeries.PLTree.preLieVector R s t = (List.map (fun (u : HopfAlgebras.PLTree α) => Finsupp.single u 1) (BSeries.PLTree.preLieGrafts s t)).sum

theorem BSeries.PLTree.preLieVector_apply {α : Type u} (R : Type v) [Semiring R] (s t u : HopfAlgebras.PLTree α) : (preLieVector R s t) u = ↑(List.count u (preLieGrafts s t))

theorem BSeries.PLTree.preLieVector_apply_eq_zero_of_order_ne {α : Type u} (R : Type v) [Semiring R] (s t u : HopfAlgebras.PLTree α) (h : ¬u.order = s.order + t.order) : (preLieVector R s t) u = 0

theorem BSeries.PLTree.order_of_mem_support_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t u : HopfAlgebras.PLTree α) (hu : u ∈ (preLieVector R s t).support) : u.order = s.order + t.order

theorem BSeries.PLTree.homogeneousOfOrder_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : HomogeneousOfOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.PLTree.supportedUpToOrder_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : SupportedUpToOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.PLTree.mapDomain_sum_single {α : Type u} {β : Type w} (R : Type v) [Semiring R] (f : HopfAlgebras.PLTree α → β) (ts : List (HopfAlgebras.PLTree α)) : Finsupp.mapDomain f (List.map (fun (u : HopfAlgebras.PLTree α) => Finsupp.single u 1) ts).sum = (List.map (fun (u : HopfAlgebras.PLTree α) => Finsupp.single (f u) 1) ts).sum

noncomputable def BSeries.PLTree.preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) : FreeModule α R

Bilinear extension of labelled planar pre-Lie grafting.

Equations

• BSeries.PLTree.preLie R x y = Finsupp.sum x fun (s : HopfAlgebras.PLTree α) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PLTree α) (b : R) => (a * b) • BSeries.PLTree.preLieVector R s t

theorem BSeries.PLTree.preLie_apply {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) : (preLie R x y) u = Finsupp.sum x fun (s : HopfAlgebras.PLTree α) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PLTree α) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))

theorem BSeries.PLTree.preLie_apply_eq_zero_of_forall_order_ne {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (preLie R x y) u = 0

theorem BSeries.PLTree.exists_order_eq_of_mem_support_preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) (hu : u ∈ (preLie R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.PLTree.HomogeneousOfOrder.preLie {α : Type u} (R : Type v) [Semiring R] {x y : FreeModule α R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (PLTree.preLie R x y) (m + n)

theorem BSeries.PLTree.SupportedUpToOrder.preLie {α : Type u} (R : Type v) [Semiring R] {x y : FreeModule α R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (PLTree.preLie R x y) (m + n)

@[simp]

theorem BSeries.PLTree.preLie_zero_left {α : Type u} (R : Type v) [Semiring R] (x : FreeModule α R) : preLie R 0 x = 0

@[simp]

theorem BSeries.PLTree.preLie_zero_right {α : Type u} (R : Type v) [Semiring R] (x : FreeModule α R) : preLie R x 0 = 0

theorem BSeries.PLTree.preLie_add_left {α : Type u} (R : Type v) [Semiring R] (x y z : FreeModule α R) : preLie R (x + y) z = preLie R x z + preLie R y z

theorem BSeries.PLTree.preLie_add_right {α : Type u} (R : Type v) [Semiring R] (x y z : FreeModule α R) : preLie R x (y + z) = preLie R x y + preLie R x z

theorem BSeries.PLTree.preLie_smul_left {α : Type u} (R : Type v) [Semiring R] (c : R) (x y : FreeModule α R) : preLie R (c • x) y = c • preLie R x y

theorem BSeries.PLTree.preLie_smul_right {α : Type u} (R : Type v) [CommSemiring R] (c : R) (x y : FreeModule α R) : preLie R x (c • y) = c • preLie R x y

theorem BSeries.PLTree.preLie_single_single {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) (a b : R) : preLie R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t

@[simp]

theorem BSeries.PLTree.preLie_single_single_one {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : preLie R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t

noncomputable def BSeries.PLTree.lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : FreeModule α R

The commutator bracket induced by labelled planar pre-Lie grafting.

Equations

• BSeries.PLTree.lieBracket R x y = BSeries.PLTree.preLie R x y - BSeries.PLTree.preLie R y x

theorem BSeries.PLTree.lieBracket_apply {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) : (lieBracket R x y) u = (Finsupp.sum x fun (s : HopfAlgebras.PLTree α) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.PLTree α) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))) - Finsupp.sum y fun (s : HopfAlgebras.PLTree α) (a : R) => Finsupp.sum x fun (t : HopfAlgebras.PLTree α) (b : R) => a * b * ↑(List.count u (preLieGrafts s t))

theorem BSeries.PLTree.lieBracket_apply_eq_zero_of_forall_order_ne {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (lieBracket R x y) u = 0

theorem BSeries.PLTree.exists_order_eq_of_mem_support_lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.PLTree α) (hu : u ∈ (lieBracket R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.PLTree.HomogeneousOfOrder.lieBracket {α : Type u} (R : Type v) [Ring R] {x y : FreeModule α R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (PLTree.lieBracket R x y) (m + n)

theorem BSeries.PLTree.SupportedUpToOrder.lieBracket {α : Type u} (R : Type v) [Ring R] {x y : FreeModule α R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (PLTree.lieBracket R x y) (m + n)

@[simp]

theorem BSeries.PLTree.lieBracket_zero_left {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R 0 x = 0

@[simp]

theorem BSeries.PLTree.lieBracket_zero_right {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R x 0 = 0

@[simp]

theorem BSeries.PLTree.lieBracket_self {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R x x = 0

theorem BSeries.PLTree.lieBracket_skew {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : lieBracket R x y = -lieBracket R y x

theorem BSeries.PLTree.lieBracket_add_left {α : Type u} (R : Type v) [Ring R] (x y z : FreeModule α R) : lieBracket R (x + y) z = lieBracket R x z + lieBracket R y z

theorem BSeries.PLTree.lieBracket_add_right {α : Type u} (R : Type v) [Ring R] (x y z : FreeModule α R) : lieBracket R x (y + z) = lieBracket R x y + lieBracket R x z

theorem BSeries.PLTree.lieBracket_smul_left {α : Type u} (R : Type v) [CommRing R] (c : R) (x y : FreeModule α R) : lieBracket R (c • x) y = c • lieBracket R x y

theorem BSeries.PLTree.lieBracket_smul_right {α : Type u} (R : Type v) [CommRing R] (c : R) (x y : FreeModule α R) : lieBracket R x (c • y) = c • lieBracket R x y

theorem BSeries.PLTree.lieBracket_single_single {α : Type u} (R : Type v) [Ring R] (s t : HopfAlgebras.PLTree α) (a b : R) : lieBracket R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t - (b * a) • preLieVector R t s

@[simp]

theorem BSeries.PLTree.lieBracket_single_single_one {α : Type u} (R : Type v) [Ring R] (s t : HopfAlgebras.PLTree α) : lieBracket R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t - preLieVector R t s

@[simp]

theorem BSeries.PLTree.erase_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : Finsupp.mapDomain HopfAlgebras.PLTree.erase (preLieVector R s t) = PTree.preLieVector R s.erase t.erase

@[simp]

theorem BSeries.PLTree.map_preLieVector {α : Type u} {β : Type w} (R : Type v) [Semiring R] (f : α → β) (s t : HopfAlgebras.PLTree α) : Finsupp.mapDomain (HopfAlgebras.PLTree.map f) (preLieVector R s t) = preLieVector R (HopfAlgebras.PLTree.map f s) (HopfAlgebras.PLTree.map f t)

@[simp]

theorem BSeries.PLTree.constLabel_preLieVector {α : Type u} (R : Type v) [Semiring R] (a : α) (s t : HopfAlgebras.PTree) : Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) (PTree.preLieVector R s t) = preLieVector R (HopfAlgebras.PLTree.constLabel a s) (HopfAlgebras.PLTree.constLabel a t)

@[simp]

theorem BSeries.PLTree.erase_preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) : Finsupp.mapDomain HopfAlgebras.PLTree.erase (preLie R x y) = PTree.preLie R (Finsupp.mapDomain HopfAlgebras.PLTree.erase x) (Finsupp.mapDomain HopfAlgebras.PLTree.erase y)

@[simp]

theorem BSeries.PLTree.map_preLie {α : Type u} {β : Type w} (R : Type v) [Semiring R] (f : α → β) (x y : FreeModule α R) : Finsupp.mapDomain (HopfAlgebras.PLTree.map f) (preLie R x y) = preLie R (Finsupp.mapDomain (HopfAlgebras.PLTree.map f) x) (Finsupp.mapDomain (HopfAlgebras.PLTree.map f) y)

@[simp]

theorem BSeries.PLTree.constLabel_preLie {α : Type u} (R : Type v) [Semiring R] (a : α) (x y : PTree.FreeModule R) : Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) (PTree.preLie R x y) = preLie R (Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) x) (Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) y)

@[simp]

theorem BSeries.PLTree.erase_lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : Finsupp.mapDomain HopfAlgebras.PLTree.erase (lieBracket R x y) = PTree.lieBracket R (Finsupp.mapDomain HopfAlgebras.PLTree.erase x) (Finsupp.mapDomain HopfAlgebras.PLTree.erase y)

@[simp]

theorem BSeries.PLTree.map_lieBracket {α : Type u} {β : Type w} (R : Type v) [Ring R] (f : α → β) (x y : FreeModule α R) : Finsupp.mapDomain (HopfAlgebras.PLTree.map f) (lieBracket R x y) = lieBracket R (Finsupp.mapDomain (HopfAlgebras.PLTree.map f) x) (Finsupp.mapDomain (HopfAlgebras.PLTree.map f) y)

@[simp]

theorem BSeries.PLTree.constLabel_lieBracket {α : Type u} (R : Type v) [Ring R] (a : α) (x y : PTree.FreeModule R) : Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) (PTree.lieBracket R x y) = lieBracket R (Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) x) (Finsupp.mapDomain (HopfAlgebras.PLTree.constLabel a) y)

@[reducible, inline]

abbrev BSeries.LRootedTree.FreeModule (α : Type u) (R : Type v) [Zero R] : Type (max u v)

Finitely supported formal sums of non-planar labelled rooted trees.

Equations

• BSeries.LRootedTree.FreeModule α R = (HopfAlgebras.LRootedTree α →₀ R)

def BSeries.LRootedTree.HomogeneousOfOrder {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : Prop

A non-planar labelled formal tree sum supported only on trees of order n.

Equations

• BSeries.LRootedTree.HomogeneousOfOrder x n = ∀ u ∈ x.support, u.order = n

def BSeries.LRootedTree.SupportedUpToOrder {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : Prop

A non-planar labelled formal tree sum supported only on trees of order at most n.

Equations

• BSeries.LRootedTree.SupportedUpToOrder x n = ∀ u ∈ x.support, u.order ≤ n

@[simp]

theorem BSeries.LRootedTree.homogeneousOfOrder_zero {α : Type u} (R : Type v) [Zero R] (n : ℕ) : HomogeneousOfOrder 0 n

theorem BSeries.LRootedTree.homogeneousOfOrder_single {α : Type u} (R : Type v) [Zero R] (s : HopfAlgebras.LRootedTree α) (a : R) : HomogeneousOfOrder (Finsupp.single s a) s.order

@[simp]

theorem BSeries.LRootedTree.supportedUpToOrder_zero {α : Type u} (R : Type v) [Zero R] (n : ℕ) : SupportedUpToOrder 0 n

theorem BSeries.LRootedTree.HomogeneousOfOrder.supportedUpToOrder {α : Type u} {R : Type v} [Zero R] {x : FreeModule α R} {n : ℕ} (h : HomogeneousOfOrder x n) : SupportedUpToOrder x n

theorem BSeries.LRootedTree.SupportedUpToOrder.mono {α : Type u} {R : Type v} [Zero R] {x : FreeModule α R} {m n : ℕ} (h : SupportedUpToOrder x m) (hmn : m ≤ n) : SupportedUpToOrder x n

def BSeries.LRootedTree.AgreeUpToOrder {α : Type u} {R : Type v} [Zero R] (x y : FreeModule α R) (n : ℕ) : Prop

Two non-planar labelled formal tree sums have equal coefficients through order n.

Equations

• BSeries.LRootedTree.AgreeUpToOrder x y n = ∀ (u : HopfAlgebras.LRootedTree α), u.order ≤ n → x u = y u

theorem BSeries.LRootedTree.agreeUpToOrder_refl {α : Type u} {R : Type v} [Zero R] (x : FreeModule α R) (n : ℕ) : AgreeUpToOrder x x n

theorem BSeries.LRootedTree.AgreeUpToOrder.symm {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {n : ℕ} (h : AgreeUpToOrder x y n) : AgreeUpToOrder y x n

theorem BSeries.LRootedTree.AgreeUpToOrder.trans {α : Type u} {R : Type v} [Zero R] {x y z : FreeModule α R} {n : ℕ} (hxy : AgreeUpToOrder x y n) (hyz : AgreeUpToOrder y z n) : AgreeUpToOrder x z n

theorem BSeries.LRootedTree.AgreeUpToOrder.mono {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {m n : ℕ} (h : AgreeUpToOrder x y n) (hmn : m ≤ n) : AgreeUpToOrder x y m

theorem BSeries.LRootedTree.agreeUpToOrder_all_iff_eq {α : Type u} {R : Type v} [Zero R] (x y : FreeModule α R) : (∀ (n : ℕ), AgreeUpToOrder x y n) ↔ x = y

theorem BSeries.LRootedTree.AgreeUpToOrder.eq_of_supportedUpToOrder {α : Type u} {R : Type v} [Zero R] {x y : FreeModule α R} {n : ℕ} (h : AgreeUpToOrder x y n) (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : x = y

theorem BSeries.LRootedTree.HomogeneousOfOrder.add {α : Type u} {R : Type v} [AddMonoid R] {x y : FreeModule α R} {n : ℕ} (hx : HomogeneousOfOrder x n) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (x + y) n

theorem BSeries.LRootedTree.SupportedUpToOrder.add {α : Type u} {R : Type v} [AddMonoid R] {x y : FreeModule α R} {n : ℕ} (hx : SupportedUpToOrder x n) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (x + y) n

theorem BSeries.LRootedTree.HomogeneousOfOrder.smul {α : Type u} {S : Type w} {R : Type v} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule α R} {n : ℕ} (h : HomogeneousOfOrder x n) : HomogeneousOfOrder (c • x) n

theorem BSeries.LRootedTree.SupportedUpToOrder.smul {α : Type u} {S : Type w} {R : Type v} [Zero R] [SMulZeroClass S R] (c : S) {x : FreeModule α R} {n : ℕ} (h : SupportedUpToOrder x n) : SupportedUpToOrder (c • x) n

theorem BSeries.LRootedTree.supportedUpToOrder_single_of_le {α : Type u} (R : Type v) [Zero R] {s : HopfAlgebras.LRootedTree α} {n : ℕ} (a : R) (hs : s.order ≤ n) : SupportedUpToOrder (Finsupp.single s a) n

noncomputable def BSeries.LRootedTree.preLieVectorOfPLTree {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : FreeModule α R

Equations

• BSeries.LRootedTree.preLieVectorOfPLTree R s t = (List.map (fun (u : HopfAlgebras.PLTree α) => Finsupp.single (HopfAlgebras.LRootedTree.ofPLTree u) 1) (BSeries.PLTree.preLieGrafts s t)).sum

theorem BSeries.LRootedTree.preLieVectorOfPLTree_apply {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) (u : HopfAlgebras.LRootedTree α) : (preLieVectorOfPLTree R s t) u = ↑(List.count u (List.map HopfAlgebras.LRootedTree.ofPLTree (PLTree.preLieGrafts s t)))

theorem BSeries.LRootedTree.preLieVectorOfPLTree_apply_eq_zero_of_order_ne {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) (u : HopfAlgebras.LRootedTree α) (h : ¬u.order = (HopfAlgebras.LRootedTree.ofPLTree s).order + (HopfAlgebras.LRootedTree.ofPLTree t).order) : (preLieVectorOfPLTree R s t) u = 0

theorem BSeries.LRootedTree.preLieVectorOfPLTree_perm_left {α : Type u} (R : Type v) [Semiring R] {s s' : HopfAlgebras.PLTree α} (hs : s.Perm s') (t : HopfAlgebras.PLTree α) : preLieVectorOfPLTree R s t = preLieVectorOfPLTree R s' t

theorem BSeries.LRootedTree.preLieVectorOfPLTree_perm_right {α : Type u} (R : Type v) [Semiring R] (s : HopfAlgebras.PLTree α) {t t' : HopfAlgebras.PLTree α} (ht : t.Perm t') : preLieVectorOfPLTree R s t = preLieVectorOfPLTree R s t'

noncomputable def BSeries.LRootedTree.preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) : FreeModule α R

The formal sum of all non-planar labelled grafts of one tree at another.

Equations

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

@[simp]

theorem BSeries.LRootedTree.preLieVector_ofPLTree {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : preLieVector R (HopfAlgebras.LRootedTree.ofPLTree s) (HopfAlgebras.LRootedTree.ofPLTree t) = preLieVectorOfPLTree R s t

@[simp]

theorem BSeries.LRootedTree.mapDomain_ofPLTree_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.PLTree α) : Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree (PLTree.preLieVector R s t) = preLieVector R (HopfAlgebras.LRootedTree.ofPLTree s) (HopfAlgebras.LRootedTree.ofPLTree t)

@[simp]

theorem BSeries.LRootedTree.erase_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) : Finsupp.mapDomain HopfAlgebras.LRootedTree.erase (preLieVector R s t) = RootedTree.preLieVector R s.erase t.erase

@[simp]

theorem BSeries.LRootedTree.map_preLieVector {α : Type u} {β : Type w} (R : Type v) [Semiring R] (f : α → β) (s t : HopfAlgebras.LRootedTree α) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) (preLieVector R s t) = preLieVector R (HopfAlgebras.LRootedTree.map f s) (HopfAlgebras.LRootedTree.map f t)

@[simp]

theorem BSeries.LRootedTree.constLabel_preLieVector {α : Type u} (R : Type v) [Semiring R] (a : α) (s t : HopfAlgebras.RootedTree) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) (RootedTree.preLieVector R s t) = preLieVector R (HopfAlgebras.LRootedTree.constLabel a s) (HopfAlgebras.LRootedTree.constLabel a t)

theorem BSeries.LRootedTree.preLieVector_apply_eq_zero_of_order_ne {α : Type u} (R : Type v) [Semiring R] (s t u : HopfAlgebras.LRootedTree α) (h : ¬u.order = s.order + t.order) : (preLieVector R s t) u = 0

theorem BSeries.LRootedTree.order_of_mem_support_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t u : HopfAlgebras.LRootedTree α) (hu : u ∈ (preLieVector R s t).support) : u.order = s.order + t.order

theorem BSeries.LRootedTree.homogeneousOfOrder_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) : HomogeneousOfOrder (preLieVector R s t) (s.order + t.order)

theorem BSeries.LRootedTree.supportedUpToOrder_preLieVector {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) : SupportedUpToOrder (preLieVector R s t) (s.order + t.order)

noncomputable def BSeries.LRootedTree.preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) : FreeModule α R

Bilinear extension of non-planar labelled pre-Lie grafting to formal tree sums.

Equations

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

theorem BSeries.LRootedTree.preLie_apply {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) : (preLie R x y) u = Finsupp.sum x fun (s : HopfAlgebras.LRootedTree α) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.LRootedTree α) (b : R) => a * b * (preLieVector R s t) u

theorem BSeries.LRootedTree.preLie_apply_eq_zero_of_forall_order_ne {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (preLie R x y) u = 0

theorem BSeries.LRootedTree.exists_order_eq_of_mem_support_preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) (hu : u ∈ (preLie R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.LRootedTree.HomogeneousOfOrder.preLie {α : Type u} (R : Type v) [Semiring R] {x y : FreeModule α R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (LRootedTree.preLie R x y) (m + n)

theorem BSeries.LRootedTree.SupportedUpToOrder.preLie {α : Type u} (R : Type v) [Semiring R] {x y : FreeModule α R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (LRootedTree.preLie R x y) (m + n)

@[simp]

theorem BSeries.LRootedTree.preLie_zero_left {α : Type u} (R : Type v) [Semiring R] (x : FreeModule α R) : preLie R 0 x = 0

@[simp]

theorem BSeries.LRootedTree.preLie_zero_right {α : Type u} (R : Type v) [Semiring R] (x : FreeModule α R) : preLie R x 0 = 0

theorem BSeries.LRootedTree.preLie_add_left {α : Type u} (R : Type v) [Semiring R] (x y z : FreeModule α R) : preLie R (x + y) z = preLie R x z + preLie R y z

theorem BSeries.LRootedTree.preLie_add_right {α : Type u} (R : Type v) [Semiring R] (x y z : FreeModule α R) : preLie R x (y + z) = preLie R x y + preLie R x z

theorem BSeries.LRootedTree.preLie_smul_left {α : Type u} (R : Type v) [Semiring R] (c : R) (x y : FreeModule α R) : preLie R (c • x) y = c • preLie R x y

theorem BSeries.LRootedTree.preLie_smul_right {α : Type u} (R : Type v) [CommSemiring R] (c : R) (x y : FreeModule α R) : preLie R x (c • y) = c • preLie R x y

theorem BSeries.LRootedTree.preLie_single_single {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) (a b : R) : preLie R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t

@[simp]

theorem BSeries.LRootedTree.preLie_single_single_one {α : Type u} (R : Type v) [Semiring R] (s t : HopfAlgebras.LRootedTree α) : preLie R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t

@[simp]

theorem BSeries.LRootedTree.mapDomain_ofPLTree_preLie {α : Type u} (R : Type v) [Semiring R] (x y : PLTree.FreeModule α R) : Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree (PLTree.preLie R x y) = preLie R (Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree x) (Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree y)

@[simp]

theorem BSeries.LRootedTree.erase_preLie {α : Type u} (R : Type v) [Semiring R] (x y : FreeModule α R) : Finsupp.mapDomain HopfAlgebras.LRootedTree.erase (preLie R x y) = RootedTree.preLie R (Finsupp.mapDomain HopfAlgebras.LRootedTree.erase x) (Finsupp.mapDomain HopfAlgebras.LRootedTree.erase y)

@[simp]

theorem BSeries.LRootedTree.map_preLie {α : Type u} {β : Type w} (R : Type v) [Semiring R] (f : α → β) (x y : FreeModule α R) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) (preLie R x y) = preLie R (Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) x) (Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) y)

@[simp]

theorem BSeries.LRootedTree.constLabel_preLie {α : Type u} (R : Type v) [Semiring R] (a : α) (x y : RootedTree.FreeModule R) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) (RootedTree.preLie R x y) = preLie R (Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) x) (Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) y)

noncomputable def BSeries.LRootedTree.lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : FreeModule α R

The commutator bracket induced by non-planar labelled pre-Lie grafting.

Equations

• BSeries.LRootedTree.lieBracket R x y = BSeries.LRootedTree.preLie R x y - BSeries.LRootedTree.preLie R y x

theorem BSeries.LRootedTree.lieBracket_apply {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) : (lieBracket R x y) u = (Finsupp.sum x fun (s : HopfAlgebras.LRootedTree α) (a : R) => Finsupp.sum y fun (t : HopfAlgebras.LRootedTree α) (b : R) => a * b * (preLieVector R s t) u) - Finsupp.sum y fun (s : HopfAlgebras.LRootedTree α) (a : R) => Finsupp.sum x fun (t : HopfAlgebras.LRootedTree α) (b : R) => a * b * (preLieVector R s t) u

theorem BSeries.LRootedTree.lieBracket_apply_eq_zero_of_forall_order_ne {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) (h : ∀ s ∈ x.support, ∀ t ∈ y.support, ¬u.order = s.order + t.order) : (lieBracket R x y) u = 0

theorem BSeries.LRootedTree.exists_order_eq_of_mem_support_lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) (u : HopfAlgebras.LRootedTree α) (hu : u ∈ (lieBracket R x y).support) : ∃ s ∈ x.support, ∃ t ∈ y.support, u.order = s.order + t.order

theorem BSeries.LRootedTree.HomogeneousOfOrder.lieBracket {α : Type u} (R : Type v) [Ring R] {x y : FreeModule α R} {m n : ℕ} (hx : HomogeneousOfOrder x m) (hy : HomogeneousOfOrder y n) : HomogeneousOfOrder (LRootedTree.lieBracket R x y) (m + n)

theorem BSeries.LRootedTree.SupportedUpToOrder.lieBracket {α : Type u} (R : Type v) [Ring R] {x y : FreeModule α R} {m n : ℕ} (hx : SupportedUpToOrder x m) (hy : SupportedUpToOrder y n) : SupportedUpToOrder (LRootedTree.lieBracket R x y) (m + n)

@[simp]

theorem BSeries.LRootedTree.lieBracket_zero_left {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R 0 x = 0

@[simp]

theorem BSeries.LRootedTree.lieBracket_zero_right {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R x 0 = 0

@[simp]

theorem BSeries.LRootedTree.lieBracket_self {α : Type u} (R : Type v) [Ring R] (x : FreeModule α R) : lieBracket R x x = 0

theorem BSeries.LRootedTree.lieBracket_skew {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : lieBracket R x y = -lieBracket R y x

theorem BSeries.LRootedTree.lieBracket_add_left {α : Type u} (R : Type v) [Ring R] (x y z : FreeModule α R) : lieBracket R (x + y) z = lieBracket R x z + lieBracket R y z

theorem BSeries.LRootedTree.lieBracket_add_right {α : Type u} (R : Type v) [Ring R] (x y z : FreeModule α R) : lieBracket R x (y + z) = lieBracket R x y + lieBracket R x z

theorem BSeries.LRootedTree.lieBracket_smul_left {α : Type u} (R : Type v) [CommRing R] (c : R) (x y : FreeModule α R) : lieBracket R (c • x) y = c • lieBracket R x y

theorem BSeries.LRootedTree.lieBracket_smul_right {α : Type u} (R : Type v) [CommRing R] (c : R) (x y : FreeModule α R) : lieBracket R x (c • y) = c • lieBracket R x y

theorem BSeries.LRootedTree.lieBracket_single_single {α : Type u} (R : Type v) [Ring R] (s t : HopfAlgebras.LRootedTree α) (a b : R) : lieBracket R (Finsupp.single s a) (Finsupp.single t b) = (a * b) • preLieVector R s t - (b * a) • preLieVector R t s

@[simp]

theorem BSeries.LRootedTree.lieBracket_single_single_one {α : Type u} (R : Type v) [Ring R] (s t : HopfAlgebras.LRootedTree α) : lieBracket R (Finsupp.single s 1) (Finsupp.single t 1) = preLieVector R s t - preLieVector R t s

@[simp]

theorem BSeries.LRootedTree.mapDomain_ofPLTree_lieBracket {α : Type u} (R : Type v) [Ring R] (x y : PLTree.FreeModule α R) : Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree (PLTree.lieBracket R x y) = lieBracket R (Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree x) (Finsupp.mapDomain HopfAlgebras.LRootedTree.ofPLTree y)

@[simp]

theorem BSeries.LRootedTree.erase_lieBracket {α : Type u} (R : Type v) [Ring R] (x y : FreeModule α R) : Finsupp.mapDomain HopfAlgebras.LRootedTree.erase (lieBracket R x y) = RootedTree.lieBracket R (Finsupp.mapDomain HopfAlgebras.LRootedTree.erase x) (Finsupp.mapDomain HopfAlgebras.LRootedTree.erase y)

@[simp]

theorem BSeries.LRootedTree.map_lieBracket {α : Type u} {β : Type w} (R : Type v) [Ring R] (f : α → β) (x y : FreeModule α R) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) (lieBracket R x y) = lieBracket R (Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) x) (Finsupp.mapDomain (HopfAlgebras.LRootedTree.map f) y)

@[simp]

theorem BSeries.LRootedTree.constLabel_lieBracket {α : Type u} (R : Type v) [Ring R] (a : α) (x y : RootedTree.FreeModule R) : Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) (RootedTree.lieBracket R x y) = lieBracket R (Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) x) (Finsupp.mapDomain (HopfAlgebras.LRootedTree.constLabel a) y)