Construction of OG T ○ A for T ∈ L, A ∈ Sym[R]^n L (Q1b)

For a pre-Lie algebra L and T ∈ L, this file constructs the OG T ○ · operation on each symmetric power Sym[R]^n L → L via Oudom-Guin Definition 2.4's recursion:

T ○_(0) (·) := T                                              -- input from Fin 0
T ○_(n+1) (a₁, …, aₙ, aₙ₊₁) := (T ○_(n) (a₁, …, aₙ)) * aₙ₊₁
                              - Σᵢ T ○_(n) (a₁, …, aᵢ * aₙ₊₁, …, aₙ)

where * is the pre-Lie product on L.

Oudom-Guin Lemma 2.5 shows T ○_(n) is symmetric in the n arguments — the key fact making this descend to Sym[R]^n L → L.

Main definitions

• circTMultilinear T n — T ○_(n) (·) as a MultilinearMap R (Fin n → L) L.
• circT T n — the lift to Sym[R]^n L →ₗ[R] L via SymmetricPower.lift, using circTMultilinear_symm (Lemma 2.5).

Status

Q1b: circT T n sorry-free (2026-05-16). Symmetry (circTMultilinear_symm) closed via three helpers:

• circTMultilinear_symm_interior — swap of two Fin.castSucc indices; uses IH on prev.
• circTMultilinear_symm_exterior — swap of one Fin.castSucc with Fin.last n; case-splits adjacent / non-adjacent. Non-adjacent reduces to adjacent via interior-swap conjugation (Equiv.swap_apply_apply). Adjacent (circTMultilinear_symm_exterior_adj) goes via the six-term decomposition (circT_succ_succ_snoc_eval — three circTMultilinear_succ unfolds) and algebraic symmetry (sixTerm_symm — pre-Lie identity for pair 1, per-degree OG identity (2.3) prev_action_pre_lie_identity for pair 2, add_comm for pair 3).
• circTMultilinear_symm_swap / circTMultilinear_symm — dispatcher + main theorem.

Q1b can now proceed to combine per-degree pieces via the TensorAlgebra detour.

References

• @cite{oudom-guin-2008} Def 2.4 + Lemma 2.5.

§1: The recursive multilinear T ○_(n) (·)

Per OG Def 2.4. We use mathlib's MultilinearMap.constOfIsEmpty for the base case (n = 0) and a recursive construction for n + 1 using the formula above.

noncomputable def PreLie.OudomGuinCircConstruct.circTMultilinear (R : Type) [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) : MultilinearMap R (fun (x : Fin n) => L) L

The OG T ○_(n) (·) as a multilinear map (Fin n → L) → L, defined recursively per Def 2.4.

Note: R is made explicit (rather than implicit) so that recursive calls within the definition can resolve typeclasses.

Equations

• One or more equations did not get rendered due to their size.
• PreLie.OudomGuinCircConstruct.circTMultilinear R T 0 = MultilinearMap.constOfIsEmpty R (fun (x : Fin 0) => L) T

@[simp]

theorem PreLie.OudomGuinCircConstruct.circTMultilinear_zero {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (f : Fin 0 → L) : (circTMultilinear R T 0) f = T

Recursive equation: circTMultilinear T 0 _ = T.

theorem PreLie.OudomGuinCircConstruct.circTMultilinear_succ {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) (f : Fin (n + 1) → L) : (circTMultilinear R T (n + 1)) f = (circTMultilinear R T n) (Fin.init f) * f (Fin.last n) - ∑ i : Fin n, (circTMultilinear R T n) (Function.update (Fin.init f) i (Fin.init f i * f (Fin.last n)))

Recursive equation: circTMultilinear T (n+1) f follows Def 2.4.

§2: Symmetry (Lemma 2.5)

The key OG Lemma 2.5: T ○_(n) (·) is symmetric in the n arguments, i.e., (circTMultilinear T n).domDomCongr σ = circTMultilinear T n for any σ : Equiv.Perm (Fin n).

Proof decomposition (this section). We split into three sub-claims:

1. Interior swap invariance (circTMultilinear_symm_interior): for i, j : Fin n, invariance of circTMultilinear R T (n+1) under Equiv.swap (Fin.castSucc i) (Fin.castSucc j). Proved by IH on n (the swap acts within Fin.init; f_last is unchanged).

2. Exterior swap invariance (circTMultilinear_symm_exterior): for i : Fin n, invariance of circTMultilinear R T (n+1) under Equiv.swap (Fin.castSucc i) (Fin.last n). Reduces to the adjacent case i = Fin.last (n-1) via conjugation by interior swaps; the adjacent case uses RightPreLieRing.assoc_symm'.

3. Any-swap invariance (circTMultilinear_symm_swap): combines (1) and (2) via a case-split on whether either of x, y : Fin (n+1) is Fin.last n.

4. Main theorem (circTMultilinear_symm): reduces general σ to (3) via Equiv.Perm.swap_induction_on.

Status (Lemma 2.5 — closed sorry-free 2026-05-16). All four pieces are sorry-free. The substantive content lives in circTMultilinear_symm_exterior_adj (adjacent case via six-term decomposition + algebraic symmetry); other pieces are structural.

§2.0: Small-arity evaluation lemmas

Direct evaluation of circTMultilinear R T n for n = 1, 2. Useful for the n = 1 base case of the exterior swap closure (Lemma 2.5).

@[simp]

theorem PreLie.OudomGuinCircConstruct.circTMultilinear_one_eval {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (g : Fin 1 → L) : (circTMultilinear R T 1) g = T * g 0

circTMultilinear R T 1 g = T * g 0.

theorem PreLie.OudomGuinCircConstruct.circTMultilinear_two_eval {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (g : Fin 2 → L) : (circTMultilinear R T 2) g = T * g 0 * g 1 - T * (g 0 * g 1)

circTMultilinear R T 2 g = (T * g 0) * g 1 - T * (g 0 * g 1).

§2.A: OG identity (2.3) at per-degree level

For any multilinear prev : MultilinearMap R (Fin n → L) L, the identity prev (a ○ (X·Y)) − prev ((a ○ X) ○ Y) = prev (a ○ (Y·X)) − prev ((a ○ Y) ○ X) holds, where prev (g ○ X) := Σ_i prev (Function.update g i (g i * X)).

This follows from the L pre-Lie identity applied to each tuple position plus a relabel symmetry on the off-diagonal (i ≠ j) terms.

Proved as a substrate lemma here for use in the exterior swap invariance (Lemma 2.5) closure.

§2.A2: Six-term decomposition + symmetry

The OG paper unfolds T ○_{n+2} twice via Def 2.4 to get a six-term expression in (prev, A, X, Y). Lemma 2.5 reduces to showing that this six-term form is symmetric under X ↔ Y, which follows from the L pre-Lie identity (for the pA·X·Y and pA·(X·Y) terms) and the per-degree OG identity (2.3) (prev_action_pre_lie_identity) for the inner-sum terms.

§2.B: Adjacent-exterior swap helper

The substantive content of Lemma 2.5's exterior case lives here, in the "adjacent" case: invariance of circT (m+3) under the swap of the last two positions (m+1, m+2). The general exterior swap reduces to this via conjugation by an interior swap (see circTMultilinear_symm_exterior).

This split lets the non-adjacent case appeal to the adjacent case as a plain hypothesis rather than mutually-recursing inside the dispatcher.

theorem PreLie.OudomGuinCircConstruct.circTMultilinear_symm (R : Type) [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) (σ : Equiv.Perm (Fin n)) : MultilinearMap.domDomCongr σ (circTMultilinear R T n) = circTMultilinear R T n

OG Lemma 2.5: T ○_(n) (·) is symmetric in its n arguments.

§3: Lift to Sym[R]^n L → L

Using SymmetricPower.lift (Q1b.0a) and circTMultilinear_symm (Lemma 2.5), we obtain the OG operation on each symmetric power.

noncomputable def PreLie.OudomGuinCircConstruct.circT {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) : SymmetricPower R (Fin n) L →ₗ[R] L

OG T ○_(n) (·) lifted to Sym[R]^n L →ₗ[R] L via the universal property of the symmetric power.

Equations

• PreLie.OudomGuinCircConstruct.circT T n = SymmetricPower.lift (PreLie.OudomGuinCircConstruct.circTMultilinear R T n) ⋯

@[simp]

theorem PreLie.OudomGuinCircConstruct.circT_tprod {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) (f : Fin n → L) : (circT T n) ((SymmetricPower.tprod R) f) = (circTMultilinear R T n) f

@[simp]

theorem PreLie.OudomGuinCircConstruct.circT_zero_tprod {R L : Type} [CommRing R] [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (f : Fin 0 → L) : (circT T 0) ((SymmetricPower.tprod R) f) = T

For n = 0: circT T 0 sends the unit tprod R Fin.elim0 to T.