The order topology on formal currents

Formal currents R⸨X⸩ ⊗[R] L carry the linear topology in which the order submodules orderSubmodule R L N, the currents of order at least N, form a basis of neighbourhoods of zero. The coefficient ring R and the coefficient module L carry no topology: this is the X-adic topology for discrete coefficients. The order submodules are defined without a choice of basis, so neither is the topology.

This topology makes the formal currents a nonarchimedean topological additive group whose topology is R-linear, and multiplication by a fixed Laurent series is continuous. For a Lie algebra L the bracket is jointly continuous, because brackets of currents of orders at least M and N have order at least M + N and every current has a finite lower order. Truncations of a current converge to it, so polynomial currents are dense.

When L is a free R-module, the topology is Hausdorff. When L is finitely generated, it is complete: a Cauchy sequence has eventually constant coefficients below every order and a common lower order, and every such coefficient family is the coefficient family of a formal current. The finiteness assumption cannot be dropped: for infinitely many basis vectors bᵢ, the partial sums of ∑ᵢ Xⁱ ⊗ bᵢ form a Cauchy sequence without a limit in the tensor product.

Main results

• TauCeti.CurrentAlgebra.hasBasis_nhds_zero: the order submodules form a basis of neighbourhoods of zero.
• TauCeti.CurrentAlgebra.tendsto_nhds_iff: convergence of currents in terms of orders.
• TauCeti.CurrentAlgebra.continuous_lie: the bracket of formal currents is continuous.
• TauCeti.CurrentAlgebra.instT2Space, TauCeti.CurrentAlgebra.instCompleteSpace: the topology is Hausdorff over a free coefficient module, and complete over a finitely generated one.
• TauCeti.CurrentAlgebra.denseRange_ofLoop: polynomial currents are dense.

References

• E. Frenkel, Langlands Correspondence for Loop Groups, §1.3, for the topology of the formal loop algebra g((t)).

@[instance_reducible]

noncomputable def TauCeti.CurrentAlgebra.orderFilterBasis (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : AddGroupFilterBasis (currentAlgebra R L)

The order submodules, as a filter basis of the additive group of formal currents.

@[instance_reducible]

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

Formal currents carry the linear topology in which the order submodules form a basis of neighbourhoods of zero.

instance TauCeti.CurrentAlgebra.instIsTopologicalAddGroupCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : IsTopologicalAddGroup (currentAlgebra R L)

theorem TauCeti.CurrentAlgebra.hasBasis_nhds_zero (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : (nhds 0).HasBasis (fun (x : ℤ) => True) fun (N : ℤ) => ↑(orderSubmodule R L N)

The order submodules form a basis of neighbourhoods of zero.

theorem TauCeti.CurrentAlgebra.hasBasis_nhds (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (u : currentAlgebra R L) : (nhds u).HasBasis (fun (x : ℤ) => True) fun (N : ℤ) => {v : currentAlgebra R L | v - u ∈ orderSubmodule R L N}

The translates of the order submodules form a basis of neighbourhoods of a current.

theorem TauCeti.CurrentAlgebra.tendsto_nhds_iff {R : Type u_1} {L : Type u_2} [CommRing R] [AddCommGroup L] [Module R L] {ι : Type u_3} {l : Filter ι} {f : ι → currentAlgebra R L} {u : currentAlgebra R L} : Filter.Tendsto f l (nhds u) ↔ ∀ (N : ℤ), ∀ᶠ (i : ι) in l, f i - u ∈ orderSubmodule R L N

A family of currents converges to u exactly when, for every order N, its differences with u eventually have order at least N.

theorem TauCeti.CurrentAlgebra.orderSubmodule_mem_nhds_zero (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : ↑(orderSubmodule R L N) ∈ nhds 0

Every order submodule is a neighbourhood of zero.

theorem TauCeti.CurrentAlgebra.isOpen_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : IsOpen ↑(orderSubmodule R L N)

Every order submodule is open.

theorem TauCeti.CurrentAlgebra.isClosed_orderSubmodule (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] (N : ℤ) : IsClosed ↑(orderSubmodule R L N)

Every order submodule is closed.

instance TauCeti.CurrentAlgebra.instIsLinearTopologyCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : IsLinearTopology R (currentAlgebra R L)

The order topology on formal currents is linear over the coefficient ring.

instance TauCeti.CurrentAlgebra.instNonarchimedeanAddGroupCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : NonarchimedeanAddGroup (currentAlgebra R L)

Formal currents form a nonarchimedean additive group: the order submodules are open subgroups.

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

Multiplication by a fixed Laurent series is continuous on formal currents.

instance TauCeti.CurrentAlgebra.instContinuousConstSMulCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : ContinuousConstSMul R (currentAlgebra R L)

Multiplication by a fixed coefficient is continuous on formal currents.

instance TauCeti.CurrentAlgebra.instT2Space (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] [Module.Free R L] : T2Space (currentAlgebra R L)

The order topology is Hausdorff over a free coefficient module.

@[instance_reducible]

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

Formal currents carry the uniform structure of their topological additive group.

instance TauCeti.CurrentAlgebra.instIsUniformAddGroupCurrentAlgebra (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] : IsUniformAddGroup (currentAlgebra R L)

instance TauCeti.CurrentAlgebra.instCompleteSpace (R : Type u_1) (L : Type u_2) [CommRing R] [AddCommGroup L] [Module R L] [Module.Finite R L] : CompleteSpace (currentAlgebra R L)

The order topology is complete over a finitely generated coefficient module.

theorem TauCeti.CurrentAlgebra.continuous_lie (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Continuous fun (p : currentAlgebra R L × currentAlgebra R L) => ⁅p.1, p.2⁆

The bracket of formal currents is jointly continuous.

theorem TauCeti.CurrentAlgebra.tendsto_ofLoop_trunc (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] (u : currentAlgebra R L) : Filter.Tendsto (fun (N : ℤ) => (ofLoop R L) ((trunc R L N) u)) Filter.atTop (nhds u)

The truncations of a formal current converge to it as the cutoff grows.

theorem TauCeti.CurrentAlgebra.denseRange_ofLoop (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : DenseRange ⇑(ofLoop R L)

Polynomial currents are dense in formal currents.