Homogeneous components of the Connes–Kreimer algebra

As an algebra, ConnesKreimer R T is the polynomial algebra in the trees, graded by the number of trees in a forest. homogeneousComponent k projects onto the span of the forests with k trees, as MvPolynomial.homogeneousComponent does for total degree.

Main declarations

• ConnesKreimer.homogeneousComponent k: the projection onto the forests with k trees.
• ConnesKreimer.homogeneousComponent_comp_homogeneousComponent: the projections are orthogonal idempotents.

Implementation notes

The grading is by number of trees, not by number of vertices. A grading by vertices would be a weighted version (MvPolynomial.weightedHomogeneousComponent), with each tree weighted by its size.

References

• [CK98]

noncomputable def ConnesKreimer.homogeneousComponent {R : Type u_1} [CommSemiring R] {T : Type u_2} (k : ℕ) : ConnesKreimer R T →ₗ[R] ConnesKreimer R T

The degree-k homogeneous component is the projection onto the span of the forests with exactly k trees.

Equations

• ConnesKreimer.homogeneousComponent k = ConnesKreimer.linearLift fun (F : UnorderedTree.Forest T) => if Multiset.card F = k then ConnesKreimer.of' F else 0

@[simp]

theorem ConnesKreimer.homogeneousComponent_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (k : ℕ) (F : UnorderedTree.Forest T) : (homogeneousComponent k) (of' F) = if Multiset.card F = k then of' F else 0

@[simp]

theorem ConnesKreimer.homogeneousComponent_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (k : ℕ) (t : T) : (homogeneousComponent k) (ofTree t) = if 1 = k then ofTree t else 0

@[simp]

theorem ConnesKreimer.homogeneousComponent_one {R : Type u_1} [CommSemiring R] {T : Type u_2} (k : ℕ) : (homogeneousComponent k) 1 = if 0 = k then 1 else 0

theorem ConnesKreimer.homogeneousComponent_comp_homogeneousComponent {R : Type u_1} [CommSemiring R] {T : Type u_2} (j k : ℕ) : homogeneousComponent j ∘ₗ homogeneousComponent k = if j = k then homogeneousComponent k else 0