Q1b Step 1: assemble per-degree circT T n into circByT_total T : SymmetricAlgebra → L

For each n, OudomGuinCircConstruct.circTMultilinear R T n gives a symmetric multilinear map (Fin n → L) → L (sorry-free per Lemma 2.5 at 0.231.112). This file assembles these per-degree pieces into a single linear map

circByT_total T : SymmetricAlgebra R L →ₗ[R] L

via the TensorAlgebra detour:

1. For each n, lift circTMultilinear T n to a linear map on the n-th PiTensorProduct via PiTensorProduct.lift.
2. Assemble across all n via DirectSum.toModule to get (⨁ n, ⨂[R]^n L) →ₗ[R] L.
3. Compose with mathlib's TensorAlgebra.equivDirectSum to get TensorAlgebra R L →ₗ[R] L.
4. Show this respects TensorAlgebra.SymRel (the symmetric-algebra relation ι(x)·ι(y) ~ ι(y)·ι(x)) — substantive content uses circTMultilinear_symm (Lemma 2.5).
5. Lift through the SymmetricAlgebra = RingQuot SymRel quotient.

Composed with mathlib's SymmetricAlgebra.ι : L →ₗ[R] SymmetricAlgebra R L on the codomain, this is the per-T operation ι(T) ○ · of the OG ○. The full oudomGuinCirc (Q1b Step 3) extends this to general left-arguments via OG Prop 2.7.iii.

Status (2026-05-16)

Step 1 fully landed sorry-free (~370 LOC).

• Items 1–3 (per-degree circTPi, graded circTGraded, TensorAlgebra-level circTTensor) — sorry-free.
• Item 4 (circTTensor_symRel: respects SymRel at n = 2 via circTMultilinear_two_eval + RightPreLieRing.assoc_symm') — sorry-free.
• Item 5 (circByT_total: lift through the RingQuot quotient to SymmetricAlgebra R L →ₗ[R] L) — sorry-free via Submodule.liftQ + LinearMap.quotKerEquivOfSurjective on surjective algHomL. The kernel containment ker algHomL ≤ ker (circTTensor T) is proven through: (a) TA_linearMap_ext_tprod (helper — linear maps from TensorAlgebra agreeing on tprods are equal, via equivDirectSum + DirectSum.linearMap_ext
  • PiTensorProduct.ext); (b) circTTensor_swap_general (bilinear extension of circTTensor_swap_tprod to general r, d ∈ TensorAlgebra); (c) RingQuot.Rel/EqvGen induction with the strong motive ∀ r d, circTTensor T (r * z₁ * d) = circTTensor T (r * z₂ * d), closing under add_left/mul_left/mul_right via associativity + additivity.

References

• @cite{oudom-guin-2008} Def 2.4 + Lemma 2.5 (per-degree symmetry).

§1: Per-degree lift via PiTensorProduct.lift

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

Per-degree lift of circTMultilinear R T n to the n-th PiTensorProduct (i.e., ⨂[R]^n L).

Equations

• PreLie.OudomGuinCircConstruct.circTPi T n = PiTensorProduct.lift (PreLie.OudomGuinCircConstruct.circTMultilinear R T n)

@[simp]

theorem PreLie.OudomGuinCircConstruct.circTPi_tprod {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) (g : Fin n → L) : (circTPi T n) ((PiTensorProduct.tprod R) g) = (circTMultilinear R T n) g

§2: Assembly across degrees via DirectSum.toModule

noncomputable def PreLie.OudomGuinCircConstruct.circTGraded {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : (DirectSum ℕ fun (n : ℕ) => TensorPower R n L) →ₗ[R] L

Assembly of all circTPi T n into a linear map from the direct sum of all tensor powers.

Equations

• PreLie.OudomGuinCircConstruct.circTGraded T = DirectSum.toModule R ℕ L fun (n : ℕ) => PreLie.OudomGuinCircConstruct.circTPi T n

@[simp]

theorem PreLie.OudomGuinCircConstruct.circTGraded_of {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (n : ℕ) (x : TensorPower R n L) : (circTGraded T) ((DirectSum.of (fun (n : ℕ) => TensorPower R n L) n) x) = (circTPi T n) x

§3: Composition with TensorAlgebra.equivDirectSum

noncomputable def PreLie.OudomGuinCircConstruct.circTTensor {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : TensorAlgebra R L →ₗ[R] L

Per-T OG operation, on the TensorAlgebra level. Assembled from per-degree circTPi T n via mathlib's TensorAlgebra ≃ₐ ⨁_n ⨂[R]^n L.

Equations

• PreLie.OudomGuinCircConstruct.circTTensor T = PreLie.OudomGuinCircConstruct.circTGraded T ∘ₗ TensorAlgebra.equivDirectSum.toLinearMap

@[simp]

theorem PreLie.OudomGuinCircConstruct.circTTensor_ι {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T x : L) : (circTTensor T) ((TensorAlgebra.ι R) x) = T * x

@[simp]

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

circTTensor T (TensorAlgebra.tprod R L n f) = circTMultilinear R T n f.

§3.A: tprod multiplication

(tprod_m a) * (tprod_n b) = tprod_{m+n} (Fin.append a b). Derived from TensorAlgebra.tprod_apply (which expresses tprod as List.prod of ιs) + List.prod_append + List.ofFn_fin_append.

theorem PreLie.OudomGuinCircConstruct.tprod_mul_tprod {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (m n : ℕ) (a : Fin m → L) (b : Fin n → L) : (TensorAlgebra.tprod R L m) a * (TensorAlgebra.tprod R L n) b = (TensorAlgebra.tprod R L (m + n)) (Fin.append a b)

The product of two tprods is the tprod of the concatenated tuple.

theorem PreLie.OudomGuinCircConstruct.ι_eq_tprod_one {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (x : L) : (TensorAlgebra.ι R) x = (TensorAlgebra.tprod R L 1) fun (x_1 : Fin 1) => x

ι R x = tprod 1 (fun _ => x).

§3.B: Swap-in-product lemma on tprods

The KEY substantive lemma reducing the kernel-containment to Lemma 2.5. For tprods of a, b with an ι X * ι Y insert: the swap of X and Y corresponds to a transposition of two adjacent positions in the concatenated tuple, which circTMultilinear_symm makes invariant.

§4: circTTensor respects SymRel (consequence of Lemma 2.5)

The substantive content: circTTensor T (ι(x) * ι(y)) = circTTensor T (ι(y) * ι(x)), which reduces to circTMultilinear T 2 (x, y) = circTMultilinear T 2 (y, x) via circTMultilinear_symm (Lemma 2.5).

theorem PreLie.OudomGuinCircConstruct.circTTensor_symRel {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) {a b : TensorAlgebra R L} (h : TensorAlgebra.SymRel R L a b) : (circTTensor T) a = (circTTensor T) b

circTTensor T respects the symmetric-algebra relation SymRel.

§5: Lift to SymmetricAlgebra via Submodule.liftQ

Use Submodule.liftQ after expressing SymmetricAlgebra R L as TensorAlgebra R L ⧸ (ker algHom) via LinearMap.quotKerEquivOfSurjective (algHom is surjective by RingQuot.mkAlgHom_surjective).

The kernel-containment ker algHom ≤ ker (circTTensor T) is the substantive content. Reduces to: for any r, c ∈ TensorAlgebra R L and X, Y ∈ L,

circTTensor T (r * (ι X * ι Y) * c) = circTTensor T (r * (ι Y * ι X) * c),

which follows from the FULL symmetric-group action on circTMultilinear T n (Lemma 2.5 across all positions, not just adjacent) applied to the concatenated tuple [r's positions, X, Y, c's positions].

noncomputable def PreLie.OudomGuinCircConstruct.algHomL {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] : TensorAlgebra R L →ₗ[R] SymmetricAlgebra R L

algHom (the quotient map) as a LinearMap.

Equations

• PreLie.OudomGuinCircConstruct.algHomL = (SymmetricAlgebra.algHom R L).toLinearMap

theorem PreLie.OudomGuinCircConstruct.algHomL_surjective {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] : Function.Surjective ⇑algHomL

§5.A: Helper — linear maps from TensorAlgebra agree iff they agree on tprods

Bilinear extension lemma: two linear maps TA → L that agree on TensorAlgebra.tprod R L n a for every n, a are equal. The proof transfers through TensorAlgebra.equivDirectSum (algebra equivalence to ⨁ⁿ ⨂ⁿ L), then uses DirectSum.linearMap_ext (per-summand check) and PiTensorProduct.ext (per-tprod check) — both @[ext] lemmas in mathlib.

theorem PreLie.OudomGuinCircConstruct.TA_linearMap_ext_tprod {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] {N : Type} [AddCommMonoid N] [Module R N] {f g : TensorAlgebra R L →ₗ[R] N} (h : ∀ (n : ℕ) (a : Fin n → L), f ((TensorAlgebra.tprod R L n) a) = g ((TensorAlgebra.tprod R L n) a)) : f = g

§5.B: Bilinear extension of circTTensor_swap_tprod

circTTensor T (r * (ι X * ι Y) * d) = circTTensor T (r * (ι Y * ι X) * d) for all r, d ∈ TensorAlgebra R L. Proven by bilinear extension from the tprod case (circTTensor_swap_tprod) via two applications of TA_linearMap_ext_tprod.

§5.C: Kernel containment via Rel/EqvGen induction

ker algHomL ≤ ker (circTTensor T). Proof: algHomL z = 0 iff z is in the same Quot (Rel SymRel)-class as 0. Via Rel induction with a strong motive (∀ r d, circTTensor T (r * z₁ * d) = circTTensor T (r * z₂ * d)), the algebraic closure under add_left, mul_left, mul_right is preserved, and the base case is circTTensor_swap_general.

noncomputable def PreLie.OudomGuinCircConstruct.circByT_total {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : SymmetricAlgebra R L →ₗ[R] L

The per-T OG operation, on SymmetricAlgebra R L. Lands in L.

Built via Submodule.liftQ + LinearMap.quotKerEquivOfSurjective applied to the surjective algHom : TensorAlgebra → SymmetricAlgebra.

Equations

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

§6: T-linearity (Q1b Step 2.1)

Each of circTMultilinear, circTTensor, circByT_total is linear in its T : L argument. Proven by descent: induction at the multilinear level, then transferred through PiTensorProduct.lift, DirectSum.toModule, equivDirectSum, and the Submodule.liftQ descent.

The final output circByT_totalLM : L →ₗ[R] SymmetricAlgebra R L →ₗ[R] L is the input to SymmetricAlgebra.lift (Q1b Step 2.2).

theorem PreLie.OudomGuinCircConstruct.circByT_total_comp_algHomL {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : circByT_total T ∘ₗ algHomL = circTTensor T

Key characterization: circByT_total T agrees with circTTensor T when precomposed with algHomL.

theorem PreLie.OudomGuinCircConstruct.circByT_total_T_add {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T₁ T₂ : L) : circByT_total (T₁ + T₂) = circByT_total T₁ + circByT_total T₂

circByT_total is additive in T. Via the algHomL characterization + surjectivity.

theorem PreLie.OudomGuinCircConstruct.circByT_total_T_smul {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (r : R) (T : L) : circByT_total (r • T) = r • circByT_total T

circByT_total is R-homogeneous in T.

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

circByT_total as a linear map in T. Input to SymmetricAlgebra.lift (Q1b Step 2.2).

Equations

• PreLie.OudomGuinCircConstruct.circByT_totalLM = { toFun := PreLie.OudomGuinCircConstruct.circByT_total, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PreLie.OudomGuinCircConstruct.circByT_totalLM_apply {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) (B : SymmetricAlgebra R L) : (circByT_totalLM T) B = (circByT_total T) B

§6.A: Base-case evaluations of circByT_total

For Prop 2.7 (i) / circ_one_right (Q1b Step 3.1): need circByT_total T 1 = T. Traces through the construction chain circByT_total → circTTensor → circTGraded → circTPi → circTMultilinear to the degree-0 base case circTMultilinear T 0 = T.

theorem PreLie.OudomGuinCircConstruct.circTTensor_one {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : (circTTensor T) 1 = T

circTTensor T 1 = T. Base case via DirectSum.one_def + TensorPower.gOne_def.

theorem PreLie.OudomGuinCircConstruct.circByT_total_one {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T : L) : (circByT_total T) 1 = T

circByT_total T 1 = T. The T ○ 1 = T base case (OG Def 2.4 base). Via circByT_total_comp_algHomL + algHomL 1 = 1 + circTTensor_one.

theorem PreLie.OudomGuinCircConstruct.circByT_total_ι {R : Type} [CommRing R] {L : Type} [RightPreLieRing L] [RightPreLieAlgebra R L] (T X : L) : (circByT_total T) ((SymmetricAlgebra.ι R L) X) = T * X

circByT_total T (ι X) = T * X. The degree-1 case (T ○ X = T · X in the pre-Lie product on L).