The Oudom-Guin ○ operation on SymmetricAlgebra R L

[OG08]

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 Mathlib.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

• [OG08] — original construction, §2.
• [manchon-2011] — survey, Theorem 1.1 (Manchon route, alternative).
• [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : circHom ((SymmetricAlgebra.ι R L) T) = circGen T

theorem PreLie.OudomGuinCirc.oudomGuinCirc_eq_ofConv {R : Type u_1} [CommRing R] {L : Type u_2} [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 witnessing that the construction satisfies the defining equations. (The uniqueness clause of Prop 2.7 is not yet formalized.)

theorem PreLie.OudomGuinCirc.circ_one_right {R : Type u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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.oudomGuinCirc_mul_ι {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) (X : L) : (oudomGuinCirc (A * B)) ((SymmetricAlgebra.ι R L) X) = (oudomGuinCirc A) ((SymmetricAlgebra.ι R L) X) * B + A * (oudomGuinCirc B) ((SymmetricAlgebra.ι R L) X)

Leibniz form for oudomGuinCirc · (ι X) on a product: (A * B) ○ ι X = (A ○ ι X) * B + A * (B ○ ι X).

Follows from Prop 2.7 (iii) applied at C = ι X, where comul (ι X) = ι X ⊗ 1 + 1 ⊗ ι X (since ι X is primitive) and _ ○ 1 = _ (circ_one_right).

theorem PreLie.OudomGuinCirc.oudomGuinCirc_algHomL_tprod_ι {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (X : L) (m : ℕ) (a : Fin m → L) : (oudomGuinCirc (OudomGuinCircConstruct.algHomL ((TensorAlgebra.tprod R L m) a))) ((SymmetricAlgebra.ι R L) X) = ∑ i : Fin m, OudomGuinCircConstruct.algHomL ((TensorAlgebra.tprod R L m) (Function.update a i (a i * X)))

Derivation formula for monomials: for a tprod z = tprod_m a in TA, the image B = algHomL z = ι(a₀) · ... · ι(a_{m-1}) ∈ S(L) satisfies oudomGuinCirc B (ι X) = Σᵢ algHomL (tprod_m (update a i (a i * X))).

Proven by induction on m; base case uses one_circ, step uses Prop 2.7 (iii)

• comul_ι + circ_one_right + circ_ι_ι.

Made public (originally private) for use in BMinusSL's psiA_L_circByT_total_eq proof — provides the Leibniz expansion of (∏ ι(a i)) ○ ι X.

theorem PreLie.OudomGuinCirc.circ_T_mul {R : Type u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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 2.8 (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 u_1} [CommRing R] {L : Type u_2} [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 u_1} [CommRing R] {L : Type u_2} [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))

noncomputable def PreLie.OudomGuinCirc.oudomGuinStarL {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A : SymmetricAlgebra R L) : SymmetricAlgebra R L →ₗ[R] SymmetricAlgebra R L

LinearMap form of oudomGuinStar A : S(L) → S(L). Since ★ is R-linear in its second argument (definition uses mul', TP.map, and Coalgebra.comul, all R-linear), we can promote A ↦ A ★ · to a LinearMap.

Required for TA-side lifting (algHomL_surjective + TA_linearMap_ext_tprod): the lift framework operates on linear maps TA → S(L), and oudomGuinStarL provides the right shape.

Equations

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

@[simp]

theorem PreLie.OudomGuinCirc.oudomGuinStarL_apply {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : (oudomGuinStarL A) B = oudomGuinStar A B

Helpers for oudomGuinStar_assoc

The proof of ★-associativity follows the OG paper p. 7 algebraic chain. Both (A★B)★C and A★(B★C) reduce to multilinear forms in cm B and a Δ³-iterate on C. They differ by a 2-3 swap on the 4-tensor Δ³(C), which is killed by comul_squared_TTTC_eq (cocommutativity in Δ³ form).

theorem PreLie.OudomGuinCirc.oudomGuinStar_one {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (X : SymmetricAlgebra R L) : oudomGuinStar X 1 = X

Helper for Q3: X ★ 1 = X for any X : S(L).

Direct: X ★ 1 = (mul' ∘ TP.map (○X) id)(cm 1) = (mul' ∘ TP.map (○X) id)(1⊗1) = (X ○ 1) · 1 = X · 1 = X (via circ_one_right and mul_one).

theorem PreLie.OudomGuinCirc.oudomGuinStar_add_right {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (X Y Z : SymmetricAlgebra R L) : oudomGuinStar X (Y + Z) = oudomGuinStar X Y + oudomGuinStar X Z

Helper for Q3: ★ is linear in its second argument.

oudomGuinStar X (Y + Z) = oudomGuinStar X Y + oudomGuinStar X Z.

theorem PreLie.OudomGuinCirc.oudomGuinStar_smul_right {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (X Y : SymmetricAlgebra R L) (r : R) : oudomGuinStar X (r • Y) = r • oudomGuinStar X Y

Helper for Q3: ★ distributes over scalar multiplication in its second argument.

theorem PreLie.OudomGuinCirc.oudomGuinStar_zero_left {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (B : SymmetricAlgebra R L) : oudomGuinStar 0 B = 0

Left zero: 0 ★ B = 0. Direct from linearity of oudomGuinCirc in its first argument.

theorem PreLie.OudomGuinCirc.oudomGuinStar_add_left {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A₁ A₂ B : SymmetricAlgebra R L) : oudomGuinStar (A₁ + A₂) B = oudomGuinStar A₁ B + oudomGuinStar A₂ B

Left additivity: (A₁ + A₂) ★ B = A₁ ★ B + A₂ ★ B. Direct from linearity of oudomGuinCirc in its first argument.

theorem PreLie.OudomGuinCirc.oudomGuinStar_smul_left {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (r : R) (A B : SymmetricAlgebra R L) : oudomGuinStar (r • A) B = r • oudomGuinStar A B

Left scalar compatibility: (r • A) ★ B = r • (A ★ B). Direct from linearity of oudomGuinCirc in its first argument.

theorem PreLie.OudomGuinCirc.oudomGuinStar_one_left {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (B : SymmetricAlgebra R L) : oudomGuinStar 1 B = B

Left unit: 1 ★ B = B. The Bialgebra counit-comul triangle.

1 ★ B = mul' (TP.map (○1) id (cm B)). Using one_circ, ○1 = algebraMap ∘ algebraMapInv (composition of counit and unit). Then the LHS reduces via Coalgebra.rTensor_counit_comul: (algebraMapInv ⊗ id) (cm B) = 1 ⊗ B, and mul' ∘ (algebraMap ⊗ id) (1 ⊗ B) = algebraMap 1 * B = 1 * B = B.

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

Bilinear LinearMap form of ★ : S(L) × S(L) → S(L).

Promotes oudomGuinStar to a doubly-linear S →ₗ[R] S →ₗ[R] S. Used as the input to TensorProduct.lift to build the (S⊗S) → S map μ_★ := TP.lift oudomGuinStarBilin, which in turn is the building block for tprodStarMul (the ★-multiplication on the tensor product Hopf algebra S⊗S).

Right-linearity comes for free from oudomGuinStar's definition (RHS is mul', TP.map, Coalgebra.comul — all R-linear). Left-linearity is witnessed by oudomGuinStar_add_left, oudomGuinStar_smul_left.

Equations

• PreLie.OudomGuinCirc.oudomGuinStarBilin = LinearMap.mk₂ R PreLie.OudomGuinCirc.oudomGuinStar ⋯ ⋯ ⋯ ⋯

@[simp]

theorem PreLie.OudomGuinCirc.oudomGuinStarBilin_apply {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : (oudomGuinStarBilin A) B = oudomGuinStar A B

noncomputable def PreLie.OudomGuinCirc.tprodStarMul {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] : TensorProduct R (TensorProduct R (SymmetricAlgebra R L) (SymmetricAlgebra R L)) (TensorProduct R (SymmetricAlgebra R L) (SymmetricAlgebra R L)) →ₗ[R] TensorProduct R (SymmetricAlgebra R L) (SymmetricAlgebra R L)

Tensor-product ★ multiplication on S(L) ⊗ S(L). Maps a 4-tensor (a ⊗ b) ⊗ (c ⊗ d) to (a ★ c) ⊗ (b ★ d).

Constructed as (TP.map μ_★ μ_★) ∘ TTTC where μ_★ := TP.lift oudomGuinStarBilin : (S⊗S) →ₗ[R] S. TTTC reshuffles the 4-tensor from (a⊗b) ⊗ (c⊗d) to (a⊗c) ⊗ (b⊗d), then the pointwise μ_★ collapses each pair.

Used to state the Hopf axiom Δ(x ★ y) = tprodStarMul((Δx) ⊗ (Δy)).

Equations

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

@[simp]

theorem PreLie.OudomGuinCirc.tprodStarMul_tmul {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a b c d : SymmetricAlgebra R L) : tprodStarMul (a ⊗ₜ[R] b ⊗ₜ[R] (c ⊗ₜ[R] d)) = oudomGuinStar a c ⊗ₜ[R] oudomGuinStar b d

theorem PreLie.OudomGuinCirc.comul_oudomGuinStar_mul {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (x y : SymmetricAlgebra R L) : CoalgebraStruct.comul (oudomGuinStar x y) = tprodStarMul (CoalgebraStruct.comul x ⊗ₜ[R] CoalgebraStruct.comul y)

theorem PreLie.OudomGuinCirc.counit_oudomGuinStar {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (A B : SymmetricAlgebra R L) : SymmetricAlgebra.algebraMapInv (oudomGuinStar A B) = SymmetricAlgebra.algebraMapInv A * SymmetricAlgebra.algebraMapInv B

Counit-multiplicativity for ★: ε(A ★ B) = ε(A) · ε(B).

Direct analog of counit_circ (counit-multiplicativity for ○), and a consequence of (S(L), ★, Δ) being a Hopf algebra (OG Lemma 2.10).

Strategy: no induction on A needed (unlike counit_circ). ★ is defined via mul', TP.map (○A) id, and cm. Push ε through mul' via AlgHom.comp_mul'; fuse the nested TP.maps via TP.map_comp; substitute ε ∘ₗ ○A = ε A • ε via counit_circ in linear-map form; pull the scalar out of TP.map, then through mul'; close via mul'_map_algebraMapInv_comul (the counit-comul triangle).

Independent value: required for the Q5c pairing-route closure (z = 1 base case of gl_product_eq_oudomGuinStar_via_pairing reduces to this).

theorem PreLie.OudomGuinCirc.oudomGuinStar_ι_split {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (X : SymmetricAlgebra R L) (T : L) : oudomGuinStar X ((SymmetricAlgebra.ι R L) T) = (oudomGuinCirc X) ((SymmetricAlgebra.ι R L) T) + X * (SymmetricAlgebra.ι R L) T

Helper for Q3 (ι T split): For any X : S(L) and T : L: X ★ ι T = X ○ ι T + X · ι T.

Direct: unfold X ★ ι T = mul'(TP.map (○X) id (cm ι T)) with primitive cm ι T = ι T ⊗ 1 + 1 ⊗ ι T, distribute, apply circ_one_right and mul_one.

theorem PreLie.OudomGuinCirc.oudomGuinStar_mul_ι_split {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (Z X : SymmetricAlgebra R L) (T : L) : oudomGuinStar Z (X * (SymmetricAlgebra.ι R L) T) = (oudomGuinCirc (oudomGuinStar Z X)) ((SymmetricAlgebra.ι R L) T) + oudomGuinStar Z X * (SymmetricAlgebra.ι R L) T - oudomGuinStar Z ((oudomGuinCirc X) ((SymmetricAlgebra.ι R L) T))

Closed-form identity for Z ★ (X · ι T). Key for closing Q3's per-tprod succ m case.

Z ★ (X · ι T) = (Z ★ X) ○ ι T + (Z ★ X) · ι T - Z ★ (X ○ ι T).

Derived by Sweedler bash on cm X: expand cm(X·ιT) = cm X · cm(ιT), apply 3.9.iv (circ_general_mul_ι) on the Z ○ (x₁·ιT) summand, then identify the residual sums via 2.7.iii applied to (Z★X)○ιT and comul_circ applied to Z★(X○ιT). The TP-induction on cm X is sound because both sides are linear in cm X (the structural relationship between X and cm X is irrelevant once both sides are expanded — they're equal as functions of cm X for ANY tensor).

This identity expresses Z★(X·ιT) in terms of Z★X and X○ιT. In per-tprod context with X = D = algHomL(tprod m a'), X ○ ι T is a sum of tprods at the same m (via oudomGuinCirc_algHomL_tprod_ι), so Q3's m+1 case reduces to Q3 at m by linearity in C — no Sweedler cocomm bash needed at all.

theorem PreLie.OudomGuinCirc.oudomGuinStar_assoc {R : Type u_1} [CommRing R] {L : Type u_2} [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.

Lifted from per-tprod (oudomGuinStar_assoc_tprod) via algHomL_surjective + TA_linearMap_ext_tprod. Mirrors Q2's lifting pattern (circ_assoc_via_comul).

Both sides are R-linear maps in C, so checking on tprods suffices.

Note: the previous proof structure used SymmetricAlgebra.induction on C with algebraMap r, ι T, add, mul cases. The first three closed sorry-free; the mul X Y case had no closed-form decomposition (the IHs for X and Y don't compose multiplicatively via ★, and TP-induction on cm(X·Y) is unsound — counterexample: A = ι T, B = 1, cmC' = ι X ⊗ ι Y gives LHS = ι(T·X)·ι Y ≠ 0 = RHS). The per-tprod approach gives a cleaner structural induction where each m+1 step adds exactly one ι generator.