Generic admissible-cut coproduct on ConnesKreimer R (UnorderedTree α)

Admissible-cut coproducts share one shape: a primitive term ofTree T ⊗ 1 plus a sum over cut summands (crown, trunk) of of' crown ⊗ ofTree trunk. They differ only in the enumeration cuts T of the cut summands. This file defines the shape once, as the algebra homomorphism comulAlgHomNG cuts; the Connes–Kreimer coproduct is its instance at the pruning cuts cutSummandsN (Coproduct/Pruning.lean).

Main definitions

• ConnesKreimer.comulTreeNG, ConnesKreimer.comulForestNG: the generic coproduct on trees and forests.
• ConnesKreimer.comulAlgHomNG: the generic coproduct as an algebra hom.
• ConnesKreimer.WithCuts R cuts: the carrier indexed by a cut enumeration, a bialgebra when IsAdmissibleCuts cuts holds.

Main results

• ConnesKreimer.comulTreeNG_eq_sum, ConnesKreimer.comulForestNG_eq_sum: the coproduct as one sum over the cut convolutions treeCutsG and forestCutsG.

References

• [CK98]
• [Foi]

noncomputable def ConnesKreimer.comulTreeNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The generic admissible-cut coproduct on a tree, for a cut enumeration cuts. At the pruning cuts cutSummandsN it is the Connes–Kreimer coproduct.

Equations

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

noncomputable def ConnesKreimer.comulForestNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (F : UnorderedTree.Forest (UnorderedTree α)) : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

Forest-level generic coproduct (multiplicative extension).

Equations

• ConnesKreimer.comulForestNG cuts F = (Multiset.map (ConnesKreimer.comulTreeNG cuts) F).prod

@[simp]

theorem ConnesKreimer.comulForestNG_zero {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) : comulForestNG cuts 0 = 1

@[simp]

theorem ConnesKreimer.comulForestNG_add {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (F G : UnorderedTree.Forest (UnorderedTree α)) : comulForestNG cuts (F + G) = comulForestNG cuts F * comulForestNG cuts G

@[simp]

theorem ConnesKreimer.comulForestNG_cons {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) (F : UnorderedTree.Forest (UnorderedTree α)) : comulForestNG cuts (T ::ₘ F) = comulTreeNG cuts T * comulForestNG cuts F

noncomputable def ConnesKreimer.comulAlgHomNG {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) : ConnesKreimer R (UnorderedTree α) →ₐ[R] TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

The generic admissible-cut coproduct as an algebra hom, parameterized by the cut enumeration cuts.

Equations

• ConnesKreimer.comulAlgHomNG cuts = ConnesKreimer.aeval (ConnesKreimer.comulTreeNG cuts)

@[simp]

theorem ConnesKreimer.comulAlgHomNG_apply_of' {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (F : UnorderedTree.Forest (UnorderedTree α)) : (comulAlgHomNG cuts) (of' F) = comulForestNG cuts F

@[simp]

theorem ConnesKreimer.comulAlgHomNG_apply_ofTree {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) : (comulAlgHomNG cuts) (ofTree T) = comulTreeNG cuts T

The generic coproduct as a sum over cut convolutions

treeCutsG/forestCutsG (Combinatorics/RootedTree/Cut.lean) enumerate the (crown, trunk-forest) pairs of a tree and their convolution over a forest; cutTensor sends a pair to of' crown ⊗ of' trunk.

noncomputable def ConnesKreimer.cutTensor {R : Type u_1} [CommSemiring R] {α : Type u_2} (p : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree.Forest (UnorderedTree α)) : TensorProduct R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α))

Tensor-product factor of a (crown, trunk) cut pair.

Equations

• ConnesKreimer.cutTensor p = ConnesKreimer.of' p.1 ⊗ₜ[R] ConnesKreimer.of' p.2

theorem ConnesKreimer.cutTensor_combinerProjG {R : Type u_1} [CommSemiring R] {α : Type u_2} (p q : UnorderedTree.Forest (UnorderedTree α) × UnorderedTree.Forest (UnorderedTree α)) : cutTensor (combinerProjG (p, q)) = cutTensor p * cutTensor q

cutTensor is multiplicative over the cut convolution combinerProjG.

theorem ConnesKreimer.comulTreeNG_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (T : UnorderedTree α) : comulTreeNG cuts T = (Multiset.map cutTensor (treeCutsG cuts T)).sum

comulTreeNG as a single multiset sum over treeCutsG.

theorem ConnesKreimer.comulForestNG_eq_sum {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (UnorderedTree.Forest (UnorderedTree α) × UnorderedTree α)) (F : UnorderedTree.Forest (UnorderedTree α)) : comulForestNG cuts F = (Multiset.map cutTensor (forestCutsG cuts F)).sum

comulForestNG as a single multiset sum over forestCutsG.

The policy-indexed carrier WithCuts

The WithLp pattern: a type synonym indexed by the cut policy, whose Bialgebra instance is gated on an admissibility mixin. The pruning coproduct keeps the plain carrier (instBialgebraRho); other admissible policies get their bialgebra here.

def ConnesKreimer.WithCuts (R : Type u_1) [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : Type (max u_2 u_1)

Type synonym for ConnesKreimer R (UnorderedTree α) carrying the generic admissible-cut coproduct at the fixed policy cuts.

Equations

• ConnesKreimer.WithCuts R cuts = ConnesKreimer R (UnorderedTree α)

@[instance_reducible]

noncomputable instance ConnesKreimer.instCommSemiringWithCuts {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : CommSemiring (WithCuts R cuts)

Equations

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

@[instance_reducible]

noncomputable instance ConnesKreimer.instAlgebraWithCuts {R : Type u_1} [CommSemiring R] {α : Type u_2} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : Algebra R (WithCuts R cuts)

Equations

• ConnesKreimer.instAlgebraWithCuts cuts = { smul := ConnesKreimer.instAlgebraWithCuts._aux_1 cuts, algebraMap := ConnesKreimer.instAlgebraWithCuts._aux_3 cuts, commutes' := ⋯, smul_def' := ⋯ }

class ConnesKreimer.IsAdmissibleCuts {α : Type u_2} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) : Prop

A cut policy is admissible when the generic coproduct comulAlgHomNG cuts is coassociative and counital, uniformly in the coefficient ring. Gates the Bialgebra instance on WithCuts (the Fact-style mixin of the WithLp pattern).

• coassoc (R : Type u_3) [CommRing R] : (↑(Algebra.TensorProduct.assoc R R R (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)) (ConnesKreimer R (UnorderedTree α)))).comp ((Algebra.TensorProduct.map (comulAlgHomNG cuts) (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp (comulAlgHomNG cuts)) = (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) (comulAlgHomNG cuts)).comp (comulAlgHomNG cuts)
• counit_rTensor (R : Type u_4) [CommSemiring R] : (Algebra.TensorProduct.map counit (AlgHom.id R (ConnesKreimer R (UnorderedTree α)))).comp (comulAlgHomNG cuts) = ↑(Algebra.TensorProduct.lid R (ConnesKreimer R (UnorderedTree α))).symm
• counit_lTensor (R : Type u_5) [CommSemiring R] : (Algebra.TensorProduct.map (AlgHom.id R (ConnesKreimer R (UnorderedTree α))) counit).comp (comulAlgHomNG cuts) = ↑(Algebra.TensorProduct.rid R R (ConnesKreimer R (UnorderedTree α))).symm

@[instance_reducible]

noncomputable instance ConnesKreimer.WithCuts.instBialgebra {α : Type u_2} (cuts : UnorderedTree α → Multiset (Multiset (UnorderedTree α) × UnorderedTree α)) {R : Type u_3} [CommRing R] [IsAdmissibleCuts cuts] : Bialgebra R (WithCuts R cuts)

Any admissible cut policy makes WithCuts R cuts a bialgebra.

Equations

• ConnesKreimer.WithCuts.instBialgebra cuts = Bialgebra.ofAlgHom (ConnesKreimer.comulAlgHomNG cuts) ConnesKreimer.counit ⋯ ⋯ ⋯