Polynomial loops as Hahn series

The polynomial loop algebra loopAlgebra R Γ L = R[Γ] ⊗[R] L of a Lie algebra L over a commutative ring R embeds into the Lie algebra HahnModule Γ R L of L-valued Hahn series, sending t ^ a ⊗ x to the monomial x t ^ a. For Γ = ℤ this is the inclusion of the polynomial loop algebra L[t, t⁻¹] into the formal loop algebra L((t)).

Main definitions and results

• LieAlgebra.LoopAlgebra.toHahnModule: the embedding, as a morphism of Lie algebras over R.
• LieAlgebra.LoopAlgebra.coeff_toHahnModule: its coefficients are those of LieAlgebra.LoopAlgebra.toFinsupp.
• LieAlgebra.LoopAlgebra.toHahnModule_single_tmul: t ^ a ⊗ x goes to the monomial x t ^ a.
• LieAlgebra.LoopAlgebra.toHahnModule_injective: the embedding is injective.
• LieHom.hahnModuleMap_toHahnModule: the embedding is natural in the Lie algebra L.

noncomputable def LieAlgebra.LoopAlgebra.toHahnModule (R : Type u_1) (Γ : Type u_2) (L : Type u_3) [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L] [LieAlgebra R L] : loopAlgebra R Γ L →ₗ⁅R⁆ HahnModule Γ R L

The embedding of polynomial loops into L-valued Hahn series, sending t ^ a ⊗ x to the monomial x t ^ a.

@[simp]

theorem LieAlgebra.LoopAlgebra.coeff_toHahnModule {R : Type u_1} {Γ : Type u_2} {L : Type u_3} [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L] [LieAlgebra R L] (p : loopAlgebra R Γ L) (a : Γ) : ((HahnModule.of R).symm ((toHahnModule R Γ L) p)).coeff a = ((toFinsupp R Γ L) p) a

The coefficients of the image of a polynomial loop are its coefficients.

@[simp]

theorem LieAlgebra.LoopAlgebra.toHahnModule_single_tmul {R : Type u_1} {Γ : Type u_2} {L : Type u_3} [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L] [LieAlgebra R L] (a : Γ) (x : L) : (toHahnModule R Γ L) (AddMonoidAlgebra.single a 1 ⊗ₜ[R] x) = (HahnModule.of R) ((HahnSeries.single a) x)

The loop t ^ a ⊗ x is sent to the monomial x t ^ a.

theorem LieAlgebra.LoopAlgebra.toHahnModule_injective {R : Type u_1} {Γ : Type u_2} {L : Type u_3} [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L] [LieAlgebra R L] : Function.Injective ⇑(toHahnModule R Γ L)

Distinct polynomial loops have distinct images in the Hahn series.

theorem LieHom.hahnModuleMap_toHahnModule {R : Type u_1} {Γ : Type u_2} {L : Type u_3} [CommRing R] [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [LieRing L] [LieAlgebra R L] {L' : Type u_4} [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (p : LieAlgebra.loopAlgebra R Γ L) : (hahnModuleMap Γ f) ((LieAlgebra.LoopAlgebra.toHahnModule R Γ L) p) = (LieAlgebra.LoopAlgebra.toHahnModule R Γ L') ((LieAlgebra.ExtendScalars.map (AlgHom.id R (AddMonoidAlgebra R Γ)) f) p)

The embedding is natural in the Lie algebra: applying a morphism f : L → L' to the coefficients of the image of a polynomial loop gives the image of the loop transformed by f.