Grossman-Larson monoid structure

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

Completes the multiplicative structure of GrossmanLarson R α (defined in GrossmanLarson.lean) by lifting the integer-case associativity GrossmanLarson.mul_assoc_basis_via_oudom_guin_pbw (proved sorry-free in OudomGuinBridge.lean via Oudom-Guin + PBW) to arbitrary CommSemiring R, then registering Semigroup/Monoid instances.

Architecture

The lift uses the R-generic, basis-form closed expressions lhs_quadruple_form and rhs_quintuple_form (in GrossmanLarsonAssoc.lean), which present both sides of (of' F₁) * (of' F₂) * (of' F₃) = (of' F₁) * ((of' F₂) * (of' F₃)) as (M.map of').sum for R-independent multisets M : Multiset (Forest (Nonplanar α)). The integer case implies the indexing multisets are equal (via Finsupp coefficient extraction + Nat→ℤ injectivity), and that R-free equality re-applies for any R.

Main results (all α : Type*-generic)

• mul_assoc_basis (R-generic) : (of' F₁ * of' F₂) * of' F₃ = of' F₁ * (of' F₂ * of' F₃) on basis vectors.
• mul_assoc (R-generic) : full associativity, by triple ConnesKreimer.addHom_ext.
• instSemigroup, instMonoid instances.

Status

[UPSTREAM] candidate. All results sorry-free.

(M.map of').sum coefficient extraction (multiset injectivity)

mul_assoc_basis (R-generic) via the ℤ-case + multiset lift

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

Basis-level associativity (R-generic, α : Type*). Lifts the integer case mul_assoc_basis_via_oudom_guin_pbw (Q6, proved sorry-free in OudomGuinBridge.lean) to arbitrary CommSemiring R via R-free multiset identification.

Full mul_assoc via triple ConnesKreimer.addHom_ext

theorem RootedTree.GrossmanLarson.mul_assoc {α : Type u_1} {R : Type u_2} [CommSemiring R] (F₁ F₂ F₃ : GrossmanLarson R α) : F₁ * F₂ * F₃ = F₁ * (F₂ * F₃)

Associativity (R-generic, α : Type*). Triple bilinearity reduction to mul_assoc_basis.

Semigroup and Monoid instances

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

@[implicit_reducible, instance 50]

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

Equations

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

@[implicit_reducible, instance 50]

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

Equations

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