The Connes–Kreimer algebra

ConnesKreimer R T is the commutative R-algebra with a basis indexed by the forests of T (finite multisets of elements of T), multiplied by disjoint union, with the empty forest as unit. It is the free commutative R-algebra on T. When T is a type of rooted trees, cutting trees makes it the Connes–Kreimer Hopf algebra; the coproducts are in the sibling Coproduct/ files and the antipode in HopfAlgebra.lean.

Main definitions

• UnorderedTree.Forest T: forests of T, as multisets.
• ConnesKreimer R T: the algebra.
• ConnesKreimer.single, ConnesKreimer.of', ConnesKreimer.ofTree: basis vectors.
• ConnesKreimer.coeff: the coefficient of a forest.
• ConnesKreimer.aeval: the algebra hom determined by its values on trees.
• ConnesKreimer.basisSingleOne, ConnesKreimer.linearLift: the forest basis and linear maps defined on it.
• ConnesKreimer.counit: the coefficient of the empty forest, as an algebra hom.

Implementation notes

ConnesKreimer R T wraps AddMonoidAlgebra R (Forest T) in a one-field structure, as Polynomial does. The bare carrier already has the group-like bialgebra structure AddMonoidAlgebra.instBialgebra, and a def synonym would leak parent instance paths (an SMul ℤ diamond). Consumers use the API of this file; toFinsuppAlgEquiv is the bridge to the bare carrier.

[UPSTREAM] candidate.

References

• [CK98]
• [Foi]

@[reducible, inline]

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

Forests of elements of T, as multisets; addition is disjoint union.

Equations

• UnorderedTree.Forest T = Multiset T

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

The Connes–Kreimer algebra on T, the R-span of the forests of T with disjoint union as product.

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

  The underlying forest-indexed AddMonoidAlgebra.

• )

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 (UnorderedTree.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 (UnorderedTree.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 (UnorderedTree.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 (UnorderedTree.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 (UnorderedTree.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 (UnorderedTree.Forest T))] [SMulZeroClass S₂ (AddMonoidAlgebra R (UnorderedTree.Forest T))] [SMulCommClass S₁ S₂ (AddMonoidAlgebra R (UnorderedTree.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 (UnorderedTree.Forest T))] [SMulZeroClass S₂ (AddMonoidAlgebra R (UnorderedTree.Forest T))] [IsScalarTower S₁ S₂ (AddMonoidAlgebra R (UnorderedTree.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 (UnorderedTree.Forest T))) r

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 (UnorderedTree.Forest T)

toFinsupp as an R-algebra equivalence, the 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 (UnorderedTree.Forest T)) : toFinsuppAlgEquiv.symm x = { toFinsupp := x }

Basis vectors

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

single F r is the basis vector with 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 : UnorderedTree.Forest T) (r : R) : (single F r).toFinsupp = AddMonoidAlgebra.single F r

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

To prove a property of every element it suffices to prove it at 0, under +, and on every single.

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

of' F is the forest F as the basis vector single F 1.

Equations

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

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

ofTree t is the forest with the single tree t.

Equations

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

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

theorem ConnesKreimer.smul_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : UnorderedTree.Forest T) (r : R) : r • of' F = single F r

@[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 : UnorderedTree.Forest T) : of' (F + G) = of' F * of' G

Disjoint union of forests is the product of the algebra.

@[simp]

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

@[simp]

theorem ConnesKreimer.of'_cons {R : Type u_1} [CommSemiring R] {T : Type u_2} (t : T) (F : UnorderedTree.Forest T) : of' (t ::ₘ F) = ofTree t * of' F

theorem ConnesKreimer.prod_map_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} (F : UnorderedTree.Forest T) : (Multiset.map ofTree F).prod = of' F

A forest is the product of its trees.

Coefficients

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

The coefficient of the forest F.

Equations

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

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

Elements agreeing coefficientwise are equal.

theorem ConnesKreimer.coeff_sum_map_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} [DecidableEq T] (s : Multiset (UnorderedTree.Forest T)) (F : UnorderedTree.Forest T) : (Multiset.map of' s).sum.coeff F = ↑(Multiset.count F s)

The coefficient of F in the formal sum of a multiset of forests is its multiplicity.

theorem ConnesKreimer.sum_map_of'_injective {R : Type u_1} [CommSemiring R] {T : Type u_2} [CharZero R] : Function.Injective fun (s : Multiset (UnorderedTree.Forest T)) => (Multiset.map of' s).sum

In characteristic zero a multiset of forests is determined by its formal sum.

def ConnesKreimer.lcoeff (R : Type u_1) [CommSemiring R] {T : Type u_2} (F : UnorderedTree.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 : UnorderedTree.Forest T) (p : ConnesKreimer R T) : (lcoeff R F) p = p.coeff F

The universal property

ConnesKreimer R T is the free commutative algebra on T, as MvPolynomial T R is: a function on trees extends uniquely to an algebra hom. The carrier is not literally MvPolynomial T R, whose monomials T →₀ ℕ match Multiset T only under DecidableEq T.

noncomputable def ConnesKreimer.aeval {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] (f : T → A) : ConnesKreimer R T →ₐ[R] A

aeval f is the algebra hom sending each tree t to f t, and so each forest to the product of the values of its trees (MvPolynomial.aeval analogue).

Equations

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

@[simp]

theorem ConnesKreimer.aeval_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] (f : T → A) (F : UnorderedTree.Forest T) : (aeval f) (of' F) = (Multiset.map f F).prod

@[simp]

theorem ConnesKreimer.aeval_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] (f : T → A) (t : T) : (aeval f) (ofTree t) = f t

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

Algebra homs out of ConnesKreimer agree if they agree on forests.

theorem ConnesKreimer.algHom_of'_eq_of_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] {φ ψ : ConnesKreimer R T →ₐ[R] A} {F : UnorderedTree.Forest T} (h : ∀ t ∈ F, φ (ofTree t) = ψ (ofTree t)) : φ (of' F) = ψ (of' F)

Algebra homs agree on a forest if they agree on each of its trees.

theorem ConnesKreimer.algHom_ext_ofTree {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 : ∀ (t : T), φ (ofTree t) = ψ (ofTree t)) : φ = ψ

Algebra homs out of ConnesKreimer agree if they agree on trees.

theorem ConnesKreimer.algHom_ext_ofTree_iff {R : Type u_1} [CommSemiring R] {T : Type u_2} {A : Type u_6} [CommSemiring A] [Algebra R A] {φ ψ : ConnesKreimer R T →ₐ[R] A} : φ = ψ ↔ ∀ (t : T), φ (ofTree t) = ψ (ofTree t)

noncomputable def ConnesKreimer.rename {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_6} (f : T → T') : ConnesKreimer R T →ₐ[R] ConnesKreimer R T'

rename f replaces each tree t of every forest by f t (MvPolynomial.rename analogue).

Equations

• ConnesKreimer.rename f = ConnesKreimer.aeval fun (t : T) => ConnesKreimer.ofTree (f t)

@[simp]

theorem ConnesKreimer.rename_ofTree {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_6} (f : T → T') (t : T) : (rename f) (ofTree t) = ofTree (f t)

@[simp]

theorem ConnesKreimer.rename_of' {R : Type u_1} [CommSemiring R] {T : Type u_2} {T' : Type u_6} (f : T → T') (F : UnorderedTree.Forest T) : (rename f) (of' F) = of' (Multiset.map f F)

The forest basis and linear maps

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

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

Equations

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

@[simp]

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

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

Linear maps out of ConnesKreimer agree if they agree on forests.

theorem ConnesKreimer.lhom_ext'_iff {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} : f = g ↔ ∀ (F : UnorderedTree.Forest T), f (of' F) = g (of' F)

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

linearLift f is the linear map sending each forest F to f F.

Equations

• ConnesKreimer.linearLift f = (ConnesKreimer.basisSingleOne.constr R) 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 : UnorderedTree.Forest T → M) (F : UnorderedTree.Forest T) : (linearLift f) (of' F) = f F

@[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 : UnorderedTree.Forest T → M) (F : UnorderedTree.Forest T) (r : R) : (linearLift f) (single F r) = r • f F

The counit

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

The counit takes the coefficient of the empty forest; it is the algebra hom sending every tree to 0.

Equations

• ConnesKreimer.counit = ConnesKreimer.aeval fun (x : T) => 0

@[simp]

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

counit (of' F) is 1 on the empty forest and 0 otherwise, stated with card to avoid 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