Documentation

Linglib.Core.Algebra.RootedTree.PreLie.InsertionUnordered

UnorderedTree multi-tree insertion #

Lift of RoseTree.Pathed.insertionForest through UnorderedTree.mk.

Given two multisets of nonplanar trees F (host forest) and G (guest forest), UnorderedTree.insertionMultiset F G produces the multiset of all forests obtained by inserting G's trees at vertices of F's trees, summing over all assignments (Foissy 2021 Theorem 5.1).

Main results #

Implementation note #

The implementation uses Multiset.toList + Quotient.out to pick representatives, making it noncomputable. The function value is nonetheless well-defined (classical choice yields a definite element). Stronger invariance theorems (host-Perm invariance lifted to the multiset-output level) would enable a Quotient.liftOn₂-based definition but are deferred — the current API suffices for the GrossmanLarson product's zero-case lemmas.

Import-direction anomaly #

This file lives under Combinatorics/ but imports Linglib.Core.Algebra.RootedTree.PreLie.Insertion (the path-based single/forest insertion operators). The path apparatus currently lives in the Algebra leg; were it to graduate to Combinatorics/, the imports would become strictly hierarchical.

source
noncomputable def UnorderedTree.insertionMultiset {α : Type u_1} (F G : Multiset (UnorderedTree α)) :
Multiset (Multiset (UnorderedTree α))

Multi-tree insertion at the nonplanar level. Given a host forest F and guest forest G (both Multiset (UnorderedTree α)), produces the multiset of all forests obtained by inserting G's trees at vertices of F's trees. Defined via list representatives (Multiset.toList) + tree representatives (Quotient.out) + RoseTree.Pathed.insertionForest.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem UnorderedTree.insertionMultiset_zero_right {α : Type u_1} (F : Multiset (UnorderedTree α)) :
    insertionMultiset F 0 = {F}

    With no guests, the multi-graft leaves F unchanged: insertionMultiset F 0 = {F}.

    source
    theorem UnorderedTree.insertionMultiset_zero_left_of_ne_zero {α : Type u_1} (G : Multiset (UnorderedTree α)) (h : G ≠ 0) :
    insertionMultiset 0 G = 0

    With no host but non-empty guests, no vertices to graft into: insertionMultiset 0 G = 0.

    §2: toList helpers #

    Multiset's toList returns a non-canonical list representative. Two different choices of representative produce Perm-equivalent lists. Below: a Perm bridge between (M + N).toList and M.toList ++ N.toList, and its Q.out-mapped lift to the tree level. Used by insertionMultiset_add_host to bridge (A + B).toList.map Q.out with the disjoint-host concatenation A.toList.map Q.out ++ B.toList.map Q.out.

    source
    theorem Multiset.toList_add_perm {β : Type u_2} (M N : Multiset β) :
    (M + N).toList.Perm (M.toList ++ N.toList)

    (M + N).toList is Perm-equivalent to M.toList ++ N.toList. Both have multiset M + N; Perm follows from Multiset.coe_eq_coe.

    [UPSTREAM] candidate: pure Multiset substrate, no rooted-tree dependencies. Belongs in mathlib's Mathlib.Data.Multiset.Basic alongside Multiset.coe_toList and Multiset.coe_add.

    source
    theorem UnorderedTree.toList_map_quotientOut_add_perm {α : Type u_1} (M N : Multiset (UnorderedTree α)) :
    (List.map Quotient.out (M + N).toList).Perm (List.map Quotient.out M.toList ++ List.map Quotient.out N.toList)

    Quotient.out-mapped lift of Multiset.toList_add_perm: at the tree level, (M + N).toList.map Quotient.out is Perm to M.toList.map Quotient.out ++ N.toList.map Quotient.out.

    source
    theorem UnorderedTree.insertionMultiset_card_eq {α : Type u_2} (A B : Multiset (UnorderedTree α)) {F' : Multiset (UnorderedTree α)} (hF' : F' ∈ insertionMultiset A B) :
    F'.card = A.card

    The insertion multiset preserves cardinality: every forest in insertionMultiset A B has the same cardinality as A.

    Proof: insertionMultiset A B is built from insertionForest (A.toList.map Q.out) (B.toList.map Q.out); every output list L has L.length = (A.toList.map Q.out).length = A.card (via RoseTree.Pathed.insertionForest_length); and the cardinality of the lifted Multiset.ofList (L.map mk) equals L.length.

    §3: Root-value preservation for singleton hosts #

    When the host forest is a single tree {T}, every output forest of insertionMultiset {T} B is a singleton {T'} and T'.rootValue = T.rootValue: grafting guests into a tree only modifies its subtrees, never its root value.

    The proof descends through the tree substrate using RoseTree.Pathed.insertionForest_singleton and multiGraft_node (which preserves the head value by structure).

    source
    theorem UnorderedTree.insertionMultiset_singleton_rootValue {α : Type u_1} (T : UnorderedTree α) (B : Multiset (UnorderedTree α)) {F' : Multiset (UnorderedTree α)} (hF' : F' ∈ insertionMultiset {T} B) :
    ∃ (T' : UnorderedTree α), F' = {T'} ∧ T'.rootValue = T.rootValue

    Singleton-host root preservation: every forest in insertionMultiset {T} B is a singleton {T'} and T'.rootValue = T.rootValue. Descends through insertionForest_singleton + RoseTree.value_multiGraft.

    Insertion into a singleton node host #

    source
    theorem UnorderedTree.insertionMultiset_singleton_node {α : Type u_1} [DecidableEq α] (a : α) (A' B : Multiset (UnorderedTree α)) :
    insertionMultiset {node a A'} B = B.powerset.bind fun (B₁ : Multiset (UnorderedTree α)) => Multiset.map (fun (F' : Multiset (UnorderedTree α)) => {node a (F' + (B - B₁))}) (insertionMultiset A' B₁)

    NIM-level keystone: at the UnorderedTree multi-insertion level, grafting B into the singleton host {node a A'} decomposes by partitioning B's grafting positions into "at the root vertex" (becomes new children) vs "in A's subtrees" (recursive NIM).

    Descent through the quotient: the singleton host's canonical planar representative is Perm-swapped for a visible planar node, RoseTree.Pathed.insertion_node_split provides the root-vs-subtree mask decomposition, and the mask enumeration is converted to the powerset bind via listChoices_bridge_powerset_paired plus the powerset partition involution (the mask convention has true = root guests, while the powerset bind runs over the subtree bucket).

    Disjoint-union hosts, representatives, and iterated grafting #

    Multi-graft into a disjoint-union host decomposes over guest partitions (the combinatorial heart of [OG08] Prop 2.7.iii); insertionMultiset computes on arbitrary RoseTree-level representatives. Proved by descent from the RoseTree.Pathed substrate (InsertionAddHost.lean).

    source
    theorem UnorderedTree.insertionMultiset_add_host {α : Type u_1} [DecidableEq α] (A B C : Multiset (UnorderedTree α)) :
    insertionMultiset (A + B) C = C.powerset.bind fun (C₁ : Multiset (UnorderedTree α)) => Multiset.map (fun (p : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => p.1 + p.2) (insertionMultiset A C₁ ×ˢ insertionMultiset B (C - C₁))

    Split law for multi-graft outputs #

    Splits of a multi-graft output factor through splits of host and guests (each guest follows its host component): the multi-graft counterpart of insertionMultiset_add_host, from which it is proved by induction on the host. Consumed by the pairing product rule for the GL product (GrossmanLarson/PairingMul.lean).

    Helper lemmas #

    A few small multiset/insertion building blocks used by both targets below.

    Split law for multi-graft outputs #

    source
    theorem UnorderedTree.insertionMultiset_antidiagonal {α : Type u_1} [DecidableEq α] (A G : Multiset (UnorderedTree α)) :
    (insertionMultiset A G).bind Multiset.antidiagonal = A.antidiagonal.bind fun (pa : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => G.antidiagonal.bind fun (pg : Multiset (UnorderedTree α) × Multiset (UnorderedTree α)) => insertionMultiset pa.1 pg.1 ×ˢ insertionMultiset pa.2 pg.2

    Splits of an insertion output factor through splits of host and guests. Each component of a multi-graft output X ∈ NIM(A, G) is one host component of A carrying the guests grafted into it, so a sub-multiset split of X induces a split of A and a split of G (guests follow their host), and the correspondence is multiplicity-faithful:

    Σ_{X ∈ NIM(A,G)} Σ_{X = X₁ + X₂} (X₁, X₂) = Σ_{A = A₁+A₂} Σ_{G = G₁+G₂} NIM(A₁,G₁) ×ˢ NIM(A₂,G₂).

    Proved by induction on A from insertionMultiset_add_host (peeling one host tree; NIM({T}, G) outputs are singleton forests, whose antidiagonal is the trivial two-way split).