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 HopfAlgebra.lean.

Main declarations

• Nonplanar.Forest: forests as multisets of trees; multiset addition is disjoint union.
• 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 RoseTree.Nonplanar.Forest (T : Type u_1) : Type u_1

A forest of T-shaped trees: finite multiset.

Equations

• RoseTree.Nonplanar.Forest T = Multiset T

The carrier

structure 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 (RoseTree.Nonplanar.Forest T)

  The underlying forest-indexed Finsupp.

• )

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

@[simp]

theorem 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 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 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 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.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem 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 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 ConnesKreimer.toFinsupp_smul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_3} [SMulZeroClass S (AddMonoidAlgebra R (RoseTree.Nonplanar.Forest T))] (s : S) (p : ConnesKreimer R T) : (s • p).toFinsupp = s • p.toFinsupp

@[simp]

theorem 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.

@[instance_reducible]

noncomputable instance 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.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

instance 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 (RoseTree.Nonplanar.Forest T))] [SMulZeroClass S₂ (AddMonoidAlgebra R (RoseTree.Nonplanar.Forest T))] [IsScalarTower S₁ S₂ (AddMonoidAlgebra R (RoseTree.Nonplanar.Forest T))] : IsScalarTower S₁ S₂ (ConnesKreimer R T)

@[instance_reducible]

noncomputable instance 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 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 (RoseTree.Nonplanar.Forest T))) r

@[instance_reducible]

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

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

Equations

• ConnesKreimer.instFunLike = { coe := fun (p : ConnesKreimer R T) => ⇑p.toFinsupp.coeff, 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.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[simp]

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

@[simp]

theorem 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

@[instance_reducible]

noncomputable instance 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 ConnesKreimer.toFinsuppAlgEquiv {R : Type u_1} [CommSemiring R] {T : Type u_2} : ConnesKreimer R T ≃ₐ[R] AddMonoidAlgebra R (RoseTree.Nonplanar.Forest T)

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

Equations

• ConnesKreimer.toFinsuppAlgEquiv = { toFun := ConnesKreimer.toFinsupp, invFun := ConnesKreimer.ofFinsupp, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

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

@[simp]

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

Basis embeddings

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

Basis vector: coefficient r on the forest F.

Equations

• ConnesKreimer.single F r = { toFinsupp := AddMonoidAlgebra.single F r }

@[simp]

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

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

theorem 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 : RoseTree.Nonplanar.Forest T) (r : R), p (single F r)) : p x

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

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

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

Equations

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

noncomputable def ConnesKreimer.of {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (RoseTree.Nonplanar.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

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

noncomputable def 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

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

@[simp]

theorem ConnesKreimer.toFinsupp_of {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : Multiplicative (RoseTree.Nonplanar.Forest T)) : (of F).toFinsupp = (AddMonoidAlgebra.of R (RoseTree.Nonplanar.Forest T)) F

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

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

@[simp]

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

@[simp]

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

Headline algebraic fact: forest disjoint union ↔ algebra product.

@[simp]

theorem 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 ConnesKreimer.coeff {R : Type u_1} [CommSemiring R] {T : Type u_2} (p : ConnesKreimer R T) (F : RoseTree.Nonplanar.Forest T) : R

The coefficient of the forest F.

Equations

• p.coeff F = p.toFinsupp.coeff F

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem 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 : RoseTree.Nonplanar.Forest T) : (s • p).coeff F = s • p.coeff F

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

@[simp]

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

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

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

Elements agreeing coefficientwise are equal.

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

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

Equations

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

@[simp]

theorem ConnesKreimer.lcoeff_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : RoseTree.Nonplanar.Forest T) (p : ConnesKreimer R T) : (lcoeff R 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 ConnesKreimer.lift {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] (f : Multiplicative (RoseTree.Nonplanar.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

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

@[simp]

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

theorem 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 : RoseTree.Nonplanar.Forest T), φ (of' F) = ψ (of' F)) : φ = ψ

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

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

ofFinsupp as an AddMonoidHom (transport vehicle for addHom_ext).

Equations

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

theorem 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 : RoseTree.Nonplanar.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 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 : RoseTree.Nonplanar.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 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 : RoseTree.Nonplanar.Forest T), f (of' F) = g (of' F)) : f = g

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

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

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

Equations

• ConnesKreimer.linearLift f = (Finsupp.lift M R (RoseTree.Nonplanar.Forest T)) f ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv R) ∘ₗ ↑↑ConnesKreimer.toFinsuppAlgEquiv

@[simp]

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

@[simp]

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

noncomputable def ConnesKreimer.mapDomainAlgHom {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_6} (f : RoseTree.Nonplanar.Forest T →+ RoseTree.Nonplanar.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

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

@[simp]

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

Base change

Coefficient-wise base change along a ring hom (Polynomial.map analogue), wrapper-native over AddMonoidAlgebra.map.

noncomputable def ConnesKreimer.map {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (p : ConnesKreimer R T) : ConnesKreimer S T

Base change along f : R →+* S: apply f to each coefficient (Polynomial.map analogue).

Equations

• ConnesKreimer.map f p = { toFinsupp := AddMonoidAlgebra.map (↑f) p.toFinsupp }

@[simp]

theorem ConnesKreimer.toFinsupp_map {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (p : ConnesKreimer R T) : (map f p).toFinsupp = AddMonoidAlgebra.map (↑f) p.toFinsupp

@[simp]

theorem ConnesKreimer.coeff_map {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (p : ConnesKreimer R T) (F : RoseTree.Nonplanar.Forest T) : (map f p).coeff F = f (p.coeff F)

@[simp]

theorem ConnesKreimer.map_single {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (F : RoseTree.Nonplanar.Forest T) (r : R) : map f (single F r) = single F (f r)

@[simp]

theorem ConnesKreimer.map_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (F : RoseTree.Nonplanar.Forest T) : map f (of' F) = of' F

theorem ConnesKreimer.map_zero {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) : map f 0 = 0

theorem ConnesKreimer.map_one {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) : map f 1 = 1

theorem ConnesKreimer.map_add {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (p q : ConnesKreimer R T) : map f (p + q) = map f p + map f q

theorem ConnesKreimer.map_smul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (r : R) (p : ConnesKreimer R T) : map f (r • p) = f r • map f p

theorem ConnesKreimer.map_mul {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (p q : ConnesKreimer R T) : map f (p * q) = map f p * map f q

theorem ConnesKreimer.map_injective {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (hf : Function.Injective ⇑f) : Function.Injective (map f)

noncomputable def ConnesKreimer.mapRingHom {R : Type u_1} [CommSemiring R] (T : Type u_2) {S : Type u_6} [CommSemiring S] (f : R →+* S) : ConnesKreimer R T →+* ConnesKreimer S T

map bundled as a ring hom (Polynomial.mapRingHom analogue); the ring structure is the disjoint-union product.

Equations

• ConnesKreimer.mapRingHom T f = { toFun := ConnesKreimer.map f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ConnesKreimer.coe_mapRingHom {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) : ⇑(mapRingHom T f) = map f

theorem ConnesKreimer.map_multiset_sum {R : Type u_1} [CommSemiring R] {T : Type u_2} {S : Type u_6} [CommSemiring S] (f : R →+* S) (s : Multiset (ConnesKreimer R T)) : map f s.sum = (Multiset.map (map f) s).sum

The forest basis

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

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

Equations

• ConnesKreimer.basisSingleOne = (AddMonoidAlgebra.basis (RoseTree.Nonplanar.Forest T) R).map ↑ConnesKreimer.toFinsuppAlgEquiv.symm

@[simp]

theorem ConnesKreimer.basisSingleOne_apply {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : RoseTree.Nonplanar.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 ConnesKreimer.counitMonoidHom {R : Type u_1} [CommSemiring R] {T : Type u_2} : Multiplicative (RoseTree.Nonplanar.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

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

noncomputable def 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

• ConnesKreimer.counit = ConnesKreimer.lift ConnesKreimer.counitMonoidHom

@[simp]

theorem ConnesKreimer.counit_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : RoseTree.Nonplanar.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 ConnesKreimer.counit_one {R : Type u_1} [CommSemiring R] {T : Type u_2} : counit 1 = 1

@[simp]

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