Single cuts as substitution

Under an extraction policy that replaces every copy of a subtree M by one tree of class R, the cuts of t with crown {M} match the occurrences of M below the root. When M occurs exactly once there, there is exactly one such cut, and its trunk is t with M replaced by R.

Main results

• ConnesKreimer.map_trunk_filter_cutSummandsG: the single cut extracting a subtree that occurs once, with trunk the substitution.

References

• [CK98]

Substitution of a subtree that does not occur

theorem ConnesKreimer.unorderedReplace_of_count_eq_zero {γ : Type u_1} [DecidableEq γ] {M R : UnorderedTree γ} (t : RoseTree γ) : Multiset.count M t.unorderedSubtrees = 0 → RoseTree.unorderedReplace M R t = UnorderedTree.mk t

Substituting for a subtree that does not occur changes nothing.

theorem ConnesKreimer.unorderedReplaceList_of_count_eq_zero {γ : Type u_1} [DecidableEq γ] {M R : UnorderedTree γ} (cs : List (RoseTree γ)) : Multiset.count M (RoseTree.unorderedSubtreesList cs) = 0 → RoseTree.unorderedReplaceList M R cs = ↑(List.map UnorderedTree.mk cs)

Substituting for a subtree that occurs in no tree of a list changes none of them.

The single cut extracting a subtree that occurs once

theorem ConnesKreimer.crown_ne_of_mem_cutListSummandsG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M : UnorderedTree γ} {cs : List (RoseTree γ)} (h : Multiset.count M (RoseTree.unorderedSubtreesList cs) = 0) {q : Multiset (RoseTree γ) × List (RoseTree γ)} (hq : q ∈ cutListSummandsG E cs) : Multiset.map UnorderedTree.mk q.1 ≠ {M}

No crown of a cut of a list of trees is {M} when M occurs in none of them.

theorem ConnesKreimer.crown_ne_of_mem_augActionG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M : UnorderedTree γ} {t : RoseTree γ} (h : Multiset.count M t.unorderedSubtrees = 0) {a : Multiset (RoseTree γ) × List (RoseTree γ)} (ha : a ∈ augActionG E t) : Multiset.map UnorderedTree.mk a.1 ≠ {M}

No crown of a per-child action on t is {M} when M is not a subtree of t.

theorem ConnesKreimer.crown_ne_of_mem_cutSummandsG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M : UnorderedTree γ} {t : RoseTree γ} (h : Multiset.count M (RoseTree.unorderedSubtreesList t.children) = 0) {p : Multiset (RoseTree γ) × RoseTree γ} (hp : p ∈ cutSummandsG E t) : Multiset.map UnorderedTree.mk p.1 ≠ {M}

No crown of a cut of t is {M} when M does not occur below the root.

theorem ConnesKreimer.map_trunk_filter_cutSummandsG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M R : UnorderedTree γ} (hE : ∀ (s : RoseTree γ), UnorderedTree.mk s = M → ∃ (ρ : RoseTree γ), E s = some [ρ] ∧ UnorderedTree.mk ρ = R) (t : RoseTree γ) : Multiset.count M (RoseTree.unorderedSubtreesList t.children) = 1 → UnorderedTree.mk t ≠ M → Multiset.map (fun (p : Multiset (RoseTree γ) × RoseTree γ) => UnorderedTree.mk p.2) (Multiset.filter (fun (p : Multiset (RoseTree γ) × RoseTree γ) => Multiset.map UnorderedTree.mk p.1 = {M}) (cutSummandsG E t)) = {RoseTree.unorderedReplace M R t}

When M occurs exactly once below the root of t, one cut of t has crown {M}, and its trunk is t with M replaced by R.

theorem ConnesKreimer.map_trunk_filter_cutListSummandsG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M R : UnorderedTree γ} (hE : ∀ (s : RoseTree γ), UnorderedTree.mk s = M → ∃ (ρ : RoseTree γ), E s = some [ρ] ∧ UnorderedTree.mk ρ = R) (cs : List (RoseTree γ)) : Multiset.count M (RoseTree.unorderedSubtreesList cs) = 1 → Multiset.map (fun (q : Multiset (RoseTree γ) × List (RoseTree γ)) => ↑(List.map UnorderedTree.mk q.2)) (Multiset.filter (fun (q : Multiset (RoseTree γ) × List (RoseTree γ)) => Multiset.map UnorderedTree.mk q.1 = {M}) (cutListSummandsG E cs)) = {RoseTree.unorderedReplaceList M R cs}

When M occurs exactly once in a list of trees, one cut of the list has crown {M}, and its remainder is the list with M replaced by R.

theorem ConnesKreimer.map_trunk_filter_augActionG {γ : Type u_1} [DecidableEq γ] (E : RoseTree γ → Option (List (RoseTree γ))) {M R : UnorderedTree γ} (hE : ∀ (s : RoseTree γ), UnorderedTree.mk s = M → ∃ (ρ : RoseTree γ), E s = some [ρ] ∧ UnorderedTree.mk ρ = R) (t : RoseTree γ) : Multiset.count M t.unorderedSubtrees = 1 → Multiset.map (fun (q : Multiset (RoseTree γ) × List (RoseTree γ)) => ↑(List.map UnorderedTree.mk q.2)) (Multiset.filter (fun (q : Multiset (RoseTree γ) × List (RoseTree γ)) => Multiset.map UnorderedTree.mk q.1 = {M}) (augActionG E t)) = {{RoseTree.unorderedReplace M R t}}

When M occurs exactly once in t, the per-child actions on t with crown {M} leave t with M replaced by R.