inductive CK.Coassoc.RTree : Type

Planar rooted trees, represented by the forest of children below the root.

• node : List RTree → RTree

@[implicit_reducible]

instance CK.Coassoc.instReprRTree : Repr RTree

Equations

• CK.Coassoc.instReprRTree = { reprPrec := CK.Coassoc.instReprRTree.repr }

partial def CK.Coassoc.instReprRTree.repr : RTree → Nat → Std.Format

@[implicit_reducible]

instance CK.Coassoc.instInhabitedRTree : Inhabited RTree

Equations

• CK.Coassoc.instInhabitedRTree = { default := CK.Coassoc.instInhabitedRTree.default }

@[reducible, inline]

abbrev CK.Coassoc.Forest : Type

A planar rooted forest is a list of planar rooted trees.

Equations

• CK.Coassoc.Forest = List CK.Coassoc.RTree

@[reducible, inline]

abbrev CK.Coassoc.Tens : Type

Formal sums of coproduct tensor monomials, represented by their forest pairs.

Equations

• CK.Coassoc.Tens = List (CK.Coassoc.Forest × CK.Coassoc.Forest)

def CK.Coassoc.tmul (x y : Tens) : Tens

product on H⊗H, leg-wise forest product (R1 planar: list append).

Equations

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

def CK.Coassoc.coprodTree : RTree → Tens

The Connes-Kreimer coproduct on one rooted tree, as a formal list of tensor terms.

Equations

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

def CK.Coassoc.coprodForest : Forest → Tens

The multiplicative extension of the coproduct from trees to forests.

Equations

• CK.Coassoc.coprodForest [] = [([], [])]
• CK.Coassoc.coprodForest (t :: ts) = CK.Coassoc.tmul (CK.Coassoc.coprodTree t) (CK.Coassoc.coprodForest ts)

Easy lemmas: units of tmul.

@[simp]

theorem CK.Coassoc.tmul_unit_left (y : Tens) : tmul [([], [])] y = y

The empty forest [([],[])] is a left unit for tmul, literally.

@[simp]

theorem CK.Coassoc.tmul_unit_right (x : Tens) : tmul x [([], [])] = x

Right unit, up to = via append_nil.

theorem CK.Coassoc.tmul_append_left (x₁ x₂ y : Tens) : tmul (x₁ ++ x₂) y = tmul x₁ y ++ tmul x₂ y

tmul is left-distributive over ++ (formal-sum bilinearity, left).

theorem CK.Coassoc.tmul_cons (p r : Forest) (xs y : Tens) : tmul ((p, r) :: xs) y = List.map (fun (x : Forest × Forest) => match x with | (p', r') => (p ++ p', r ++ r')) y ++ tmul xs y

tmul on a cons unfolds to a map head plus the tail product.

theorem CK.Coassoc.tmul_assoc (x y z : Tens) : tmul (tmul x y) z = tmul x (tmul y z)

tmul is associative, literally (legs by append_assoc, sums by flatMap nesting).

theorem CK.Coassoc.coprodForest_append (F G : Forest) : coprodForest (F ++ G) = tmul (coprodForest F) (coprodForest G)

Multiplicativity of Δ: the coproduct of a forest product is the product of coproducts. Literal = (rides on tmul_assoc + units).

List/Perm plumbing for the Fubini swap (core Lean, no Mathlib).

theorem CK.Coassoc.perm_middle_swap {α : Type u_1} (A B C D : List α) : (A ++ B ++ (C ++ D)).Perm (A ++ C ++ (B ++ D))

(A++B)++(C++D) ~ (A++C)++(B++D): swap the inner two blocks.

theorem CK.Coassoc.flatMap_append_distrib {α : Type u_1} {β : Type u_2} (l : List α) (X Y : α → List β) : (List.flatMap (fun (a : α) => X a ++ Y a) l).Perm (List.flatMap X l ++ List.flatMap Y l)

flatMap distributes over a pointwise append, up to Perm.

theorem CK.Coassoc.flatMap_const_nil {α : Type u_1} {β : Type u_2} (l : List α) : List.flatMap (fun (x : α) => []) l = []

flatMap of a constantly-empty function is empty.

theorem CK.Coassoc.flatMap_singleton_eq_map {α : Type u_1} {β : Type u_2} (g : α → β) (l : List α) : List.flatMap (fun (a : α) => [g a]) l = List.map g l

flatMap of a singleton-valued function is a map.

theorem CK.Coassoc.flatMap_comm {α : Type u_1} {β : Type u_2} {γ : Type u_3} (l1 : List α) (l2 : List β) (f : α → β → List γ) : (List.flatMap (fun (a : α) => List.flatMap (fun (b : β) => f a b) l2) l1).Perm (List.flatMap (fun (b : β) => List.flatMap (fun (a : α) => f a b) l1) l2)

Fubini: two independent nested flatMaps commute, up to Perm.

theorem CK.Coassoc.Perm.flatMap_congr_right {α : Type u_1} {β : Type u_2} (l : List α) {f g : α → List β} (h : ∀ (a : α), (f a).Perm (g a)) : (List.flatMap f l).Perm (List.flatMap g l)

Congruence: pointwise-Perm inner functions give Perm flatMaps (over the same list).

Coassociativity. Δ³ two ways; equal as formal sums (List.Perm).

@[reducible, inline]

abbrev CK.Coassoc.Tens3 : Type

Formal sums of triple tensor monomials, represented by forest triples.

Equations

• CK.Coassoc.Tens3 = List (CK.Coassoc.Forest × CK.Coassoc.Forest × CK.Coassoc.Forest)

def CK.Coassoc.coLeft (x : Tens) : Tens3

(Δ⊗id)∘Δ: expand the LEFT leg of each tensor via coprodForest.

Equations

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

def CK.Coassoc.coRight (x : Tens) : Tens3

(id⊗Δ)∘Δ: expand the RIGHT leg of each tensor via coprodForest.

Equations

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

def CK.Coassoc.tmul3 (x y : Tens3) : Tens3

leg-wise product on triple tensors (R1 planar: list append on each of the 3 legs).

Equations

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

theorem CK.Coassoc.coLeft_tmul (x y : Tens) : List.Perm (coLeft (tmul x y)) (tmul3 (coLeft x) (coLeft y))

coLeft is a coalgebra-style morphism for tmul → tmul3, up to Perm.

theorem CK.Coassoc.coRight_tmul (x y : Tens) : List.Perm (coRight (tmul x y)) (tmul3 (coRight x) (coRight y))

coRight likewise.

theorem CK.Coassoc.coprodTree_node (F : Forest) : coprodTree (RTree.node F) = ([RTree.node F], []) :: List.map (fun (pr : Forest × Forest) => (pr.fst, [RTree.node pr.snd])) (coprodForest F)

Unfold the tree coproduct (the B₊ cocycle), as a simp lemma.

theorem CK.Coassoc.coprodForest_single (t : RTree) : coprodForest [t] = coprodTree t

A singleton forest's coproduct is the tree coproduct.

theorem CK.Coassoc.tmul3_perm {a a' b b' : Tens3} (ha : List.Perm a a') (hb : List.Perm b b') : List.Perm (tmul3 a b) (tmul3 a' b')

tmul3 respects Perm in both arguments.

theorem CK.Coassoc.coassocTree (t : RTree) : List.Perm (coLeft (coprodTree t)) (coRight (coprodTree t))

Coassociativity on a tree.

theorem CK.Coassoc.coassocForest (F : Forest) : List.Perm (coLeft (coprodForest F)) (coRight (coprodForest F))

Coassociativity on a forest (needed for the mutual recursion).

theorem CK.Coassoc.coprod_coassoc (t : RTree) : List.Perm (coLeft (coprodTree t)) (coRight (coprodTree t))

Coassociativity of the Connes–Kreimer / Foissy (planar) coproduct on rooted trees: (Δ⊗id)∘Δ and (id⊗Δ)∘Δ agree as formal sums (multiset equality / List.Perm). The wall: proven by mutual induction tree↔forest via the B₊ Hochschild-1-cocycle, on top of multiplicativity + a Fubini swap. First formalization in any ITP.