Connes-Kreimer Hopf algebra carrier on n-ary rooted trees

[MCB25] [foissy-introduction-hopf-algebras-trees]

The Connes-Kreimer Hopf algebra on a tree type T is the formal R-linear combinations of forests (multisets of trees), with product = forest disjoint union and coproduct = sum over admissible cuts (defined in Coproduct/Pruning.lean for Δ^ρ, Coproduct/Trace.lean for Δ^c).

This file provides the carrier and counit generic over a tree type T (parameterized over Type*) — nothing here pattern-matches on the tree carrier. The intended specializations:

• T = RoseTree α — n-ary rooted trees (the root-level carrier in Linglib/Core/Data/RoseTree/Basic.lean; the sibling coproduct files instantiate here).
• T = RootedTree.Nonplanar α — n-ary nonplanar rooted trees (Nonplanar α := Quotient RoseTree.instSetoid, a quotient of RoseTree α).

The product structure (algebra) doesn't depend on which T is used — forests are multisets, multiset addition is commutative (Hopf algebra is commutative). The coproduct depends on the cut substrate of T; see sibling files for specific instantiations.

The one-field structure (Polynomial playbook)

ConnesKreimer R T wraps AddMonoidAlgebra R (Forest T) as a one-field structure rather than a def-synonym, for the same reason mathlib's Polynomial R wraps AddMonoidAlgebra R ℕ:

• the admissible-cut Bialgebra cannot live on the bare carrier — mathlib's group-like AddMonoidAlgebra.instBialgebra already occupies it;
• a def-synonym's forwarded instances leave the parent type's instance paths reachable, which produced a genuine SMul ℤ diamond (two routes: Algebra ℤ → Module ℤ → SMul ℤ vs AddCommGroup → SubNegMonoid → zsmul), previously worked around by a noncomputable def addCommGroupOf registered via attribute [local instance] at three consumer sites.

With the structure, all operations are defined on the toFinsupp field and the instance stack is built by injective transport from a single bottom instance (instCommSemiring; a separate AddCommMonoid bottom would itself be a parallel path). The CommRing/AddCommGroup instance is now a safe global instance — its zsmul is the pulled-back structural operation and no alternative path exists, so the diamond is gone by construction.

Consumers should speak the self-contained API — of', ofTree, single, lift, algHom_ext, addHom_ext, counit — and never name AddMonoidAlgebra/Finsupp on ConnesKreimer values; toFinsuppAlgEquiv is the sanctioned escape hatch.

Layer status

[UPSTREAM] candidate. No sorries.

MCB anchor

[MCB25] §1.2 "Workspaces: Product and Coproduct" introduces the Hopf algebra of workspaces; the carrier is V(𝔉_{SO_0}) = AddMonoidAlgebra R (Multiset (FCM α)). This file generalizes the carrier to arbitrary tree type T, with binary FCM as one specialization (eventual Phase B target).

[foissy-introduction-hopf-algebras-trees] §1.2: "The Hopf algebra H_R is the free associative commutative unitary K-algebra generated by T", where T is the set of rooted trees. Same structure here, with T parameterized.

Naming

Type: RootedTree.ConnesKreimer R T with eponymous namespace RootedTree.ConnesKreimer. Eponymous-type-and-namespace pattern matches mathlib idiom (Polynomial, WittVector, PowerSeries, etc.) — no abbreviation. The eventual upstream-mathlib home would be Mathlib.RingTheory.HopfAlgebra.RootedTree.ConnesKreimer or similar.

§1: Forest type alias

A forest is a multiset of trees. Multiset addition is the disjoint union (forest concatenation).

@[reducible, inline]

abbrev RootedTree.Forest (T : Type u_1) : Type u_1

A forest of T-shaped trees: finite multiset.

Equations

• RootedTree.Forest T = Multiset T

§2: The Connes-Kreimer Hopf algebra carrier

structure RootedTree.ConnesKreimer (R : Type u_1) [CommSemiring R] (T : Type u_2) : Type (max u_1 u_2)

The Connes-Kreimer Hopf algebra on tree type T: a one-field wrapper around AddMonoidAlgebra R (Forest T). As an algebra: product = forest disjoint union (commutative), unit = empty forest. The Bialgebra structure (coproduct + coassoc + counit laws) is in sibling files.

• ofFinsupp :: (
• toFinsupp : AddMonoidAlgebra R (Forest T)

  The underlying forest-indexed Finsupp.

• )

theorem RootedTree.ConnesKreimer.toFinsupp_injective {R : Type u_1} [CommSemiring R] {T : Type u_2} : Function.Injective toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_inj {R : Type u_1} [CommSemiring R] {T : Type u_2} {p q : ConnesKreimer R T} : p.toFinsupp = q.toFinsupp ↔ p = q

theorem RootedTree.ConnesKreimer.ext {R : Type u_1} [CommSemiring R] {T : Type u_2} {p q : ConnesKreimer R T} (h : p.toFinsupp = q.toFinsupp) : p = q

theorem RootedTree.ConnesKreimer.ext_iff {R : Type u_1} [CommSemiring R] {T : Type u_2} {p q : ConnesKreimer R T} : p = q ↔ p.toFinsupp = q.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.ofFinsupp_toFinsupp {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) : { toFinsupp := p.toFinsupp } = p

Structural operations

Each operation is defined on the toFinsupp field; the toFinsupp_* pushforward lemmas are all rfl and form the simp normal form.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instZero {R : Type u_1} [CommSemiring R] {T : Type u_2} : Zero (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instZero = { zero := { toFinsupp := 0 } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instOne {R : Type u_1} [CommSemiring R] {T : Type u_2} : One (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instOne = { one := { toFinsupp := 1 } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instAdd {R : Type u_1} [CommSemiring R] {T : Type u_2} : Add (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instAdd = { add := fun (p q : RootedTree.ConnesKreimer R T) => { toFinsupp := p.toFinsupp + q.toFinsupp } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instMul {R : Type u_1} [CommSemiring R] {T : Type u_2} : Mul (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instMul = { mul := fun (p q : RootedTree.ConnesKreimer R T) => { toFinsupp := p.toFinsupp * q.toFinsupp } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.smulZeroClass {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [SMulZeroClass S (AddMonoidAlgebra R (Forest T))] : SMulZeroClass S (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.smulZeroClass = { smul := fun (s : S) (p : RootedTree.ConnesKreimer R T) => { toFinsupp := s • p.toFinsupp }, smul_zero := ⋯ }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instNatCast {R : Type u_1} [CommSemiring R] {T : Type u_2} : NatCast (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instNatCast = { natCast := fun (n : ℕ) => { toFinsupp := ↑n } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instPowNat {R : Type u_1} [CommSemiring R] {T : Type u_2} : Pow (ConnesKreimer R T) ℕ

Equations

• RootedTree.ConnesKreimer.instPowNat = { pow := fun (p : RootedTree.ConnesKreimer R T) (n : ℕ) => { toFinsupp := p.toFinsupp ^ n } }

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_zero {R : Type u_1} [CommSemiring R] {T : Type u_2} : toFinsupp 0 = 0

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_one {R : Type u_1} [CommSemiring R] {T : Type u_2} : toFinsupp 1 = 1

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_add {R : Type u_1} [CommSemiring R] {T : Type u_2} (p q : ConnesKreimer R T) : (p + q).toFinsupp = p.toFinsupp + q.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_mul {R : Type u_1} [CommSemiring R] {T : Type u_2} (p q : ConnesKreimer R T) : (p * q).toFinsupp = p.toFinsupp * q.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_smul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [SMulZeroClass S (AddMonoidAlgebra R (Forest T))] (s : S) (p : ConnesKreimer R T) : (s • p).toFinsupp = s • p.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_pow {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) (n : ℕ) : (p ^ n).toFinsupp = p.toFinsupp ^ n

The instance stack

Built by injective transport from the single bottom instCommSemiring.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCommSemiring {R : Type u_1} [CommSemiring R] {T : Type u_2} : CommSemiring (ConnesKreimer R T)

Equations

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

noncomputable def RootedTree.ConnesKreimer.toFinsuppAddHom {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T →+ AddMonoidAlgebra R (Forest T)

toFinsupp bundled as an AddMonoidHom (transport vehicle).

Equations

• RootedTree.ConnesKreimer.toFinsuppAddHom = { toFun := RootedTree.ConnesKreimer.toFinsupp, map_zero' := ⋯, map_add' := ⋯ }

Granular action instances (mirroring Polynomial): keeping these one synthesis step away from the underlying carrier lets nested-tensor goals (CK ⊗ (CK ⊗ CK)) resolve without deep pending chains.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.distribSMul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [DistribSMul S (AddMonoidAlgebra R (Forest T))] : DistribSMul S (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.distribSMul = { toSMulZeroClass := RootedTree.ConnesKreimer.smulZeroClass, smul_add := ⋯ }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.distribMulAction {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [Monoid S] [DistribMulAction S (AddMonoidAlgebra R (Forest T))] : DistribMulAction S (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.distribMulAction = { toSMul := RootedTree.ConnesKreimer.smulZeroClass.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instModule {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [Semiring S] [Module S (AddMonoidAlgebra R (Forest T))] : Module S (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instModule = { toDistribMulAction := RootedTree.ConnesKreimer.distribMulAction, add_smul := ⋯, zero_smul := ⋯ }

instance RootedTree.ConnesKreimer.smulCommClass {R : Type u_1} [CommSemiring R] {T : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [SMulZeroClass S₁ (AddMonoidAlgebra R (Forest T))] [SMulZeroClass S₂ (AddMonoidAlgebra R (Forest T))] [SMulCommClass S₁ S₂ (AddMonoidAlgebra R (Forest T))] : SMulCommClass S₁ S₂ (ConnesKreimer R T)

instance RootedTree.ConnesKreimer.isScalarTower {R : Type u_1} [CommSemiring R] {T : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [SMul S₁ S₂] [SMulZeroClass S₁ (AddMonoidAlgebra R (Forest T))] [SMulZeroClass S₂ (AddMonoidAlgebra R (Forest T))] [IsScalarTower S₁ S₂ (AddMonoidAlgebra R (Forest T))] : IsScalarTower S₁ S₂ (ConnesKreimer R T)

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instAlgebra {R : Type u_1} [CommSemiring R] {T : Type u_2} : Algebra R (ConnesKreimer R T)

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_algebraMap {R : Type u_1} [CommSemiring R] {T : Type u_2} (r : R) : ((algebraMap R (ConnesKreimer R T)) r).toFinsupp = (algebraMap R (AddMonoidAlgebra R (Forest T))) r

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instFunLike {R : Type u_1} [CommSemiring R] {T : Type u_2} : FunLike (ConnesKreimer R T) (Forest T) R

Coefficient lookup: a Connes-Kreimer element is a function from forests to coefficients.

Equations

• RootedTree.ConnesKreimer.instFunLike = { coe := fun (p : RootedTree.ConnesKreimer R T) => ⇑p.toFinsupp, coe_injective := ⋯ }

Global ring instance (the diamond killer)

zsmul is the pulled-back structural operation; no parent-type path to SMul ℤ exists, so the former addCommGroupOf local-instance hack is unnecessary — and deleted.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instNeg {R : Type u_3} [CommRing R] {T : Type u_4} : Neg (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instNeg = { neg := fun (p : RootedTree.ConnesKreimer R T) => { toFinsupp := -p.toFinsupp } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instSub {R : Type u_3} [CommRing R] {T : Type u_4} : Sub (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instSub = { sub := fun (p q : RootedTree.ConnesKreimer R T) => { toFinsupp := p.toFinsupp - q.toFinsupp } }

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instIntCast {R : Type u_3} [CommRing R] {T : Type u_4} : IntCast (ConnesKreimer R T)

Equations

• RootedTree.ConnesKreimer.instIntCast = { intCast := fun (z : ℤ) => { toFinsupp := ↑z } }

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_neg {R : Type u_3} [CommRing R] {T : Type u_4} (p : ConnesKreimer R T) : (-p).toFinsupp = -p.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_sub {R : Type u_3} [CommRing R] {T : Type u_4} (p q : ConnesKreimer R T) : (p - q).toFinsupp = p.toFinsupp - q.toFinsupp

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instCommRing {R : Type u_3} [CommRing R] {T : Type u_4} : CommRing (ConnesKreimer R T)

Equations

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

The algebra equivalence to the bare carrier

noncomputable def RootedTree.ConnesKreimer.toFinsuppAlgEquiv {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T ≃ₐ[R] AddMonoidAlgebra R (Forest T)

toFinsupp as an R-algebra equivalence — the sanctioned bridge between the wrapper and the bare AddMonoidAlgebra.

Equations

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

@[simp]

theorem RootedTree.ConnesKreimer.toFinsuppAlgEquiv_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) : toFinsuppAlgEquiv p = p.toFinsupp

@[simp]

theorem RootedTree.ConnesKreimer.toFinsuppAlgEquiv_symm_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (x : AddMonoidAlgebra R (Forest T)) : toFinsuppAlgEquiv.symm x = { toFinsupp := x }

§3: Basis embeddings — single, of', ofTree

noncomputable def RootedTree.ConnesKreimer.single {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) (r : R) : ConnesKreimer R T

Basis vector: coefficient r on the forest F.

Equations

• RootedTree.ConnesKreimer.single F r = { toFinsupp := Finsupp.single F r }

@[simp]

theorem RootedTree.ConnesKreimer.toFinsupp_single {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) (r : R) : (single F r).toFinsupp = Finsupp.single F r

theorem RootedTree.ConnesKreimer.smul_single_one {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) (r : R) : single F r = r • single F 1

theorem RootedTree.ConnesKreimer.induction_linear {R : Type u_1} [CommSemiring R] {T : Type u_2} {p : ConnesKreimer R T → Prop} (x : ConnesKreimer R T) (zero : p 0) (add : ∀ (f g : ConnesKreimer R T), p f → p g → p (f + g)) (single : ∀ (F : Forest T) (r : R), p (single F r)) : p x

Linear induction: prove p at 0, under +, and on every single.

noncomputable def RootedTree.ConnesKreimer.of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : ConnesKreimer R T

Bare embedding: a forest as the basis vector single F 1.

Equations

• RootedTree.ConnesKreimer.of' F = RootedTree.ConnesKreimer.single F 1

noncomputable def RootedTree.ConnesKreimer.of {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (Forest T) →* ConnesKreimer R T

MonoidHom embedding: Multiplicative (Forest T) →* ConnesKreimer R T.

Equations

• RootedTree.ConnesKreimer.of = { toFun := fun (F : Multiplicative (RootedTree.Forest T)) => RootedTree.ConnesKreimer.of' (Multiplicative.toAdd F), map_one' := ⋯, map_mul' := ⋯ }

noncomputable def RootedTree.ConnesKreimer.ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : ConnesKreimer R T

Embed a single tree as a singleton-forest basis vector.

Equations

• RootedTree.ConnesKreimer.ofTree t = RootedTree.ConnesKreimer.of' {t}

theorem RootedTree.ConnesKreimer.of_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Multiplicative (Forest T)) : of F = of' (Multiplicative.toAdd F)

theorem RootedTree.ConnesKreimer.toFinsupp_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : (of' F).toFinsupp = Finsupp.single F 1

@[simp]

theorem RootedTree.ConnesKreimer.of'_zero {R : Type u_1} [CommSemiring R] {T : Type u_2} : of' 0 = 1

@[simp]

theorem RootedTree.ConnesKreimer.of'_add {R : Type u_1} [CommSemiring R] {T : Type u_2} (F G : Forest T) : of' (F + G) = of' F * of' G

Headline algebraic fact: forest disjoint union ↔ algebra product.

@[simp]

theorem RootedTree.ConnesKreimer.of'_singleton {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : of' {t} = ofTree t

Coefficients

coeff is the simp-normal spelling of coefficient extraction (Polynomial.coeff analogue); the FunLike application p F reduces to it.

noncomputable def RootedTree.ConnesKreimer.coeff {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) (F : Forest T) : R

The coefficient of the forest F.

Equations

• p.coeff F = p.toFinsupp F

@[simp]

theorem RootedTree.ConnesKreimer.coe_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) (F : Forest T) : p F = p.coeff F

theorem RootedTree.ConnesKreimer.coeff_def {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) (F : Forest T) : p.coeff F = p.toFinsupp F

@[simp]

theorem RootedTree.ConnesKreimer.coeff_zero {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : coeff 0 F = 0

@[simp]

theorem RootedTree.ConnesKreimer.coeff_add {R : Type u_1} [CommSemiring R] {T : Type u_2} (p q : ConnesKreimer R T) (F : Forest T) : (p + q).coeff F = p.coeff F + q.coeff F

@[simp]

theorem RootedTree.ConnesKreimer.coeff_smul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [SMulZeroClass S R] (s : S) (p : ConnesKreimer R T) (F : Forest T) : (s • p).coeff F = s • p.coeff F

theorem RootedTree.ConnesKreimer.coeff_single {R : Type u_1} [CommSemiring R] {T : Type u_2} (F G : Forest T) (r : R) [Decidable (F = G)] : (single F r).coeff G = if F = G then r else 0

@[simp]

theorem RootedTree.ConnesKreimer.coeff_single_same {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) (r : R) : (single F r).coeff F = r

theorem RootedTree.ConnesKreimer.coeff_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F G : Forest T) [Decidable (F = G)] : (of' F).coeff G = if F = G then 1 else 0

theorem RootedTree.ConnesKreimer.ext_coeff {R : Type u_1} [CommSemiring R] {T : Type u_2} {p q : ConnesKreimer R T} (h : ∀ (F : Forest T), p.coeff F = q.coeff F) : p = q

Elements agreeing coefficientwise are equal.

noncomputable def RootedTree.ConnesKreimer.lcoeff {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : ConnesKreimer R T →ₗ[R] R

coeff bundled as a linear functional (Polynomial.lcoeff analogue).

Equations

• RootedTree.ConnesKreimer.lcoeff F = { toFun := fun (p : RootedTree.ConnesKreimer R T) => p.coeff F, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RootedTree.ConnesKreimer.lcoeff_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) (p : ConnesKreimer R T) : (lcoeff F) p = p.coeff F

§4: lift, algHom_ext, addHom_ext — the self-contained hom API

Consumers use these instead of reaching for AddMonoidAlgebra.lift / Finsupp.addHom_ext on the bare carrier.

noncomputable def RootedTree.ConnesKreimer.lift {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_3} [CommSemiring A] [Algebra R A] (f : Multiplicative (Forest T) →* A) : ConnesKreimer R T →ₐ[R] A

Lift a monoid hom off the forest monoid to an algebra hom off the Connes-Kreimer algebra (the wrapper-native AddMonoidAlgebra.lift).

Equations

• RootedTree.ConnesKreimer.lift f = ((AddMonoidAlgebra.lift R A (RootedTree.Forest T)) f).comp ↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv

@[simp]

theorem RootedTree.ConnesKreimer.lift_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_3} [CommSemiring A] [Algebra R A] (f : Multiplicative (Forest T) →* A) (F : Forest T) : (lift f) (of' F) = f (Multiplicative.ofAdd F)

theorem RootedTree.ConnesKreimer.algHom_ext {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_3} [CommSemiring A] [Algebra R A] {φ ψ : ConnesKreimer R T →ₐ[R] A} (h : ∀ (F : Forest T), φ (of' F) = ψ (of' F)) : φ = ψ

Algebra homs off ConnesKreimer agree if they agree on of'.

noncomputable def RootedTree.ConnesKreimer.ofFinsuppAddHom {R : Type u_1} [CommSemiring R] {T : Type u_2} : AddMonoidAlgebra R (Forest T) →+ ConnesKreimer R T

ofFinsupp as an AddMonoidHom (transport vehicle for addHom_ext).

Equations

• RootedTree.ConnesKreimer.ofFinsuppAddHom = { toFun := RootedTree.ConnesKreimer.ofFinsupp, map_zero' := ⋯, map_add' := ⋯ }

theorem RootedTree.ConnesKreimer.addHom_ext {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddZeroClass M] {f g : ConnesKreimer R T →+ M} (h : ∀ (F : Forest T) (r : R), f (single F r) = g (single F r)) : f = g

Additive homs off ConnesKreimer agree if they agree on single.

theorem RootedTree.ConnesKreimer.lhom_ext {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] {f g : ConnesKreimer R T →ₗ[R] M} (h : ∀ (F : Forest T) (r : R), f (single F r) = g (single F r)) : f = g

Linear maps off ConnesKreimer agree if they agree on single.

theorem RootedTree.ConnesKreimer.lhom_ext' {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] {f g : ConnesKreimer R T →ₗ[R] M} (h : ∀ (F : Forest T), f (of' F) = g (of' F)) : f = g

Linear maps off ConnesKreimer agree if they agree on the basis of'.

noncomputable def RootedTree.ConnesKreimer.linearLift {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] (f : Forest T → M) : ConnesKreimer R T →ₗ[R] M

Linearly extend a function off the forest basis (wrapper-native Finsupp.lift).

Equations

• RootedTree.ConnesKreimer.linearLift f = (Finsupp.lift M R (RootedTree.Forest T)) f ∘ₗ ↑↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv

@[simp]

theorem RootedTree.ConnesKreimer.linearLift_single {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] (f : Forest T → M) (F : Forest T) (r : R) : (linearLift f) (single F r) = r • f F

@[simp]

theorem RootedTree.ConnesKreimer.linearLift_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module R M] (f : Forest T → M) (F : Forest T) : (linearLift f) (of' F) = f F

noncomputable def RootedTree.ConnesKreimer.mapDomainAlgHom {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_3} (f : Forest T →+ Forest T') : ConnesKreimer R T →ₐ[R] ConnesKreimer R T'

Transport a forest-monoid hom to an algebra hom between Connes-Kreimer algebras (wrapper-native AddMonoidAlgebra.mapDomainAlgHom).

Equations

• RootedTree.ConnesKreimer.mapDomainAlgHom f = ((↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv.symm).comp (AddMonoidAlgebra.mapDomainAlgHom R R f)).comp ↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv

@[simp]

theorem RootedTree.ConnesKreimer.mapDomainAlgHom_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_3} (f : Forest T →+ Forest T') (F : Forest T) : (mapDomainAlgHom f) (of' F) = of' (f F)

The forest basis

noncomputable def RootedTree.ConnesKreimer.basisSingleOne {R : Type u_1} [CommSemiring R] {T : Type u_2} : Module.Basis (Forest T) R (ConnesKreimer R T)

The forests, via of', as an R-basis of the Connes-Kreimer algebra (Polynomial.basisMonomials analogue).

Equations

• RootedTree.ConnesKreimer.basisSingleOne = Finsupp.basisSingleOne.map ↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv.symm

@[simp]

theorem RootedTree.ConnesKreimer.basisSingleOne_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : basisSingleOne F = of' F

§5: Counit

The counit ε : ConnesKreimer R T → R extracts the coefficient of the empty forest, packaged as an algebra hom.

noncomputable def RootedTree.ConnesKreimer.counitMonoidHom {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (Forest T) →* R

The counit as a Multiplicative (Forest T) →* R monoid hom.

Uses Multiset.card_eq_zero to avoid requiring DecidableEq T: test "is empty" via "has cardinality zero" (card is Nat, decidable).

Equations

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

noncomputable def RootedTree.ConnesKreimer.counit {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T →ₐ[R] R

The counit on ConnesKreimer R T as an algebra hom.

Equations

• RootedTree.ConnesKreimer.counit = RootedTree.ConnesKreimer.lift RootedTree.ConnesKreimer.counitMonoidHom

@[simp]

theorem RootedTree.ConnesKreimer.counit_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Forest T) : counit (of' F) = if Multiset.card F = 0 then 1 else 0

counit (of' F) = if F.card = 0 then 1 else 0. The card formulation avoids needing DecidableEq T.

@[simp]

theorem RootedTree.ConnesKreimer.counit_one {R : Type u_1} [CommSemiring R] {T : Type u_2} : counit 1 = 1

@[simp]

theorem RootedTree.ConnesKreimer.counit_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) : counit (ofTree t) = 0