The Oudom-Guin ○ operation on SymmetricAlgebra R L

@cite{oudom-guin-2008}

For a pre-Lie algebra L, this file constructs the canonical extension of the pre-Lie product · : L × L → L to a bilinear operation ○ : S(L) × S(L) → S(L) satisfying the three defining equations of Oudom-Guin (2008) Proposition 2.7:

• (i) A ○ 1 = A
• (ii) T ○ (B * X) = (T ○ B) ○ X − T ○ (B ○ X) (for T ∈ L)
• (iii) (A * B) ○ C = (A ○ C₍₁₎) * (B ○ C₍₂₎) (where Δ(C) = Σ C₍₁₎ ⊗ C₍₂₎)

These equations uniquely determine ○. From ○, the Oudom-Guin product ★ : S(L) × S(L) → S(L), A ★ B := (A ○ B₍₁₎) * B₍₂₎ (Definition 2.9), is associative (Lemma 2.10), making (S(L), ★, Δ) a Hopf algebra isomorphic to U(L_Lie) (Theorem 2.12).

Why this file (and not GuinOudom.lean)

The sibling file GuinOudom.lean follows the Manchon route: build η : U(L_Lie) → S(L) directly via the M operator and obtain ★ as the transferred UEA product. That route requires η to be an isomorphism (classical PBW), which mathlib does not yet have, so the Manchon-route ★ is currently blocked.

This file follows the Oudom-Guin route: define ○ and ★ directly on S(L), prove ★ associative via Lemma 2.10's 6-line algebraic chain (using Prop 2.7's defining equations + cocommutativity of Δ). No PBW is required for associativity.

Status

Q1b construction landed (2026-05-16). oudomGuinCirc is built via SymmetricAlgebra.lift into the convolution algebra WithConv (S(L) →ₗ[R] S(L)). The convolution-algebra structure (LinearMap.convAlgebra in Linglib.Core.RingTheory.Coalgebra.Convolution) makes S(L) →ₗ[R] S(L) an R-algebra under the convolution product (f * g)(c) := μ ∘ (f ⊗ g) ∘ Δ(c), commutative because S(L) is cocommutative (Q1a).

The generator-level input map circGen : L →ₗ[R] WithConv (S(L) →ₗ[R] S(L)) sends T ↦ ι ∘ circByT_total T (lifting the L-valued circByT_total T from Q1b Step 1 to S(L)-valued via ι : L → S(L)). Q1b Step 1's T-linearity of circByT_total (proven in Linglib.Core.Algebra.PreLie.OudomGuinCircTotal) is what makes this generator map linear.

Remaining for Q1c (uniqueness from defining equations) is deferred.

The interface (defining equations + Prop 2.8.v + Lemma 2.10) is stable and consumers (Q2/Q3/Q4/Q5/Q6 of the pivot) can build against it.

References

• @cite{oudom-guin-2008} — original construction, §2.
• @cite{manchon-2011} — survey, Theorem 1.1 (Manchon route, alternative).
• @cite{chapoton-livernet-2001} — free pre-Lie algebra = rooted trees.

Convention

Right pre-Lie (RightPreLieAlgebra from Tapia 2025), matching GuinOudom.lean. Pre-Lie product written as * on L. Oudom-Guin's ○ notation is reserved for the extension to S(L).

§1: The ○ operation on S(L) × S(L) → S(L)

Oudom-Guin (2008) Proposition 2.7's defining equations characterize a unique bilinear extension of the pre-Lie product · : L × L → L to an operation ○ : S(L) × S(L) → S(L). The construction lifts via SymmetricAlgebra.lift into the convolution algebra WithConv (S(L) →ₗ[R] S(L)) (commutative because S(L) is cocommutative).

The generator-level input is circGen : L →ₗ[R] WithConv (S(L) →ₗ[R] S(L)), sending T ↦ ι ∘ circByT_total T — the L-valued Q1b Step 1 map circByT_total T post-composed with ι : L → S(L) to land in S(L), then opted into the convolution multiplication.

SymmetricAlgebra.lift R L circGen extends circGen uniquely to an R-algebra hom circHom : S(L) →ₐ[R] WithConv (S(L) →ₗ[R] S(L)). The bilinear oudomGuinCirc is then A ↦ B ↦ (circHom A).ofConv B.

noncomputable def PreLie.OudomGuinCirc.circGen {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] : L →ₗ[R] WithConv (SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L)

Generator map: T ↦ toConv (ι ∘ circByT_total T). Input to SymmetricAlgebra.lift. Linear in T by circByT_total_T_add/smul from OudomGuinCircTotal.

Equations

• PreLie.OudomGuinCirc.circGen = { toFun := fun (T : L) => WithConv.toConv (SymmetricAlgebra.ι R L ∘ₗ PreLie.OudomGuinCircConstruct.circByT_total T), map_add' := ⋯, map_smul' := ⋯ }

noncomputable def PreLie.OudomGuinCirc.circHom {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] : SymmetricAlgebra R L →ₐ[R] WithConv (SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L)

The lifted algebra hom circHom : S(L) →ₐ[R] WithConv (S(L) →ₗ[R] S(L)), extending circGen via the universal property of SymmetricAlgebra.

By construction:

• circHom (ι T) = toConv (ι ∘ circByT_total T) (circGen T).
• circHom (A * B) = circHom A * circHom B (convolution).
• circHom 1 = 1 (= toConv (Algebra.linearMap R S(L) ∘ counit)).

Convolution is commutative on WithConv (C →ₗ[R] A) when C is cocommutative and A is commutative — both hold for S(L), allowing SymmetricAlgebra.lift to land here.

Equations

• PreLie.OudomGuinCirc.circHom = SymmetricAlgebra.lift PreLie.OudomGuinCirc.circGen

noncomputable def PreLie.OudomGuinCirc.oudomGuinCirc {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] : SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L

The Oudom-Guin ○ operation on S(L). Bilinear extension of the pre-Lie product · : L × L → L satisfying Prop 2.7's defining equations.

Defined as A ↦ B ↦ (circHom A).ofConv B. The composition ofConv ∘ₗ circHom.toLinearMap : S(L) →ₗ[R] (S(L) →ₗ[R] S(L)) is linear in A (since circHom is an algebra hom, hence linear) and linear in B (since each (circHom A).ofConv is a linear map).

Equations

• PreLie.OudomGuinCirc.oudomGuinCirc = ↑(WithConv.linearEquiv R (SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L)) ∘ₗ PreLie.OudomGuinCirc.circHom.toLinearMap

@[simp]

theorem PreLie.OudomGuinCirc.circHom_ι {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : circHom ((SymmetricAlgebra.ι R L) T) = circGen T

theorem PreLie.OudomGuinCirc.oudomGuinCirc_eq_ofConv {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A : SymmetricAlgebra R L) : oudomGuinCirc A = (circHom A).ofConv

Helper: oudomGuinCirc A is (circHom A).ofConv as a linear map. By definition of oudomGuinCirc as a composition.

def PreLie.OudomGuinCirc.«term_○_» : Lean.TrailingParserDescr

Notation for the Oudom-Guin ○ operation.

Equations

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

§2: Defining equations (Prop 2.7)

Oudom-Guin's Proposition 2.7 states that the three equations below uniquely characterize ○. We state each as a theorem. With the construction sorry-fenced, these are also sorry-fenced (they witness that the construction satisfies the defining equations).

theorem PreLie.OudomGuinCirc.circ_one_right {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A : SymmetricAlgebra R L) : (oudomGuinCirc A) 1 = A

Prop 2.7 (i): right unit. A ○ 1 = A for all A ∈ S(L).

Proof structure: induction on A via SymmetricAlgebra.induction.

• algebraMap r: (algebraMap r).ofConv 1 = r • algebraMap (counit 1) = r • algebraMap 1 = r • 1 = algebraMap r.
• ι T: (circGen T).ofConv 1 = (ι ∘ circByT_total T) 1 = ι (circByT_total T 1) = ι T by circByT_total_one (OG Def 2.4 base).
• mul A B: (circHom A * circHom B).ofConv 1 = mul' (map (.ofConv) (.ofConv) (comul 1)) = mul' (map (.ofConv) (.ofConv) (1 ⊗ 1)) = (.ofConv 1) * (.ofConv 1) = A * B by IH.
• add: linearity.

theorem PreLie.OudomGuinCirc.circ_mul_distrib_via_comul {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B C : SymmetricAlgebra R L) : (oudomGuinCirc (A * B)) C = (LinearMap.mul' R (SymmetricAlgebra R L) ∘ₗ TensorProduct.map (oudomGuinCirc A) (oudomGuinCirc B)) (CoalgebraStruct.comul C)

Prop 2.7 (iii): distributivity via Δ. (A * B) ○ C = Σ (A ○ C₍₁₎) · (B ○ C₍₂₎) (Sweedler-summed over the coproduct).

This is the defining equation that extends ○ from L × S(L) to S(L) × S(L) on the left argument.

Stated via Coalgebra.comul from Q1a's Bialgebra instance on SymmetricAlgebra R L. By construction: circHom is an algebra hom into the convolution algebra, so circHom (A * B) = circHom A * circHom B (convolution), which unfolds to exactly the RHS.

§3: Reduction to L × L pre-Lie product

When both arguments are images of L under ι, the OG ○ agrees with the original pre-Lie product on L.

theorem PreLie.OudomGuinCirc.circ_ι_ι {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T X : L) : (oudomGuinCirc ((SymmetricAlgebra.ι R L) T)) ((SymmetricAlgebra.ι R L) X) = (SymmetricAlgebra.ι R L) (T * X)

ι(T) ○ ι(X) = ι(T * X) for T, X ∈ L. The pre-Lie product on L lifts to S(L) via ι.

Direct: oudomGuinCirc (ι T) (ι X) = (circGen T).ofConv (ι X) = ι (circByT_total T (ι X)) = ι (T * X) by circByT_total_ι (degree-1 base case of Q1b Step 1).

theorem PreLie.OudomGuinCirc.one_circ {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A : SymmetricAlgebra R L) : (oudomGuinCirc 1) A = SymmetricAlgebra.algebraMapInv A • 1

1 ○ A = ε(A) · 1 for A ∈ S(L). The counit map appears here. (Prop 2.8 (i) in Oudom-Guin.)

Direct: oudomGuinCirc 1 A = (circHom 1).ofConv A = (1 : WithConv).ofConv A = algebraMap R (S L) (counit A) = counit A • 1. Then counit = algebraMapInv by instBialgebra's construction.

theorem PreLie.OudomGuinCirc.counit_circ {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : SymmetricAlgebra.algebraMapInv ((oudomGuinCirc A) B) = SymmetricAlgebra.algebraMapInv A * SymmetricAlgebra.algebraMapInv B

Prop 2.8 (ii): counit and ○ commute. ε(A ○ B) = ε(A) · ε(B).

Strategy: prove the linear-map equality ε ∘ₗ oudomGuinCirc A = ε A • ε, then apply at B. Induction on A:

• algebraMap r: (algebraMap r in WithConv).ofConv B' = r • algebraMap (counit B'); ε of both sides reduces via algebraMap_leftInverse + counit = algebraMapInv.
• ι T: (circGen T).ofConv B' = ι (circByT_total T B'); ε kills ι.
• mul A₁ A₂: push ε through mul' (AlgHom.comp_mul'), fuse nested TensorProduct.map, apply IH, close via mul'_map_algebraMapInv_comul.
• add: linearity.

§3.A: Prop 2.7 (ii) — the Def 2.4 recursion at the S(L) level

circ_T_mul: ι T ○ (B · ι X) = (ι T ○ B) ○ ι X - ι T ○ (B ○ ι X).

Proof strategy: tprod-extensionality. The identity is linear in B; verify on the spanning set of monomials ι(a₀) · ... · ι(a_{m-1}) = algHomL (tprod_m a) via circTMultilinear_succ (Def 2.4 at the per-degree level). The crucial helper is the derivation formula oudomGuinCirc (algHomL z) (ι X) = derivative_TA z X expressed as a sum over positions, then matched with the multilinear recursion.

theorem PreLie.OudomGuinCirc.circ_T_mul {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (B : SymmetricAlgebra R L) (X : L) : (oudomGuinCirc ((SymmetricAlgebra.ι R L) T)) (B * (SymmetricAlgebra.ι R L) X) = (oudomGuinCirc ((oudomGuinCirc ((SymmetricAlgebra.ι R L) T)) B)) ((SymmetricAlgebra.ι R L) X) - (oudomGuinCirc ((SymmetricAlgebra.ι R L) T)) ((oudomGuinCirc B) ((SymmetricAlgebra.ι R L) X))

Prop 2.7 (ii): recursive equation for T ∈ L on the left. T ○ (B · X) = (T ○ B) ○ X − T ○ (B ○ X) for T, X ∈ L, B ∈ S(L).

This is the Def 2.4 recursion lifted to the symmetric-algebra setting.

Proof: tprod-extensionality. Define the linear map Δ_X(B) := LHS(B) - RHS(B) : S(L) →ₗ S(L). To show Δ_X = 0, it suffices to show Δ_X ∘ₗ algHomL = 0 : TA →ₗ S(L). Via TA_linearMap_ext_tprod, this reduces to checking on tprods, which follows from circByT_total_algHomL_tprod_mul_ι + oudomGuinCirc_algHomL_tprod_ι + circ_ι_ι (collapsing the algInv-of-multilinear into T*X-form).

§3.B: Prop 2.8 (iii) — Δ commutes with ○

Δ(A ○ B) = Σ (A₍₁₎ ○ B₍₁₎) ⊗ (A₍₂₎ ○ B₍₂₎), Sweedler-summed over both coproducts. Stated and proved as a pointwise identity, with the multi-Sweedler reshuffling encoded by TensorProduct.tensorTensorTensorComm (TTTC): (M ⊗ N) ⊗ (P ⊗ Q) → (M ⊗ P) ⊗ (N ⊗ Q), applied to Δ A ⊗ Δ B ∈ (S ⊗ S) ⊗ (S ⊗ S).

Proof structure: induction on A via SymmetricAlgebra.induction. The mul case requires the iterated-coproduct invariance TTTC ∘ (Δ ⊗ Δ) ∘ Δ = (Δ ⊗ Δ) ∘ Δ, which follows from cocommutativity of Δ (via Coalgebra.IsCocomm). We factor this into the auxiliary lemma comul_squared_TTTC_eq.

theorem PreLie.OudomGuinCirc.comul_circ {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : CoalgebraStruct.comul ((oudomGuinCirc A) B) = (TensorProduct.map (TensorProduct.lift oudomGuinCirc) (TensorProduct.lift oudomGuinCirc)) ((TensorProduct.tensorTensorTensorComm R (SymmetricAlgebra R L) (SymmetricAlgebra R L) (SymmetricAlgebra R L) (SymmetricAlgebra R L)) ((TensorProduct.map CoalgebraStruct.comul CoalgebraStruct.comul) (A ⊗ₜ[R] B)))

Prop 2.8 (iii) of Oudom-Guin (2008). Δ(A ○ B) = Σ (A₍₁₎ ○ B₍₁₎) ⊗ (A₍₂₎ ○ B₍₂₎), the bialgebra-style "○ is a coalgebra map" identity on S(L) ⊗ S(L) with the tensor product coalgebra structure.

In linear-map terms: (uncurried ○) : S(L) ⊗ S(L) → S(L) is a coalgebra map (target coalgebra: S(L); source coalgebra: tensor product). Equivalently:

Δ ∘ μ = (μ ⊗ μ) ∘ TTTC ∘ (Δ ⊗ Δ)    as maps  S ⊗ S → S ⊗ S

where μ = TensorProduct.lift oudomGuinCirc.

Proof: induction on A via SymmetricAlgebra.induction with generalizing B. The four cases:

• algebraMap r: both sides reduce to r • ε(B) • (1 ⊗ 1) via one_circ (Prop 2.8.i) + counit triangle. Uses helpers map_uncurry_TTTC_pure + map_circ_a_circ_one_comul.
• ι T: both sides reduce to (ι T ○ B) ⊗ 1 + 1 ⊗ (ι T ○ B) via primitivity of ι T (so Δ(ι T) = ι T ⊗ 1 + 1 ⊗ ι T) and circByT_total T B ∈ L (so its image under ι is primitive too). Uses map_circ_a_circ_one_comul and map_circ_one_circ_b_comul on the two halves of Δ(ι T).
• mul A₁ A₂: OG's Sweedler-chasing chain using Prop 2.7.iii (circ_mul_distrib_via_comul) twice, Bialgebra.comul_mul, IH on both factors, and comul_squared_TTTC_eq (cocommutativity-derived 4-fold symmetry) to align the inner pairing.
• add A₁ A₂: linearity.

§4: Prop 2.8.v — the key inductive lemma

(A ○ B) ○ C = A ○ ((B ○ C₍₁₎) · C₍₂₎). Proved by induction on the length of A (Oudom-Guin paper page 7).

This is THE substantive lemma needed for Lemma 2.10's proof of ★ associativity.

theorem PreLie.OudomGuinCirc.circ_assoc_via_comul {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B C : SymmetricAlgebra R L) : (oudomGuinCirc ((oudomGuinCirc A) B)) C = (oudomGuinCirc A) ((LinearMap.mul' R (SymmetricAlgebra R L) ∘ₗ TensorProduct.map (oudomGuinCirc B) LinearMap.id) (CoalgebraStruct.comul C))

Prop 3.9 (v) of Oudom-Guin (2008). The inductive key for Lemma 2.10's proof of ★ associativity.

(A ○ B) ○ C = A ○ ((B ○ C₍₁₎) · C₍₂₎), Sweedler-summed over the coproduct of C.

Proof: lift circ_assoc_via_comul_tprod (per-tprod claim) via algHomL_surjective + TA_linearMap_ext_tprod.

§5: The Oudom-Guin ★ product on S(L) (Q3)

Oudom-Guin (2008) Definition 2.9 defines the ★ product on S(L) by A ★ B := (A ○ B₍₁₎) · B₍₂₎, Sweedler-summed over the coproduct.

Lemma 2.10 shows ★ is associative (and makes (S(L), ★, Δ) a Hopf algebra). The proof is 6 lines of algebra using Prop 2.7.iii (circ_mul_distrib_via_comul), Prop 2.8.v (circ_assoc_via_comul, Q2), and cocommutativity of Δ (Coalgebra.IsCocomm — landed sorry-free in Q1a's Bialgebra file).

noncomputable def PreLie.OudomGuinCirc.oudomGuinStar {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : SymmetricAlgebra R L

The Oudom-Guin ★ product on S(L) (Oudom-Guin 2008 Def 2.9): A ★ B := (A ○ B₍₁₎) · B₍₂₎, Sweedler-summed over Δ(B).

Equations

• PreLie.OudomGuinCirc.oudomGuinStar A B = (LinearMap.mul' R (SymmetricAlgebra R L)) ((TensorProduct.map (PreLie.OudomGuinCirc.oudomGuinCirc A) LinearMap.id) (CoalgebraStruct.comul B))

def PreLie.OudomGuinCirc.«term_★_» : Lean.TrailingParserDescr

Notation for the Oudom-Guin ★ product.

Equations

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

@[simp]

theorem PreLie.OudomGuinCirc.oudomGuinStar_def {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : oudomGuinStar A B = (LinearMap.mul' R (SymmetricAlgebra R L)) ((TensorProduct.map (oudomGuinCirc A) LinearMap.id) (CoalgebraStruct.comul B))

theorem PreLie.OudomGuinCirc.oudomGuinStar_assoc {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B C : SymmetricAlgebra R L) : oudomGuinStar (oudomGuinStar A B) C = oudomGuinStar A (oudomGuinStar B C)

Oudom-Guin Lemma 2.10: the ★ product is associative.

Proof structure (6-line algebraic chain from OG paper p. 7):

(A ★ B) ★ C
  = (((A ○ B₁) · B₂) ○ C₁) · C₂                [def of ★]
  = ((A ○ B₁) ○ C₁) · (B₂ ○ C₂) · C₃          [Prop 2.7.iii]
  = (A ○ ((B₁ ○ C₁) · C₂)) · (B₂ ○ C₃) · C₄   [Prop 2.8.v / Q2]
  = (A ○ ((B₁ ○ C₁) · C₃)) · (B₂ ○ C₂) · C₄   [cocomm of Δ — Q1a]
  = A ★ ((B ○ C₁) · C₂)                        [def of ★ + Prop 2.7.iii]
  = A ★ (B ★ C)                                [def of ★]

Sorry-fenced: depends on circ_mul_distrib_via_comul (Prop 2.7.iii) and circ_assoc_via_comul (Prop 2.8.v / Q2). Both are sorry'd pending the construction of oudomGuinCirc (Q1b). Once Q1b lands, the 6-line chain becomes concrete Sweedler manipulations (~50-100 LOC in Lean, given Lean's verbosity with TensorProduct).