The Connes–Kreimer–Foissy Hopf algebra of planar rooted trees

The carrier is H k = MonoidAlgebra k (FreeMonoid RTree): the free k-module on planar forests, with forest concatenation as product. The combinatorial coproduct of Formalizations.RingTheory.HopfAlgebra.ConnesKreimer.Coproduct is lifted to a linear map, and H k becomes a Mathlib Coalgebra, Bialgebra and HopfAlgebra.

Main results

• ConnesKreimer.coassoc_map: (Δ ⊗ id) ∘ Δ = (id ⊗ Δ) ∘ Δ as linear maps.
• ConnesKreimer.instCKCoalg: Coalgebra k (H k).
• ConnesKreimer.Δ_mul, ConnesKreimer.Δ_one, ConnesKreimer.instCKBialg: Bialgebra k (H k).
• ConnesKreimer.antipodeF: the antipode by the connected-graded recursion S(f) = −Σ_{(p,r), r ≠ ∅} S(p)·r.
• ConnesKreimer.leftAntipode_eq, ConnesKreimer.rightAntipode'_eq, ConnesKreimer.antipode_eq_antipode': both antipode axioms.
• ConnesKreimer.instCKHopf: HopfAlgebra k (H k).

Implementation notes

Ported from Lean v4.30.0-rc2. In current Mathlib MonoidAlgebra is a structure over its coefficient Finsupp, no longer the Finsupp itself; linear maps out of H k are defined through MonoidAlgebra.coeffLinearEquiv and tested on the basis by ConnesKreimer.lhom_ext. These adaptations follow the port of the same development in LeanPool/lean-pool (LeanPool/ConnesKreimer/Core.lean).

References

• A. Connes, D. Kreimer, Hopf algebras, renormalization and noncommutative geometry, Comm. Math. Phys. 199 (1998) 203–242.
• L. Foissy, Les algèbres de Hopf des arbres enracinés décorés, I, Bull. Sci. Math. 126 (2002) 193–239.
• C. Marín, How a Tree Remembers Its Cuts: the Connes–Kreimer–Foissy Hopf Algebra of Rooted Trees, Machine-Checked in Lean 4 (2026), doi:10.5281/zenodo.20762280. Ported from ConnesKreimer.lean of karlesmarin/connes-kreimer-lean (Lean v4.30.0-rc2).

Mathlib bridge: lift the combinatorial coassoc to a Coalgebra instance.

@[reducible, inline]

abbrev ConnesKreimer.H (k : Type u_1) [CommRing k] : Type u_1

Carrier: forests with k-coefficients (product = forest concatenation).

Equations

• ConnesKreimer.H k = MonoidAlgebra k (FreeMonoid ConnesKreimer.RTree)

theorem ConnesKreimer.lhom_ext (k : Type u_1) [CommRing k] {N : Type u_2} [AddCommMonoid N] [Module k N] ⦃φ ψ : H k →ₗ[k] N⦄ (h : ∀ (f : Forest) (b : k), φ (MonoidAlgebra.single f b) = ψ (MonoidAlgebra.single f b)) : φ = ψ

Extensionality for linear maps out of H k, tested on the forest basis. A Forest-indexed repackaging of MonoidAlgebra.lhom_ext' (Forest and FreeMonoid RTree are definitionally but not reducibly equal, and rw needs the former).

noncomputable def ConnesKreimer.e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : TensorProduct k (H k) (H k)

Pure 2-tensor of a cut (p, r).

Equations

• ConnesKreimer.e2 k pr = MonoidAlgebra.single pr.1 1 ⊗ₜ[k] MonoidAlgebra.single pr.2 1

noncomputable def ConnesKreimer.e3 (k : Type u_1) [CommRing k] (t : Forest × Forest × Forest) : TensorProduct k (H k) (TensorProduct k (H k) (H k))

Pure 3-tensor of an iterated cut (a, b, c), associated to the right.

Equations

• ConnesKreimer.e3 k t = MonoidAlgebra.single t.1 1 ⊗ₜ[k] (MonoidAlgebra.single t.2.1 1 ⊗ₜ[k] MonoidAlgebra.single t.2.2 1)

noncomputable def ConnesKreimer.Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : TensorProduct k (H k) (H k)

Δ on a basis forest.

Equations

• ConnesKreimer.Δ₀ k f = (List.map (ConnesKreimer.e2 k) (ConnesKreimer.coprodForest f)).sum

noncomputable def ConnesKreimer.E3 (k : Type u_1) [CommRing k] (l : Tens3) : TensorProduct k (H k) (TensorProduct k (H k) (H k))

E3 of a triple-tensor list.

Equations

• ConnesKreimer.E3 k l = (List.map (ConnesKreimer.e3 k) l).sum

noncomputable def ConnesKreimer.Δ (k : Type u_1) [CommRing k] : H k →ₗ[k] TensorProduct k (H k) (H k)

Comultiplication.

Equations

• ConnesKreimer.Δ k = Finsupp.linearCombination k (ConnesKreimer.Δ₀ k) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

theorem ConnesKreimer.Δ_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (Δ k) (MonoidAlgebra.single f b) = b • Δ₀ k f

theorem ConnesKreimer.E3_flatMap (k : Type u_1) [CommRing k] (L : Tens) (g : Forest × Forest → Tens3) : E3 k (List.flatMap g L) = (List.map (fun (x : Forest × Forest) => E3 k (g x)) L).sum

E3 distributes over flatMap.

theorem ConnesKreimer.linmap_list_sum (k : Type u_1) [CommRing k] {α : Type u_4} {M : Type u_2} {N : Type u_3} [AddCommMonoid M] [AddCommMonoid N] [Module k M] [Module k N] (φ : M →ₗ[k] N) (l : List α) (h : α → M) : φ (List.map h l).sum = (List.map (fun (a : α) => φ (h a)) l).sum

A linear map commutes with a List.sum of mapped terms.

theorem ConnesKreimer.elem_lemma (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (TensorProduct.assoc k (H k) (H k) (H k)) ((LinearMap.rTensor (H k) (Δ k)) (e2 k pr)) = E3 k (List.map (fun (ab : Forest × Forest) => (ab.1, ab.2, pr.2)) (coprodForest pr.1))

The per-cut computation: assoc ∘ rTensor Δ on a pure 2-tensor e2 (p,r) equals E3 of the left-leg refinement. This is the heart of the coassoc bridge.

theorem ConnesKreimer.elem_lemma_R (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.lTensor (H k) (Δ k)) (e2 k pr) = E3 k (List.map (fun (bc : Forest × Forest) => (pr.1, bc.1, bc.2)) (coprodForest pr.2))

Right-leg analogue: lTensor Δ on e2 (p,r) equals E3 of the right-leg refinement. No assoc needed — the tensor is already right-associated.

theorem ConnesKreimer.lhs_core (k : Type u_1) [CommRing k] (f : Forest) : (TensorProduct.assoc k (H k) (H k) (H k)) ((LinearMap.rTensor (H k) (Δ k)) (Δ₀ k f)) = E3 k (coLeft (coprodForest f))

LHS structural map on Δ₀ f.

theorem ConnesKreimer.rhs_core (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.lTensor (H k) (Δ k)) (Δ₀ k f) = E3 k (coRight (coprodForest f))

RHS structural map on Δ₀ f.

theorem ConnesKreimer.perm_E3 (k : Type u_1) [CommRing k] (f : Forest) : E3 k (coLeft (coprodForest f)) = E3 k (coRight (coprodForest f))

The combinatorial coassoc, transported to E3.

theorem ConnesKreimer.coassoc_map (k : Type u_1) [CommRing k] : ↑(TensorProduct.assoc k (H k) (H k) (H k)) ∘ₗ LinearMap.rTensor (H k) (Δ k) ∘ₗ Δ k = LinearMap.lTensor (H k) (Δ k) ∘ₗ Δ k

Coassociativity as an equality of linear maps.

Counit.

def ConnesKreimer.εmon (k : Type u_1) [CommRing k] : FreeMonoid RTree →* k

Counit monoid hom: every generator ↦ 0, so a word ↦ 0 ^ len = indicator of empty.

Equations

• ConnesKreimer.εmon k = FreeMonoid.lift fun (x : ConnesKreimer.RTree) => 0

@[simp]

theorem ConnesKreimer.εmon_nil (k : Type u_1) [CommRing k] : (εmon k) [] = 1

@[simp]

theorem ConnesKreimer.εmon_of (k : Type u_1) [CommRing k] (a : RTree) : (εmon k) (FreeMonoid.of a) = 0

@[simp]

theorem ConnesKreimer.εmon_cons (k : Type u_1) [CommRing k] (a : RTree) (l : Forest) : (εmon k) (a :: l) = 0

theorem ConnesKreimer.εmon_append (k : Type u_1) [CommRing k] (p p' : Forest) : (εmon k) (p ++ p') = (εmon k) p * (εmon k) p'

noncomputable def ConnesKreimer.εalg (k : Type u_1) [CommRing k] : H k →ₐ[k] k

Counit as an algebra hom, then linear.

Equations

• ConnesKreimer.εalg k = (MonoidAlgebra.lift k k (FreeMonoid ConnesKreimer.RTree)) (ConnesKreimer.εmon k)

noncomputable def ConnesKreimer.ε (k : Type u_1) [CommRing k] : H k →ₗ[k] k

The Connes-Kreimer counit as a linear map.

Equations

• ConnesKreimer.ε k = (ConnesKreimer.εalg k).toLinearMap

theorem ConnesKreimer.ε_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (ε k) (MonoidAlgebra.single f b) = b * (εmon k) f

theorem ConnesKreimer.smul_list_sum (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (c : k) (l : List M) : c • l.sum = (List.map (fun (x : M) => c • x) l).sum

Scalar smul commutes with a List.sum.

theorem ConnesKreimer.smul_list_sum' (k : Type u_1) [CommRing k] {α : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module k M] (c : k) (l : List α) (F : α → M) : c • (List.map F l).sum = (List.map (fun (x : α) => c • F x) l).sum

Smul through a mapped List.sum.

theorem ConnesKreimer.tmul_scalar_right (k : Type u_1) [CommRing k] (m : H k) (c : k) : m ⊗ₜ[k] c = c • m ⊗ₜ[k] 1

Pull a base-ring scalar out of the right tensor leg (avoids CompatibleSMul).

theorem ConnesKreimer.tmul_scalar_left (k : Type u_1) [CommRing k] (c : k) (m : H k) : c ⊗ₜ[k] m = c • 1 ⊗ₜ[k] m

Pull a base-ring scalar out of the left tensor leg.

theorem ConnesKreimer.map_flatMap_sum {α : Type u_2} {β : Type u_3} {M : Type u_4} [AddCommMonoid M] (L : List α) (G : α → List β) (h : β → M) : (List.map h (List.flatMap G L)).sum = (List.map (fun (a : α) => (List.map h (G a)).sum) L).sum

Generic map-over-flatMap List.sum distribution.

The left-counit collapse: ε on the left leg selects the unique ([], f) cut.

theorem ConnesKreimer.collapseL_tree (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (t : RTree) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.1 • g pr.2) (coprodTree t)).sum = g [t]

theorem ConnesKreimer.collapseL_forest (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (f : Forest) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.1 • g pr.2) (coprodForest f)).sum = g f

The right-counit collapse: ε on the right leg selects the unique (f, []) cut.

theorem ConnesKreimer.collapseR_tree (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (t : RTree) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.2 • g pr.1) (coprodTree t)).sum = g [t]

theorem ConnesKreimer.collapseR_forest (k : Type u_1) [CommRing k] {M : Type u_2} [AddCommMonoid M] [Module k M] (f : Forest) (g : Forest → M) : (List.map (fun (pr : Forest × Forest) => (εmon k) pr.2 • g pr.1) (coprodForest f)).sum = g f

theorem ConnesKreimer.rTensor_ε_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.rTensor (H k) (ε k)) (Δ₀ k f) = 1 ⊗ₜ[k] MonoidAlgebra.single f 1

(ε ⊗ id) ∘ Δ on a basis forest gives 1 ⊗ single f 1.

theorem ConnesKreimer.lTensor_ε_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.lTensor (H k) (ε k)) (Δ₀ k f) = MonoidAlgebra.single f 1 ⊗ₜ[k] 1

(id ⊗ ε) ∘ Δ on a basis forest gives single f 1 ⊗ 1.

theorem ConnesKreimer.single_smul_one (k : Type u_1) [CommRing k] (f : FreeMonoid RTree) (b : k) : MonoidAlgebra.single f b = b • MonoidAlgebra.single f 1

@[instance_reducible]

noncomputable instance ConnesKreimer.instCoalgebraStructH (k : Type u_1) [CommRing k] : CoalgebraStruct k (H k)

Equations

• ConnesKreimer.instCoalgebraStructH k = { comul := ConnesKreimer.Δ k, counit := ConnesKreimer.ε k }

@[instance_reducible]

noncomputable instance ConnesKreimer.instCKCoalg (k : Type u_1) [CommRing k] : Coalgebra k (H k)

Equations

• ConnesKreimer.instCKCoalg k = { toCoalgebraStruct := ConnesKreimer.instCoalgebraStructH k, coassoc := ⋯, rTensor_counit_comp_comul := ⋯, lTensor_counit_comp_comul := ⋯ }

Bialgebra: Δ and ε are algebra homs.

theorem ConnesKreimer.single_append (k : Type u_1) [CommRing k] (p p' : Forest) : MonoidAlgebra.single (p ++ p') 1 = MonoidAlgebra.single p 1 * MonoidAlgebra.single p' 1

single of a concatenation is the product (algebra structure of H).

theorem ConnesKreimer.e2_mul (k : Type u_1) [CommRing k] (pr pr' : Forest × Forest) : e2 k (pr.1 ++ pr'.1, pr.2 ++ pr'.2) = e2 k pr * e2 k pr'

e2 is multiplicative across leg-wise concatenation.

theorem ConnesKreimer.mul_list_sum {M : Type u_2} [NonUnitalNonAssocSemiring M] (a : M) (L : List M) : a * L.sum = (List.map (fun (b : M) => a * b) L).sum

Left-distribute a product over a List.sum.

theorem ConnesKreimer.list_sum_mul_sum {M : Type u_2} [NonUnitalNonAssocSemiring M] (L1 L2 : List M) : L1.sum * L2.sum = (List.flatMap (fun (a : M) => List.map (fun (b : M) => a * b) L2) L1).sum

Product of two List.sums is the double sum.

theorem ConnesKreimer.Δ₀_mul (k : Type u_1) [CommRing k] (F G : Forest) : Δ₀ k (F ++ G) = Δ₀ k F * Δ₀ k G

Δ₀ is multiplicative.

theorem ConnesKreimer.Δ_mul (k : Type u_1) [CommRing k] (a b : H k) : (Δ k) (a * b) = (Δ k) a * (Δ k) b

Δ is multiplicative on all of H (reduce to the forest basis, bilinearly).

theorem ConnesKreimer.Δ_one (k : Type u_1) [CommRing k] : (Δ k) 1 = 1

Δ 1 = 1.

@[instance_reducible]

noncomputable instance ConnesKreimer.instCKBialg (k : Type u_1) [CommRing k] : Bialgebra k (H k)

Equations

• ConnesKreimer.instCKBialg k = Bialgebra.mk' k (ConnesKreimer.H k) ⋯ ⋯ ⋯ ⋯

Toward HopfAlgebra: node count (grading) and its conservation under cuts.

Conservation `|p| + |r| = |f|` makes the antipode recursion well-founded
(`r ≠ [] ⟹ |p| < |f|`). 

def ConnesKreimer.sizeT : RTree → ℕ

Number of nodes in a rooted tree.

Equations

• ConnesKreimer.sizeT (ConnesKreimer.RTree.node F) = 1 + ConnesKreimer.sizeF F

def ConnesKreimer.sizeF : Forest → ℕ

Number of nodes in a rooted forest.

Equations

• ConnesKreimer.sizeF [] = 0
• ConnesKreimer.sizeF (t :: ts) = ConnesKreimer.sizeT t + ConnesKreimer.sizeF ts

theorem ConnesKreimer.sizeF_append (F G : Forest) : sizeF (F ++ G) = sizeF F + sizeF G

theorem ConnesKreimer.size_consTree (t : RTree) (pr : Forest × Forest) : pr ∈ coprodTree t → sizeF pr.1 + sizeF pr.2 = sizeT t

theorem ConnesKreimer.size_consForest (f : Forest) (pr : Forest × Forest) : pr ∈ coprodForest f → sizeF pr.1 + sizeF pr.2 = sizeF f

theorem ConnesKreimer.sizeF_pos {f : Forest} (h : f ≠ []) : 0 < sizeF f

noncomputable def ConnesKreimer.sf (k : Type u_1) [CommRing k] (r : Forest) : H k

A forest as an H-basis element, with the index forced to FreeMonoid RTree via ofList (so it is always typed H k, even on the empty forest).

Equations

• ConnesKreimer.sf k r = MonoidAlgebra.single (FreeMonoid.ofList r) 1

@[simp]

theorem ConnesKreimer.sf_nil (k : Type u_1) [CommRing k] : sf k [] = 1

theorem ConnesKreimer.sf_append (k : Type u_1) [CommRing k] (a b : Forest) : sf k (a ++ b) = sf k a * sf k b

@[irreducible]

noncomputable def ConnesKreimer.antipodeF (k : Type u_1) [CommRing k] : Forest → H k

The antipode on the forest basis, by well-founded recursion on node count. S(∅) = 1; S(f) = -Σ_{(p,r) cut, r ≠ ∅} S(p)·r. Recursion decreases since |p| < |f|.

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.antipodeF k [] = 1

Antipode as a linear map + the left convolution axiom (S ⋆ id = η∘ε).

noncomputable def ConnesKreimer.antipode (k : Type u_1) [CommRing k] : H k →ₗ[k] H k

The antipode linear map obtained by extending antipodeF from the forest basis.

Equations

• ConnesKreimer.antipode k = Finsupp.linearCombination k (ConnesKreimer.antipodeF k) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

theorem ConnesKreimer.antipode_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (antipode k) (MonoidAlgebra.single f b) = b • antipodeF k f

theorem ConnesKreimer.antipodeF_cons (k : Type u_1) [CommRing k] (t : RTree) (ts : Forest) : antipodeF k (t :: ts) = -(List.map (fun (pr : Forest × Forest) => antipodeF k pr.1 * sf k pr.2) (List.filter (fun (pr : Forest × Forest) => !List.isEmpty pr.2) (coprodForest (t :: ts)))).sum

antipodeF on a nonempty forest, as a plain (non-attach) sum.

theorem ConnesKreimer.isEmpty_append_of_ne {r b : Forest} (h : r ≠ []) : List.isEmpty (r ++ b) = false

r ++ b is nonempty when r is.

theorem ConnesKreimer.filter_emptyR_tmul (A B : Tens) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (tmul A B) = tmul (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) A) (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) B)

Filtering cuts by "empty right leg" factorizes over tmul.

theorem ConnesKreimer.coprodTree_filter_emptyR (t : RTree) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (coprodTree t) = [([t], [])]

The unique empty-right cut of a tree t is ([t], []).

theorem ConnesKreimer.coprodForest_filter_emptyR (f : Forest) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.2) (coprodForest f) = [(f, [])]

theorem ConnesKreimer.filter_emptyL_tmul (A B : Tens) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (tmul A B) = tmul (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) A) (List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) B)

Filtering cuts by "empty left leg" factorizes over tmul.

theorem ConnesKreimer.coprodTree_filter_emptyL (t : RTree) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (coprodTree t) = [([], [t])]

The unique empty-left cut of a tree t is ([], [t]).

theorem ConnesKreimer.coprodForest_filter_emptyL (f : Forest) : List.filter (fun (pr : Forest × Forest) => List.isEmpty pr.1) (coprodForest f) = [([], f)]

theorem ConnesKreimer.map_sum_filter_split (k : Type u_1) [CommRing k] {α : Type u_2} (L : List α) (P : α → Bool) (g : α → H k) : (List.map g L).sum = (List.map g (List.filter P L)).sum + (List.map g (List.filter (fun (x : α) => !P x) L)).sum

Split a mapped List.sum by a boolean predicate.

theorem ConnesKreimer.leftConvF (k : Type u_1) [CommRing k] (f : Forest) : (List.map (fun (pr : Forest × Forest) => antipodeF k pr.1 * sf k pr.2) (coprodForest f)).sum = (εmon k) f • 1

Left convolution axiom on a basis forest: (S ⋆ id)(f) = ε(f)·1. Near-definitional.

theorem ConnesKreimer.mul_rTensor_antipode_e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((LinearMap.rTensor (H k) (antipode k)) (e2 k pr)) = antipodeF k pr.1 * sf k pr.2

μ ∘ (S ⊗ id) on a pure 2-tensor e2 (p,r) gives S(p)·r.

theorem ConnesKreimer.rTensor_antipode_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.mul' k (H k) ∘ₗ LinearMap.rTensor (H k) (antipode k)) (Δ₀ k f) = (εmon k) f • 1

μ ∘ (S ⊗ id) ∘ Δ on a basis forest equals ε(f)·1 (left antipode identity).

Mirror (right) antipode S', satisfying id ⋆ S' = η∘ε.

@[irreducible]

noncomputable def ConnesKreimer.antipodeF' (k : Type u_1) [CommRing k] : Forest → H k

The right antipode by well-founded recursion on node count. S'(∅) = 1; S'(f) = -Σ_{(p,r) cut, p ≠ ∅} p·S'(r). Decreases since |r| < |f|.

Equations

• One or more equations did not get rendered due to their size.
• ConnesKreimer.antipodeF' k [] = 1

theorem ConnesKreimer.antipodeF'_cons (k : Type u_1) [CommRing k] (t : RTree) (ts : Forest) : antipodeF' k (t :: ts) = -(List.map (fun (pr : Forest × Forest) => sf k pr.1 * antipodeF' k pr.2) (List.filter (fun (pr : Forest × Forest) => !List.isEmpty pr.1) (coprodForest (t :: ts)))).sum

theorem ConnesKreimer.rightConvF' (k : Type u_1) [CommRing k] (f : Forest) : (List.map (fun (pr : Forest × Forest) => sf k pr.1 * antipodeF' k pr.2) (coprodForest f)).sum = (εmon k) f • 1

Right convolution id ⋆ S' on a basis forest equals ε(f)·1. Near-definitional.

noncomputable def ConnesKreimer.antipode' (k : Type u_1) [CommRing k] : H k →ₗ[k] H k

The mirrored antipode candidate used to prove the right convolution identity.

Equations

• ConnesKreimer.antipode' k = Finsupp.linearCombination k (ConnesKreimer.antipodeF' k) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)

theorem ConnesKreimer.antipode'_single (k : Type u_1) [CommRing k] (f : Forest) (b : k) : (antipode' k) (MonoidAlgebra.single f b) = b • antipodeF' k f

theorem ConnesKreimer.mul_lTensor_antipode'_e2 (k : Type u_1) [CommRing k] (pr : Forest × Forest) : (LinearMap.mul' k (H k)) ((LinearMap.lTensor (H k) (antipode' k)) (e2 k pr)) = sf k pr.1 * antipodeF' k pr.2

theorem ConnesKreimer.lTensor_antipode'_Δ₀ (k : Type u_1) [CommRing k] (f : Forest) : (LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode' k)) (Δ₀ k f) = (εmon k) f • 1

μ ∘ (id ⊗ S') ∘ Δ on a basis forest equals ε(f)·1 (right antipode identity).

theorem ConnesKreimer.leftAntipode_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.rTensor (H k) (antipode k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

Left antipode identity as a linear-map equality (the Hopf left axiom).

theorem ConnesKreimer.rightAntipode'_eq (k : Type u_1) [CommRing k] : LinearMap.mul' k (H k) ∘ₗ LinearMap.lTensor (H k) (antipode' k) ∘ₗ Δ k = Algebra.linearMap k (H k) ∘ₗ ε k

Right antipode identity for S' as a linear-map equality.

theorem ConnesKreimer.antipode_eq_antipode' (k : Type u_1) [CommRing k] : antipode k = antipode' k

The left and right antipodes coincide (a left convolution-inverse of id that has a right convolution-inverse must equal it — pure monoid algebra in WithConv).

@[instance_reducible]

noncomputable instance ConnesKreimer.instHopfAlgebraStructH (k : Type u_1) [CommRing k] : HopfAlgebraStruct k (H k)

Equations

• ConnesKreimer.instHopfAlgebraStructH k = { toBialgebra := ConnesKreimer.instCKBialg k, antipode := ConnesKreimer.antipode k }

@[instance_reducible]

noncomputable instance ConnesKreimer.instCKHopf (k : Type u_1) [CommRing k] : HopfAlgebra k (H k)

Equations

• ConnesKreimer.instCKHopf k = { toHopfAlgebraStruct := ConnesKreimer.instHopfAlgebraStructH k, mul_antipode_rTensor_comul := ⋯, mul_antipode_lTensor_comul := ⋯ }