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

The Connes-Kreimer Hopf algebra on a tree type T ([CK98]; [Foi] §1.2) is the formal R-linear span of forests (multisets of trees), with product = forest disjoint union and coproduct = sum over admissible cuts. This file provides the carrier, its algebra structure, and the counit, generic over T; the coproducts and the Bialgebra/HopfAlgebra instances are in the sibling Coproduct/ files and HopfAlgebraNonplanar.lean.

Main declarations

• RootedTree.Forest: forests as multisets of trees; multiset addition is disjoint union.
• RootedTree.ConnesKreimer: one-field wrapper around AddMonoidAlgebra R (Forest T).
• ConnesKreimer.single, ConnesKreimer.of', ConnesKreimer.ofTree, ConnesKreimer.coeff: basis embeddings and coefficient extraction.
• ConnesKreimer.lift, ConnesKreimer.algHom_ext, ConnesKreimer.addHom_ext, ConnesKreimer.linearLift: the wrapper-native hom API.
• ConnesKreimer.counit: the counit ε (coefficient of the empty forest) as an algebra hom.

Implementation notes

ConnesKreimer R T wraps AddMonoidAlgebra R (Forest T) as a one-field structure (mathlib's Polynomial pattern): the bare carrier already carries the group-like AddMonoidAlgebra.instBialgebra, and a def-synonym leaks parent instance paths (an SMul ℤ diamond). Consumers speak the wrapper-native API rather than applying AddMonoidAlgebra/Finsupp lemmas to ConnesKreimer values; toFinsuppAlgEquiv is the bridge for wholesale transport.

[UPSTREAM] candidate.

Forests

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

The 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]

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.

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]

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_4} {S₂ : Type u_5} [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_4} {S₂ : Type u_5} [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]

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

zsmul is the pulled-back structural operation and no parent-type path to SMul ℤ exists, so the instance is safely global.

@[implicit_reducible]

noncomputable instance RootedTree.ConnesKreimer.instNeg {R : Type u_6} [CommRing R] {T : Type u_7} : 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_6} [CommRing R] {T : Type u_7} : 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_6} [CommRing R] {T : Type u_7} : IntCast (ConnesKreimer R T)

Equations

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

@[simp]

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

@[simp]

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

@[implicit_reducible]

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

Equations

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

The algebra equivalence to the bare carrier

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 }

Basis embeddings

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, multiplicative by construction as AddMonoidAlgebra.of transported through the wrapper equivalence.

Equations

• RootedTree.ConnesKreimer.of = (↑↑RootedTree.ConnesKreimer.toFinsuppAlgEquiv.symm).comp (AddMonoidAlgebra.of R (RootedTree.Forest T))

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.

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.

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

Lifts and hom extensionality

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_6} [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_6} [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_6} [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'.

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_6} [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_6} [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_6} [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_6} [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_6} [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_6} [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_6} (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_6} (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

The counit

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

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

The counit as a monoid hom: the indicator of the empty forest, expressed as 0 ^ card (so 0 ^ 0 = 1, 0 ^ n = 0) — multiplicativity is pow_add, and no DecidableEq T is needed.

Equations

• RootedTree.ConnesKreimer.counitMonoidHom = { toFun := fun (F : Multiplicative (RootedTree.Forest T)) => 0 ^ Multiset.card (Multiplicative.toAdd F), map_one' := ⋯, map_mul' := ⋯ }

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