Formal currents and their order filtration

Formal currents in a Lie algebra L over R are the scalar extension R⸨X⸩ ⊗[R] L, with the coefficientwise scalar action and Mathlib's scalar-extension bracket. The order submodule orderSubmodule R L N is spanned by tensors whose scalar series vanish below N. The bracket of currents of orders at least M and N has order at least M + N; conversely, when L is perfect every current of order at least M + N is a sum of such brackets. Hence a linear map killing these brackets kills every current of order at least M + N, and formal currents of a perfect Lie algebra are perfect. Every current has a finite lower bound. The coefficient, order and truncation API also applies to any coefficient module, without a Lie structure.

When L is free, coefficients determine a current. For any coefficient module, membership in an order submodule is equivalent to vanishing of all lower coefficients. These descriptions make the filtration independent of a choice of basis. No finite-dimensionality is needed for these statements: in infinite dimension, the tensor product still only contains finite sums of scalar series times vectors. It need not contain every L-valued Laurent series. When L is finite, free or not, every coefficient family vanishing below some order is the coefficient family of a current.

Polynomial currents embed through LieAlgebra.ExtendScalars.map and the existing Laurent-polynomial inclusion. Their coefficients agree with Mathlib's LieAlgebra.LoopAlgebra.toFinsupp. Truncation below N produces a polynomial current whose difference from the original lies in orderSubmodule R L N, and it kills orderSubmodule R L N. A linear map on polynomial currents killing all modes t^n ⊗ x with n ≥ N therefore extends to formal currents by composing with truncation below N.

The polynomial currents of order below N, spanned by the modes t^m ⊗ x with m < N, form the submodule truncSubmodule R L N. It is the range of truncation below N and a complement of orderSubmodule R L N, over every commutative ring. The bracket of polynomial currents of orders below M and N has order below M + N - 1; for N = 0 this makes the negative currents t⁻¹ L[t⁻¹] a Lie subalgebra.

References

• V. Kac, Infinite-Dimensional Lie Algebras, Chapter 7 (current algebras).

The constructions use Mathlib's LieAlgebra.ExtendScalars and TensorProduct.equivFinsuppOfBasisRight; no additional Lie structure is imposed.

@[reducible, inline]

abbrev TauCeti.currentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : Type (max u_1 u_2)

Formal currents in a module; for a Lie algebra, equipped with the scalar-extension bracket.

@[instance_reducible]

noncomputable instance TauCeti.CurrentAlgebra.instModuleLaurentSeriesCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : Module (LaurentSeries R) (currentAlgebra R L)

Formal currents are a module over Laurent series, with the coefficientwise scalar action.

@[instance_reducible]

noncomputable instance TauCeti.CurrentAlgebra.instLieRingCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieRing (currentAlgebra R L)

The scalar-extension Lie ring, using the coefficientwise scalar action on series.

@[instance_reducible]

noncomputable instance TauCeti.CurrentAlgebra.instLieAlgebraCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra R (currentAlgebra R L)

Formal currents are a Lie algebra over the coefficient ring.

@[instance_reducible]

noncomputable instance TauCeti.CurrentAlgebra.instLieAlgebraLaurentSeriesCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra (LaurentSeries R) (currentAlgebra R L)

Formal currents are also a Lie algebra over the Laurent-series ring.

def TauCeti.CurrentAlgebra.coeff (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (n : ℤ) : currentAlgebra R L →ₗ[R] L

The coefficient of a formal current at an integer exponent.

@[simp]

theorem TauCeti.CurrentAlgebra.coeff_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (n : ℤ) (f : LaurentSeries R) (x : L) : (coeff R L n) (f ⊗ₜ[R] x) = f.coeff n • x

@[simp]

theorem HahnModule.coeff_tensorProductToHahnModule {R : Type u_1} [CommRing R] {V : Type u_3} [AddCommGroup V] [Module R V] (u : TauCeti.currentAlgebra R V) (n : ℤ) : ((of R).symm ((tensorProductToHahnModule ℤ R V) u)).coeff n = (TauCeti.CurrentAlgebra.coeff R V n) u

On formal currents, the comparison with module-valued Laurent series preserves coefficients.

theorem TauCeti.CurrentAlgebra.ext (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] [Module.Free R L] {u v : currentAlgebra R L} (h : ∀ (n : ℤ), (coeff R L n) u = (coeff R L n) v) : u = v

Coefficients determine a formal current over a free coefficient module.

theorem TauCeti.CurrentAlgebra.ext_iff {R : Type u_1} {L : Type u_2} [CommRing R] [AddCommGroup L] [Module R L] [Module.Free R L] {u v : currentAlgebra R L} : u = v ↔ ∀ (n : ℤ), (coeff R L n) u = (coeff R L n) v

theorem TauCeti.CurrentAlgebra.exists_forall_coeff_eq (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] [Module.Finite R L] (c : ℤ → L) {a : ℤ} (hc : ∀ n < a, c n = 0) : ∃ (u : currentAlgebra R L), ∀ (n : ℤ), (coeff R L n) u = c n

Over a finite coefficient module, every coefficient family vanishing below some order is the coefficient family of a formal current. Freeness is not needed.

def TauCeti.CurrentAlgebra.orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : Submodule R (currentAlgebra R L)

Currents of order at least N, expressed without choosing a basis.

theorem TauCeti.CurrentAlgebra.orderSubmodule_def (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : orderSubmodule R L N = Submodule.span R {u : TensorProduct R (LaurentSeries R) L | ∃ (f : LaurentSeries R) (x : L), ↑N ≤ HahnSeries.orderTop f ∧ u = f ⊗ₜ[R] x}

The order submodule is spanned by the tensors whose scalar series have order at least N.

theorem TauCeti.CurrentAlgebra.tmul_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) {f : LaurentSeries R} (hf : ↑N ≤ HahnSeries.orderTop f) (x : L) : f ⊗ₜ[R] x ∈ orderSubmodule R L N

A tensor has order at least the order of its scalar series.

theorem TauCeti.CurrentAlgebra.single_tmul_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {N m : ℤ} (h : N ≤ m) (r : R) (x : L) : (HahnSeries.single m) r ⊗ₜ[R] x ∈ orderSubmodule R L N

A mode r tᵐ ⊗ x has order at least N whenever N ≤ m.

theorem TauCeti.CurrentAlgebra.coeff_eq_zero_of_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {N n : ℤ} {u : currentAlgebra R L} (hu : u ∈ orderSubmodule R L N) (hn : n < N) : (coeff R L n) u = 0

A current of order at least N has zero coefficients below N.

theorem TauCeti.CurrentAlgebra.orderSubmodule_antitone (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : Antitone (orderSubmodule R L)

Increasing the required order makes the order submodule smaller.

@[simp]

theorem TauCeti.CurrentAlgebra.iInf_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] [Module.Free R L] : ⨅ (N : ℤ), orderSubmodule R L N = ⊥

The order filtration is separated over a free coefficient module.

theorem TauCeti.CurrentAlgebra.exists_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (u : currentAlgebra R L) : ∃ (N : ℤ), u ∈ orderSubmodule R L N

Every formal current has a finite lower order, also in infinite dimension.

theorem TauCeti.CurrentAlgebra.smul_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {M N : ℤ} {f : LaurentSeries R} {u : currentAlgebra R L} (hf : ↑M ≤ HahnSeries.orderTop f) (hu : u ∈ orderSubmodule R L N) : f • u ∈ orderSubmodule R L (M + N)

A scalar series of order at least M times a current of order at least N has order at least M + N.

noncomputable def TauCeti.CurrentAlgebra.trunc (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : currentAlgebra R L →ₗ[R] TensorProduct R (LaurentPolynomial R) L

Truncate a formal current strictly below an integer cutoff, producing a polynomial current.

@[simp]

theorem TauCeti.CurrentAlgebra.trunc_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) (f : LaurentSeries R) (x : L) : (trunc R L N) (f ⊗ₜ[R] x) = (LaurentSeries.trunc N) f ⊗ₜ[R] x

@[simp]

theorem TauCeti.CurrentAlgebra.equivFinsuppOfBasisLeft_trunc (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N n : ℤ) (u : currentAlgebra R L) : ((TensorProduct.equivFinsuppOfBasisLeft (AddMonoidAlgebra.basis ℤ R)) ((trunc R L N) u)) n = if n < N then (coeff R L n) u else 0

Truncation retains exactly the coefficients strictly below its cutoff, in the standard monomial coordinates on polynomial currents over any coefficient module.

theorem TauCeti.CurrentAlgebra.rTensor_toLaurentSeries_trunc_sub_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) (u : currentAlgebra R L) : (LinearMap.rTensor L (IsScalarTower.toAlgHom R (LaurentPolynomial R) (LaurentSeries R)).toLinearMap) ((trunc R L N) u) - u ∈ orderSubmodule R L N

Including a polynomial truncation back into formal currents changes the current only in orders at least the cutoff, for any coefficient module.

theorem TauCeti.CurrentAlgebra.mem_orderSubmodule_iff (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) (u : currentAlgebra R L) : u ∈ orderSubmodule R L N ↔ ∀ n < N, (coeff R L n) u = 0

Vanishing of lower coefficients characterizes order for any coefficient module.

def TauCeti.CurrentAlgebra.truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : Submodule R (currentAlgebra R L)

Polynomial currents of order below N, spanned by the modes t^m ⊗ x with m < N. For N = 0 these are the negative currents t⁻¹ L[t⁻¹].

theorem TauCeti.CurrentAlgebra.truncSubmodule_def (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : truncSubmodule R L N = Submodule.span R {u : TensorProduct R (HahnSeries ℤ R) L | ∃ m < N, ∃ (x : L), u = (HahnSeries.single m) 1 ⊗ₜ[R] x}

The polynomial currents of order below N are spanned by the modes t^m ⊗ x with m < N.

theorem TauCeti.CurrentAlgebra.single_tmul_mem_truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] {m N : ℤ} (h : m < N) (r : R) (x : L) : (HahnSeries.single m) r ⊗ₜ[R] x ∈ truncSubmodule R L N

A monomial current r t^m ⊗ x with m < N has order below N.

theorem TauCeti.CurrentAlgebra.truncSubmodule_mono (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : Monotone (truncSubmodule R L)

Increasing the bound makes the submodule of polynomial currents of order below it larger.

theorem TauCeti.CurrentAlgebra.lie_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {M N : ℤ} {u v : currentAlgebra R L} (hu : u ∈ orderSubmodule R L M) (hv : v ∈ orderSubmodule R L N) : ⁅u, v⁆ ∈ orderSubmodule R L (M + N)

The bracket of currents of orders at least M and N has order at least M + N.

def TauCeti.CurrentAlgebra.orderLieSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : LieSubalgebra R (currentAlgebra R L)

The Lie subalgebra of currents of order at least the nonnegative integer n.

@[simp]

theorem TauCeti.CurrentAlgebra.orderLieSubalgebra_toSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) : (orderLieSubalgebra R L n).toSubmodule = orderSubmodule R L ↑n

The underlying submodule of a_n is the order submodule.

@[simp]

theorem TauCeti.CurrentAlgebra.mem_orderLieSubalgebra (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℕ) (u : currentAlgebra R L) : u ∈ orderLieSubalgebra R L n ↔ u ∈ orderSubmodule R L ↑n

Membership in a_n is the order condition.

theorem TauCeti.CurrentAlgebra.orderLieSubalgebra_antitone (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Antitone (orderLieSubalgebra R L)

The current Lie subalgebras decrease with the order.

theorem TauCeti.CurrentAlgebra.lie_mem_truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {M N : ℤ} {u v : currentAlgebra R L} (hu : u ∈ truncSubmodule R L M) (hv : v ∈ truncSubmodule R L N) : ⁅u, v⁆ ∈ truncSubmodule R L (M + N - 1)

The bracket of polynomial currents of orders below M and N has order below M + N - 1.

theorem TauCeti.CurrentAlgebra.orderSubmodule_add_le_span_lie (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) (M N : ℤ) : orderSubmodule R L (M + N) ≤ Submodule.span R {w : currentAlgebra R L | ∃ u ∈ orderSubmodule R L M, ∃ v ∈ orderSubmodule R L N, ⁅u, v⁆ = w}

Currents of a perfect Lie algebra are sums of brackets of higher-order currents. If L is perfect, every current of order at least M + N is a linear combination of brackets of currents of orders at least M and N.

theorem TauCeti.CurrentAlgebra.orderSubmodule_add_le_ker_of_map_lie_eq_zero (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {P : Type u_3} [AddCommGroup P] [Module R P] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) {M N : ℤ} (F : currentAlgebra R L →ₗ[R] P) (hF : ∀ u ∈ orderSubmodule R L M, ∀ v ∈ orderSubmodule R L N, F ⁅u, v⁆ = 0) : orderSubmodule R L (M + N) ≤ F.ker

A linear map killing brackets of high order kills currents of high order. If L is perfect and a linear map F on currents vanishes on every bracket of currents of orders at least M and N, then F vanishes on all currents of order at least M + N.

theorem TauCeti.CurrentAlgebra.derivedSeries_one_eq_top (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (hL : LieAlgebra.derivedSeries R L 1 = ⊤) : LieAlgebra.derivedSeries R (currentAlgebra R L) 1 = ⊤

Formal currents of a perfect Lie algebra are perfect as a Lie algebra over the base ring: every current is an R-linear combination of brackets of currents. Mathlib's LieAlgebra.derivedSeries_baseChange gives the weaker statement over the Laurent series ring; the statement over R is the one that applies to R-linear cochains.

noncomputable def TauCeti.CurrentAlgebra.ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra.loopAlgebra R ℤ L →ₗ⁅R⁆ currentAlgebra R L

The inclusion of polynomial currents into formal currents.

@[simp]

theorem TauCeti.CurrentAlgebra.ofLoop_tmul (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (p : LaurentPolynomial R) (x : L) : (ofLoop R L) (p ⊗ₜ[R] x) = LaurentPolynomial.toLaurentSeries p ⊗ₜ[R] x

@[simp]

theorem TauCeti.CurrentAlgebra.coeff_ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (n : ℤ) (u : LieAlgebra.loopAlgebra R ℤ L) : (coeff R L n) ((ofLoop R L) u) = ((LieAlgebra.LoopAlgebra.toFinsupp R ℤ L) u) n

The inclusion preserves polynomial-current coefficients.

theorem TauCeti.CurrentAlgebra.ofLoop_injective (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Injective ⇑(ofLoop R L)

Polynomial currents embed in formal currents over every commutative base ring.

@[simp]

theorem TauCeti.CurrentAlgebra.toFinsupp_trunc (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (N n : ℤ) (u : currentAlgebra R L) : ((LieAlgebra.LoopAlgebra.toFinsupp R ℤ L) ((trunc R L N) u)) n = if n < N then (coeff R L n) u else 0

Truncation retains exactly the coefficients strictly below its cutoff.

theorem TauCeti.CurrentAlgebra.ofLoop_trunc_sub_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (N : ℤ) (u : currentAlgebra R L) : (ofLoop R L) ((trunc R L N) u) - u ∈ orderSubmodule R L N

The truncation error has order at least the cutoff, without a freeness assumption.

theorem TauCeti.CurrentAlgebra.ofLoop_trunc_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (P : ℤ) {M : ℤ} {u : currentAlgebra R L} (hu : u ∈ orderSubmodule R L M) : (ofLoop R L) ((trunc R L P) u) ∈ orderSubmodule R L M

Truncating a current preserves every lower order bound, including when the cutoff lies below that bound. No freeness of the coefficient module is needed.

theorem TauCeti.CurrentAlgebra.ofLoop_single_tmul_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (a : ℤ) (x : L) : (ofLoop R L) (AddMonoidAlgebra.single a 1 ⊗ₜ[R] x) ∈ orderSubmodule R L a

The polynomial mode t^a ⊗ x has order at least a.

theorem TauCeti.CurrentAlgebra.trunc_eq_zero_of_mem_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {N : ℤ} {u : currentAlgebra R L} (hu : u ∈ orderSubmodule R L N) : (trunc R L N) u = 0

Truncation below N kills the currents of order at least N.

theorem TauCeti.CurrentAlgebra.ofLoop_trunc_mem_truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (N : ℤ) (u : currentAlgebra R L) : (ofLoop R L) ((trunc R L N) u) ∈ truncSubmodule R L N

Truncation below N lands in the polynomial currents of order below N.

theorem TauCeti.CurrentAlgebra.ofLoop_trunc_of_mem_truncSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {N : ℤ} {u : currentAlgebra R L} (hu : u ∈ truncSubmodule R L N) : (ofLoop R L) ((trunc R L N) u) = u

Truncation below N fixes the polynomial currents of order below N.

theorem TauCeti.CurrentAlgebra.mem_truncSubmodule_iff (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {N : ℤ} {u : currentAlgebra R L} : u ∈ truncSubmodule R L N ↔ (ofLoop R L) ((trunc R L N) u) = u

The polynomial currents of order below N are the range of truncation below N: a current lies in truncSubmodule R L N exactly when truncation below N fixes it.

theorem TauCeti.CurrentAlgebra.isCompl_truncSubmodule_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (N : ℤ) : IsCompl (truncSubmodule R L N) (orderSubmodule R L N)

The polynomial currents of order below N complement the currents of order at least N. Every current is uniquely its truncation below N plus a current of order at least N, over every commutative ring.

theorem TauCeti.CurrentAlgebra.apply_trunc_ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] {V : Type u_3} [AddCommGroup V] [Module R V] {N : ℤ} (g : LieAlgebra.loopAlgebra R ℤ L →ₗ[R] V) (hg : ∀ (n : ℤ), N ≤ n → ∀ (x : L), g (AddMonoidAlgebra.single n 1 ⊗ₜ[R] x) = 0) (p : LieAlgebra.loopAlgebra R ℤ L) : g ((trunc R L N) ((ofLoop R L) p)) = g p

A linear map on polynomial currents which vanishes on all modes t^n ⊗ x with n ≥ N is unchanged by first truncating polynomial currents below N.

theorem TauCeti.CurrentAlgebra.lie_single_neg_one_eq_lie_single_zero {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) : ⁅(HahnSeries.single (-1)) 1 ⊗ₜ[R] x, (HahnSeries.single 1) 1 ⊗ₜ[R] y⁆ = ⁅(HahnSeries.single 0) 1 ⊗ₜ[R] x, (HahnSeries.single 0) 1 ⊗ₜ[R] y⁆

The brackets of X⁻¹ ⊗ x with X ⊗ y and of 1 ⊗ x with 1 ⊗ y agree.