The Guin-Oudom isomorphism for pre-Lie algebras

@cite{oudom-guin-2008} @cite{foissy-typed-decorated-rooted-trees-2018} @cite{chapoton-livernet-2001} @cite{manchon-2011}

Let (L, ▷) be a (right) pre-Lie algebra over a commutative ring R. The Guin-Oudom theorem (Oudom-Guin 2008) states that the symmetric algebra S(L) carries a canonical non-commutative product ★ such that (S(L), ★) is associative and isomorphic as an R-algebra to the universal enveloping algebra U(L_Lie) of the Lie algebra obtained from L by antisymmetrization.

This file builds the abstract substrate. Specialization to InsertionAlgebra α (the pre-Lie algebra on nonplanar rooted trees, Foissy 2018 Prop 2.2) is in Linglib/Core/Algebra/RootedTree/PreLie/, and the Grossman-Larson product on ConnesKreimer ℤ (Nonplanar α) ≅ S(InsertionAlgebra α) is in R.5.

Convention

We use the right pre-Lie convention associator x y z = associator x z y throughout, matching RightPreLieRing/RightPreLieAlgebra. Foissy 2018 uses the LEFT pre-Lie convention; the conversion is the Lᵐᵒᵖ opposite multiplication and is mediated by mathlib's RightPreLieRing.instLeftPreLieRingMop. Foissy formulas can be cited after the convention swap.

Main definitions

For a RightPreLieAlgebra R L:

• PreLie.GuinOudom.preLieAction — the pre-Lie action ▷ : L →ₗ[R] Der R (S(L)) (S(L)) extending x ▷ ι y = ι (y * x) via SymmetricAlgebra.liftDerivation (the mathlib-gap substrate, in the sibling file Core/LinearAlgebra/SymmetricAlgebra/Derivation.lean).
• PreLie.GuinOudom.M — Manchon's operator M_a u := ι(a) · u − (a ▷ u), bundled as L →ₗ[R] End(S(L)). The MINUS sign (vs Manchon's PLUS) compensates for the right-to-left pre-Lie translation.
• PreLie.GuinOudom.MLieHom — M as a Lie algebra morphism, witnessed by M_lie_hom : M ⁅a, b⁆ = ⁅M a, M b⁆ for the mathlib LieAdmissibleRing bracket.
• PreLie.GuinOudom.MAlgHom — the lift U(L_Lie) →ₐ[R] End(S(L)) via UniversalEnvelopingAlgebra.lift R MLieHom.
• PreLie.GuinOudom.η — Manchon's η : U(L_Lie) →ₗ[R] S(L), defined as η(u) := MAlgHom u 1.

TODO

• ★ : SymmetricAlgebra R L → SymmetricAlgebra R L → SymmetricAlgebra R L — the Guin-Oudom product, naturally defined as s ★ t := η(η⁻¹(s) · η⁻¹(t)). Requires η to be an isomorphism, i.e. the PBW theorem for U(L_Lie) ≅ S(L) as filtered modules. Mathlib does not currently have PBW (no Poincare/BirkhoffWitt/Witt/PBW namespace; no SymmetricAlgebra ≃ UEA; no associated-graded for UEA; only adjacent is UEA(FreeLieAlg X) ≃ FreeAlgebra X in Mathlib.Algebra.Lie.Free which doesn't generalize). Blocked on PBW upstream.
• guinOudom : (SymmetricAlgebra R L, ★) ≃ₐ[R] UniversalEnvelopingAlgebra R L — the Guin-Oudom isomorphism. Same blocker.
• For downstream Δ^c coassociativity on ConnesKreimer ℤ (Nonplanar α), the Grossman-Larson product is defined directly via Foissy 2021 Theorem 5.1's combinatorial formula in Linglib/Core/Algebra/RootedTree/GrossmanLarson.lean, bypassing the abstract ★ and the PBW dependency.

Sanity tests: Lie instances are inferable from RightPreLieRing

Mathlib's instance chain RightPreLieRing → LieAdmissibleRing → LieRing (Mathlib/Algebra/NonAssoc/LieAdmissible/Defs.lean, Tapia 2025) makes the Lie bracket [x, y] := x * y - y * x automatic. Same for the algebra version. We don't need any manual derivation in linglib.

§1: The pre-Lie action ▷ : L × S(L) → S(L)

For a RightPreLieAlgebra R L, the pre-Lie product · : L × L → L extends canonically to an R-linear "action" ▷ : L → S(L) → S(L) via Leibniz, using the substrate SymmetricAlgebra.liftDerivation. Specifically, for fixed x : L, the function y ↦ ι (x * y) : L → S(L) lifts to a self-derivation δ_x of S(L). The collection {δ_x}_{x : L} packages as a linear map from L to Derivation R (S(L)) (S(L)).

noncomputable def PreLie.GuinOudom.preLieAction {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] : L →ₗ[R] Derivation R (SymmetricAlgebra R L) (SymmetricAlgebra R L)

The pre-Lie action of L on SymmetricAlgebra R L, as a linear map L →ₗ[R] Derivation R (S(L)) (S(L)): for each x : L, the unique self-derivation extending y ↦ ι (x * y). Composition of actionLinearMapBundled with the substrate equivalence SymmetricAlgebra.liftDerivation.

Equations

• PreLie.GuinOudom.preLieAction = ↑SymmetricAlgebra.liftDerivation ∘ₗ PreLie.GuinOudom.actionLinearMapBundled✝

def PreLie.GuinOudom.«term_▷_» : Lean.TrailingParserDescr

Notation for the pre-Lie action: x ▷ s for preLieAction x s.

Equations

• PreLie.GuinOudom.«term_▷_» = Lean.ParserDescr.trailingNode `PreLie.GuinOudom.«term_▷_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ▷ ") (Lean.ParserDescr.cat `term 76))

@[simp]

theorem PreLie.GuinOudom.preLieAction_ι {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (x y : L) : (preLieAction x) ((SymmetricAlgebra.ι R L) y) = (SymmetricAlgebra.ι R L) (y * x)

@[simp]

theorem PreLie.GuinOudom.preLieAction_one {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (x : L) : (preLieAction x) 1 = 0

theorem PreLie.GuinOudom.preLieAction_mul {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (x : L) (s t : SymmetricAlgebra R L) : (preLieAction x) (s * t) = s • (preLieAction x) t + t • (preLieAction x) s

§2: Manchon's M operator and the Lie algebra morphism

For a RightPreLieAlgebra R L, define M_a : S(L) →ₗ[R] S(L) by M_a u := ι(a) · u − (a ▷ u) (Manchon 2009 Theorem 1.1 adapted for right pre-Lie). The collection {M_a}_{a : L} packages into a linear map M : L →ₗ[R] End(S(L)). The key result (M_lie_hom) is that M is a Lie algebra morphism: M_⁅a, b⁆ = ⁅M_a, M_b⁆.

This is the bridge that lets us extend M via the universal enveloping algebra: M : L →ₗ⁅R⁆ End(S(L)) lifts to an algebra hom M' : U(L_Lie) →ₐ[R] End(S(L)) via UniversalEnvelopingAlgebra.lift.

Sign convention: Manchon's exposition uses LEFT pre-Lie convention where [a, b] := a ▷ b − b ▷ a matches mathlib's LieAdmissibleRing bracket a*b − b*a. In our RIGHT pre-Lie convention, the translated a ▷_LEFT b = b *_RIGHT a gives [a,b]_Manchon = b*a − a*b = −[a,b]_LA. The MINUS sign in M_a u := ι(a)·u − (a ▷ u) (vs Manchon's plus) compensates: with this M, [M_a, M_b] = M_{[a,b]_LA} for mathlib's bracket. (Verified by explicit calculation; the right pre-Lie identity gives [L_a, L_b] = −L_{[a,b]_LA}, and the cross-term sign in L_a(ι(b)·u) flips to absorb it.)

Proof sketch:

M_a M_b u  = M_a (ι(b)·u − (b ▷ u))
           = ι(a)·ι(b)·u − ι(a)·(b▷u) − L_a(ι(b)·u) + L_a L_b u
           = ι(a)·ι(b)·u − ι(a)·(b▷u) − ι(b)·L_a u − ι(b*a)·u + L_a L_b u   (Leibniz)

⁅M_a, M_b⁆ u = (ι(a*b) − ι(b*a))·u + ⁅L_a, L_b⁆ u
            = ι([a,b]_LA)·u − L_{[a,b]_LA} u                                (anti-morphism)
            = M_⁅a, b⁆ u

where [a, b]_LA = a*b − b*a is mathlib's LieAdmissible commutator.

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

Manchon's M operator: for each a : L, the linear endomorphism of S(L) given by M_a u := ι(a) · u − (a ▷ u). Bundled as a linear map L →ₗ[R] End(S(L)).

Sign convention: the MINUS (vs Manchon's PLUS) compensates for the right ↔ left pre-Lie translation, ensuring M is a Lie hom for mathlib's LieAdmissibleRing bracket [a,b] := a*b − b*a.

Equations

• PreLie.GuinOudom.M = { toFun := fun (a : L) => LinearMap.mulLeft R ((SymmetricAlgebra.ι R L) a) - ↑(PreLie.GuinOudom.preLieAction a), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PreLie.GuinOudom.M_apply {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a : L) (u : SymmetricAlgebra R L) : (M a) u = (SymmetricAlgebra.ι R L) a * u - (preLieAction a) u

@[simp]

theorem PreLie.GuinOudom.M_apply_one {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a : L) : (M a) 1 = (SymmetricAlgebra.ι R L) a

preLieAction is a Lie ANTI-morphism

Key intermediate result: ⁅preLieAction a, preLieAction b⁆ = -preLieAction ⁅a, b⁆ as derivations of S(L). Equivalently, preLieAction : L → Der S(L) is a Lie hom into the OPPOSITE Lie algebra structure on derivations.

The sign comes from our right pre-Lie convention: with T ▷ Y = ι(Y * T) (T on right of pre-Lie), the commutator [L_a, L_b] u for u ∈ L expands to ι((u*b)*a − (u*a)*b), which by the right pre-Lie identity (associator symmetric in last two) equals ι(u*(b*a) − u*(a*b)) = ι(−u*[a,b]_LA) = −L_{[a,b]_LA} u.

M is a Lie algebra morphism

The deep step. By Manchon (2009) Theorem 1.1, the operator M_a u := ι(a) · u − (a ▷ u) is a Lie algebra morphism L → End(S(L)). This is the bridge that lets us extend M via the universal enveloping algebra U(L_Lie).

theorem PreLie.GuinOudom.M_lie_hom {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a b : L) : M ⁅a, b⁆ = ⁅M a, M b⁆

Main result of §2: M is a Lie algebra morphism L → End(S(L)). For all a, b : L, M_⁅a, b⁆ = ⁅M_a, M_b⁆ where the bracket on End(S(L)) is the commutator under composition.

By Manchon (2009) Theorem 1.1 (adapted to right pre-Lie convention with the sign correction). The proof unwinds the commutator pointwise on S(L), expands M_a (ι(b) · u - L_b u) via Leibniz, and uses the right pre-Lie identity (encapsulated as preLieAction_lie_anti) to identify the remaining [L_a, L_b] u term with -L_⁅a, b⁆ u.

§3: Lift to the universal enveloping algebra

M : L →ₗ⁅R⁆ End(S(L)) is a Lie algebra morphism (M_lie_hom). By the universal property of UniversalEnvelopingAlgebra, this extends uniquely to an R-algebra morphism MAlgHom : U(L_Lie) →ₐ[R] End(S(L)).

noncomputable def PreLie.GuinOudom.MLieHom {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] : L →ₗ⁅R⁆ Module.End R (SymmetricAlgebra R L)

M bundled as a Lie algebra morphism L →ₗ⁅R⁆ End(S(L)), where the Lie structure on End(S(L)) is the commutator under composition (via Module.End's associative ring structure).

Equations

• PreLie.GuinOudom.MLieHom = { toLinearMap := PreLie.GuinOudom.M, map_lie' := ⋯ }

@[simp]

theorem PreLie.GuinOudom.MLieHom_apply {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a : L) : MLieHom a = M a

noncomputable def PreLie.GuinOudom.MAlgHom {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] : UniversalEnvelopingAlgebra R L →ₐ[R] Module.End R (SymmetricAlgebra R L)

The lift of M to the universal enveloping algebra of L_Lie via UniversalEnvelopingAlgebra.lift. This is the algebra hom M' : U(L_Lie) →ₐ[R] End(S(L)) of Manchon (2009) Theorem 1.1.

Equations

• PreLie.GuinOudom.MAlgHom = (UniversalEnvelopingAlgebra.lift R) PreLie.GuinOudom.MLieHom

@[simp]

theorem PreLie.GuinOudom.MAlgHom_ι {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a : L) : MAlgHom ((UniversalEnvelopingAlgebra.ι R) a) = M a

§4: Manchon's η : U(L_Lie) →ₗ[R] S(L)

Define η(u) := M'(u) (1). Manchon's key insight: η is a filtered linear isomorphism (PBW-style argument), so the U(L_Lie) algebra structure transports to S(L) via η⁻¹, giving the Guin-Oudom product ★. The iso theorem itself is C3 (R.4.3).

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

Manchon's η: the linear map U(L_Lie) →ₗ[R] S(L) defined by η(u) := M'(u) (1).

Equations

• PreLie.GuinOudom.η = { toFun := fun (u : UniversalEnvelopingAlgebra R L) => (PreLie.GuinOudom.MAlgHom u) 1, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PreLie.GuinOudom.η_apply {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (u : UniversalEnvelopingAlgebra R L) : η u = (MAlgHom u) 1

@[simp]

theorem PreLie.GuinOudom.η_ι {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] (a : L) : η ((UniversalEnvelopingAlgebra.ι R) a) = (SymmetricAlgebra.ι R L) a

@[simp]

theorem PreLie.GuinOudom.η_one {R : Type u_1} [CommRing R] {L : Type u_2} [RightPreLieRing L] [RightPreLieAlgebra R L] : η 1 = 1