HopfAlgebra R (ConnesKreimer R (Nonplanar α)) — Foissy Connes-Kreimer Hopf algebra

@cite{marcolli-chomsky-berwick-2025} @cite{foissy-introduction-hopf-algebras-trees}

Completes Phase A.7 by upgrading the Bialgebra instance from CoproductNonplanar.lean to a full HopfAlgebra instance via the recursive Foissy / MCB eq. (1.2.12) antipode:

S(x) = -x - Σᵢ S(x'ᵢ) · x''ᵢ (for x of positive weight; reduced coproduct) S(1) = 1

Equivalently, summing over ALL cut summands (including the empty cut (0, T), which contributes ofTree T):

S(T) = -Σ_{(cf, rem) ∈ cutSummandsN T} (Π_{Tᵢ ∈ cf} S(ofTree Tᵢ)) · ofTree rem

Foissy's coassoc closure (in CoproductNonplanar.lean) plus this antipode construction realize MCB Lemma 1.2.11 (book p. 38): the n-ary Connes–Kreimer Hopf algebra of nonplanar rooted trees. Requires CommRing R (the antipode formula uses negation; the Bialgebra instance only needs CommSemiring).

Status

[UPSTREAM] candidate. Sorry-free. The full HopfAlgebra R (ConnesKreimer R (Nonplanar α)) instance is now realized via the right-antipode + WithConv.left_inv_eq_right_inv route — the Sweedler/Kassel argument that mathlib uses internally for IsGroupLikeElem but does not yet expose as a generic constructor. Mathlib has no generic graded-connected bialgebra → Hopf algebra construction (its HopfAlgebra/Basic.lean lists this as TODO); this file is a candidate factoring of Foissy's specific recursion.

Architecture

• Auxiliary depth lemma (cutSummandsN_subtree_depth_lt): every tree appearing in a cut forest of T has strictly smaller depth than T. Lifted from a planar mutual structural-induction proof.
• Auxiliary weight lemma (cutSummandsN_rem_weight_lt): for nontrivial cuts, the remainder has strictly smaller weight than the source. Substrate for the weight-recursive right antipode.
• Multiplicity-1 uniqueness (cutSummandsN_filter_card_zero): the empty cut (0, T) appears with multiplicity exactly 1. Mutual planar structural induction (with auxiliary cutListSummandsP version) plus a multiset_filter_product helper. Substrate for the right-antipode cancellation.
• Antipode on a tree (antipodeTreeN): well-founded recursion on Nonplanar.depth, using the closed form S(T) = -Σ over cutSummandsN T of (Π S(Tᵢ)) · ofTree rem.
• Right antipode (antipodeRightTreeN): well-founded recursion on Nonplanar.weight, using the dual form R(T) = -ofTree T - Σ_{cf ≠ 0} of'(cf) · R(rem). The lTensor cancellation falls out of _unfold plus cutSummandsN_filter_card_zero.
• Antipodes as AlgHoms (antipodeAlgHomN, antipodeRightAlgHomN): multiplicative extension to forests via AddMonoidAlgebra.lift. H is commutative, so both are algebra homs (not just anti-multiplicative).
• rTensor axiom proved by single-step antipodeTreeN_unfold cancellation on trees + Multiset induction on forests.
• lTensor axiom proved by deriving R = antipodeRightAlgHomN satisfies it directly (uniqueness + _unfold), then using WithConv.left_inv_eq_right_inv to conclude S = R as algebra homs.
• HopfAlgebra instance assembled via HopfAlgebra.ofAlgHom.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCommRingNonplanar {R : Type u_1} [CommRing R] {α : Type u_2} : CommRing (ConnesKreimer R (Nonplanar α))

ConnesKreimer R T inherits the CommRing structure from AddMonoidAlgebra R (Forest T) when R is a commutative ring. The Bialgebra substrate only needed CommSemiring; the antipode formula needs negation, hence CommRing.

Equations

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

§1: Subtree depth bound on cut summands

Substrate for the well-founded antipode definition. The depth of any tree appearing in a cut forest of T is strictly less than T.depth. Proved mutually on the planar substrate, then descended via the planar representation.

Planar mutual induction

Nonplanar version (descent via planar rep)

Weight conservation (vertex count) for cuts

Δ^ρ (the deletion variant) preserves total vertex count: for every cut (cf, rem) of T, the cut forest's total weight plus the remainder's weight equals T's weight. Substrate for the lTensor sorry closure: the "right antipode" antipodeRight recurses on rem (weight strictly decreases for nontrivial cuts), in contrast to the standard antipode which recurses on cf (depth strictly decreases).

§1.6: Multiplicity-1 uniqueness for the empty cut

Substrate for the lTensor closure (§6 below). The empty cut (0, T) appears with multiplicity exactly 1 in cutSummandsN T (and in cutSummandsP T₀ for any planar rep). This is the combinatorial fact that the right antipode recursion needs to cancel cleanly.

§2: Antipode definition

Recursive on tree depth via Lean's well-founded recursion. The closed form

S(T) = -Σ_{(cf, rem) ∈ cutSummandsN T} (Π_{Tᵢ ∈ cf} S(Tᵢ)) · ofTree rem

includes the empty cut (0, T) (contributing 1 · ofTree T = ofTree T) so that the negation cleanly gives -ofTree T - Σ_{nontrivial} .... The recursive call on Tᵢ ∈ cf is well-founded by cutSummandsN_subtree_depth_lt.

@[irreducible]

noncomputable def RootedTree.ConnesKreimer.antipodeTreeN {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : ConnesKreimer R (Nonplanar α)

The antipode on a single nonplanar tree, via Foissy's recursive formula summing over all cut summands. The membership proofs h_mem and h_T_i (warned-unused by the linter inside the lambda body) are consumed by decreasing_by to discharge the well-foundedness obligation.

Equations

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

Multiplicative extension to forests

noncomputable def RootedTree.ConnesKreimer.antipodeMonoidHomN {R : Type u_1} [CommRing R] {α : Type u_2} : Multiplicative (Forest (Nonplanar α)) →* ConnesKreimer R (Nonplanar α)

The forest-level antipode: multiplicative extension of antipodeTreeN to forests. Packaged as a MonoidHom to enable lifting via AddMonoidAlgebra.lift.

Equations

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

noncomputable def RootedTree.ConnesKreimer.antipodeAlgHomN {R : Type u_1} [CommRing R] {α : Type u_2} : ConnesKreimer R (Nonplanar α) →ₐ[R] ConnesKreimer R (Nonplanar α)

The antipode as an algebra hom S : H →ₐ[R] H. Since H is commutative, the antipode is a (not anti-)algebra hom.

Equations

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

Right antipode (lTensor recursion)

To close the lTensor antipode axiom (which our standard antipode antipodeTreeN satisfies but for which the axiom isn't directly visible from the definition), we construct an auxiliary "right antipode" antipodeRightTreeN that satisfies the lTensor axiom by definition. The two coincide as elements of H by the monoid left_inv_eq_right_inv argument in the convolution algebra WithConv (H →ₗ[R] H). See §5 below.

The right antipode recurses on rem (which has strictly smaller weight for nontrivial cuts, by cutSummandsN_rem_weight_lt) instead of on cf.

@[irreducible]

noncomputable def RootedTree.ConnesKreimer.antipodeRightTreeN {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : ConnesKreimer R (Nonplanar α)

The right antipode on a single nonplanar tree: defined to satisfy the lTensor axiom by direct cancellation. Recurses on rem for nontrivial cuts (well-founded by cutSummandsN_rem_weight_lt).

Equations

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

Multiplicative extension to forests for R

noncomputable def RootedTree.ConnesKreimer.antipodeRightMonoidHomN {R : Type u_1} [CommRing R] {α : Type u_2} : Multiplicative (Forest (Nonplanar α)) →* ConnesKreimer R (Nonplanar α)

The forest-level right antipode: multiplicative extension.

Equations

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

noncomputable def RootedTree.ConnesKreimer.antipodeRightAlgHomN {R : Type u_1} [CommRing R] {α : Type u_2} : ConnesKreimer R (Nonplanar α) →ₐ[R] ConnesKreimer R (Nonplanar α)

The right antipode as an algebra hom R : H →ₐ[R] H.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.antipodeRightAlgHomN_apply_of' {R : Type u_1} [CommRing R] {α : Type u_2} (F : Forest (Nonplanar α)) : antipodeRightAlgHomN (of' F) = (Multiset.map antipodeRightTreeN F).prod

@[simp]

theorem RootedTree.ConnesKreimer.antipodeRightAlgHomN_apply_ofTree {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : antipodeRightAlgHomN (ofTree T) = antipodeRightTreeN T

@[simp]

theorem RootedTree.ConnesKreimer.antipodeAlgHomN_apply_of' {R : Type u_1} [CommRing R] {α : Type u_2} (F : Forest (Nonplanar α)) : antipodeAlgHomN (of' F) = (Multiset.map antipodeTreeN F).prod

@[simp]

theorem RootedTree.ConnesKreimer.antipodeAlgHomN_apply_ofTree {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : antipodeAlgHomN (ofTree T) = antipodeTreeN T

theorem RootedTree.ConnesKreimer.antipodeRightTreeN_unfold {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : antipodeRightTreeN T = -ofTree T - (Multiset.map (fun (pf : Forest (Nonplanar α) × Nonplanar α) => if Multiset.card pf.1 ≠ 0 then of' pf.1 * antipodeRightTreeN pf.2 else 0) (cutSummandsN T)).sum

The recursive lTensor equation for the right antipode, in non-attach-decorated form. Mirrors antipodeTreeN_unfold but for the lTensor recursion.

theorem RootedTree.ConnesKreimer.antipodeTreeN_unfold {R : Type u_1} [CommRing R] {α : Type u_2} (T : Nonplanar α) : antipodeTreeN T = -(Multiset.map (fun (pf : Forest (Nonplanar α) × Nonplanar α) => (Multiset.map antipodeTreeN pf.1).prod * ofTree pf.2) (cutSummandsN T)).sum

The recursive Foissy equation, in non-attach-decorated form. The attach-style def above keeps the membership info for well-foundedness; this unfold strips it for downstream proofs.

§3: Antipode axiom on trees (depth-induction-free!)

The Foissy recursion was set up so that the antipode axiom on a single tree follows directly from antipodeTreeN_unfold — no further induction is needed. The summands of the antipode definition exactly cancel the summands produced by (lift S id) ∘ comulTreeN T.

§4: Antipode axiom on forests (Multiset induction)

Forest law follows from the tree law by multiplicativity. Convolution (lift S id _) is an algebra hom on H ⊗ H (since H is commutative), so it factors through comulForestN (T ::ₘ F') = comulTreeN T * comulForestN F'. The tree case (lift S id _)(comulTreeN T) = 0 (from §3) makes the cons step produce 0 · _ = 0, matching counit(of' (T ::ₘ F')) = 0.

§5: AlgHom-form rTensor axiom

Lift the forest-level statement (a per-element identity for of' F) to the algebra-hom equality HopfAlgebra.ofAlgHom consumes. Reduces via AddMonoidAlgebra.algHom_ext.

§6: lTensor axiom via WithConv glue

The standard antipode S = antipodeAlgHomN satisfies the rTensor axiom (antipode_rTensor_axiom); the right antipode R = antipodeRightAlgHomN satisfies the lTensor axiom (antipodeRight_lTensor_axiom). In the convolution monoid WithConv (H →ₗ[R] H) these read S * id = 1 and id * R = 1 respectively, so left_inv_eq_right_inv gives S = R as linear maps. By AlgHom.toLinearMap_injective, S = R as algebra homs. Substituting S for R in antipodeRight_lTensor_axiom discharges the lTensor axiom for S.

§7: HopfAlgebra instance

Assemble the Bialgebra (from CoproductNonplanar.lean) + antipode + axioms via mathlib's HopfAlgebra.ofAlgHom.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instHopfAlgebraNonplanar {R : Type u_1} [CommRing R] {α : Type u_2} : HopfAlgebra R (ConnesKreimer R (Nonplanar α))

Equations

• RootedTree.ConnesKreimer.instHopfAlgebraNonplanar = HopfAlgebra.ofAlgHom RootedTree.ConnesKreimer.antipodeAlgHomN ⋯ ⋯