Grossman-Larson monoid structure

[grossman-larson-1989] [foissy-2021] [OG08]

Associativity of the Grossman-Larson product and the Semigroup/Monoid instances. Foissy coassociativity of Δ^ρ (Coproduct/Pruning.lean) transports back through the GL/CK duality (ConnesKreimer.pairing_product_assoc): over ℤ the symmetry-weighted pairing separates points, giving associativity, and ConnesKreimer.map base change descends the basis case through ℤ → ℕ → R to any CommSemiring (the product's structure constants are ℕ-valued).

Main results (all α : Type*-generic)

• mul_assoc_basis, mul_assoc — associativity, R-generic.
• instSemigroup, instMonoid instances.

[UPSTREAM] candidate.

theorem GrossmanLarson.mul_assoc_basis {α : Type u_1} [DecidableEq α] {R : Type u_2} [CommSemiring R] (F₁ F₂ F₃ : RoseTree.Nonplanar.Forest (RoseTree.Nonplanar α)) : of' F₁ * of' F₂ * of' F₃ = of' F₁ * (of' F₂ * of' F₃)

Basis-level associativity (R-generic): the ℤ case descends through ConnesKreimer.map base change — along ℕ → ℤ by injectivity, then along Nat.cast : ℕ → R.

theorem GrossmanLarson.mul_assoc {α : Type u_1} [DecidableEq α] {R : Type u_2} [CommSemiring R] (x y z : GrossmanLarson R α) : x * y * z = x * (y * z)

Associativity (R-generic): trilinear reduction of mul_assoc_basis, one ConnesKreimer.lhom_ext' per slot.

Semigroup and Monoid instances

With associativity proved, register the typeclass instances. The underlying Mul is the existing instMul from Basic.lean (so no Semigroup.mul-vs-instMul diamond). One is forwarded from ConnesKreimer via instOne (also in Basic.lean).

@[instance_reducible, instance 50]

noncomputable instance GrossmanLarson.instSemigroup {α : Type u_1} [DecidableEq α] {R : Type u_2} [CommSemiring R] : Semigroup (GrossmanLarson R α)

Equations

• GrossmanLarson.instSemigroup = { mul := fun (x1 x2 : GrossmanLarson R α) => x1 * x2, mul_assoc := ⋯ }

@[instance_reducible, instance 50]

noncomputable instance GrossmanLarson.instMonoid {α : Type u_1} [DecidableEq α] {R : Type u_2} [CommSemiring R] : Monoid (GrossmanLarson R α)

Equations

• GrossmanLarson.instMonoid = { toSemigroup := GrossmanLarson.instSemigroup, one := 1, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }