Lie algebras of Hahn series with Lie algebra coefficients

For a Lie ring L and an ordered cancellative monoid Γ, the Hahn series HahnModule Γ R L with coefficients in L form a Lie ring under the coefficient convolution ⁅x, y⁆_c = ∑_{a + b = c} ⁅x_a, y_b⁆. Each sum is finite, because the supports are partially well-ordered, and the support of the bracket lies in the sum of the supports. For Γ = ℤ and a Lie algebra L over a field K, this is the formal loop algebra L((t)).

If L is a Lie algebra over a commutative ring R, the bracket is bilinear for the coefficientwise action of R, and also for the convolution action of the Hahn series HahnSeries Γ R, so HahnModule Γ R L is a Lie algebra over both. On monomials, ⁅single a x, single b y⁆ = single (a + b) ⁅x, y⁆.

The construction is functorial in L: a morphism f : L → L' of Lie algebras over R, applied to every coefficient, is a morphism of Lie algebras HahnModule Γ R L → HahnModule Γ R L' over HahnSeries Γ R, and isomorphisms of Lie algebras induce isomorphisms. This rests on the naturality of the coefficientwise extension of biadditive maps (HahnModule.convolutionAddMonoidHom_map_map, HahnModule.map_convolutionAddMonoidHom).

Main definitions and results

• HahnModule.instBracket: the coefficient convolution bracket, the coefficientwise extension HahnModule.convolutionAddMonoidHom of the bracket of L.
• HahnModule.of_symm_lie: the bracket is the coefficientwise extension of the bracket of L.
• HahnModule.coeff_lie: the coefficient formula for the bracket.
• HahnModule.support_lie_subset: the support of a bracket lies in the sum of the supports.
• HahnModule.orderTop_add_le_lie: over a linearly ordered Γ, the order of a bracket is at least the sum of the orders.
• HahnModule.instLieRing: the Lie ring of L-valued Hahn series.
• HahnModule.instLieAlgebra, HahnModule.instLieAlgebraHahnSeries: the Lie algebra structures over R and over HahnSeries Γ R.
• HahnModule.single_lie_single: the bracket of two monomials.
• LieHom.hahnModuleMap Γ f: the morphism of Lie algebras of Hahn series induced by f, with coefficients LieHom.coeff_hahnModuleMap, compatible with identities and composition (LieHom.hahnModuleMap_id, LieHom.hahnModuleMap_comp) and injective when f is (LieHom.hahnModuleMap_injective).
• LieEquiv.hahnModuleCongr Γ e: the isomorphism of Lie algebras of Hahn series induced by an isomorphism e.

References

• E. Frenkel, Langlands Correspondence for Loop Groups, §1.2.

The proof of the Leibniz rule reindexes double sums over antidiagonals, following the proof of HahnSeries.mul_assoc in Mathlib's Mathlib/RingTheory/HahnSeries/Multiplication.lean.

@[instance_reducible]

noncomputable instance HahnModule.instBracket {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] : Bracket (HahnModule Γ R L) (HahnModule Γ R L)

The coefficient convolution bracket ⁅x, y⁆_c = ∑_{a + b = c} ⁅x_a, y_b⁆ of Hahn series with coefficients in a Lie ring: the coefficientwise extension convolutionAddMonoidHom of the biadditive bracket of L.

theorem HahnModule.of_symm_lie {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] (x y : HahnModule Γ R L) : (of R).symm ⁅x, y⁆ = ((convolutionAddMonoidHom Γ R (LieRingModule.toEnd L L)) x) y

Read through HahnModule.of, the bracket is the coefficientwise extension convolutionAddMonoidHom of the bracket of L.

theorem HahnModule.coeff_lie {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] (x y : HahnModule Γ R L) (c : Γ) : ((of R).symm ⁅x, y⁆).coeff c = ∑ ij ∈ Finset.antidiagonal ⋯ ⋯ c, ⁅((of R).symm x).coeff ij.1, ((of R).symm y).coeff ij.2⁆

The coefficient formula ⁅x, y⁆_c = ∑_{a + b = c} ⁅x_a, y_b⁆.

theorem HahnModule.coeff_lie_left' {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] {x y : HahnModule Γ R L} {c : Γ} {s : Set Γ} (hs : s.IsPWO) (hxs : ((of R).symm x).support ⊆ s) : ((of R).symm ⁅x, y⁆).coeff c = ∑ ij ∈ Finset.antidiagonal hs ⋯ c, ⁅((of R).symm x).coeff ij.1, ((of R).symm y).coeff ij.2⁆

The coefficients of a bracket may be computed over any partially well-ordered set containing the support of the first argument.

theorem HahnModule.coeff_lie_right' {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] {x y : HahnModule Γ R L} {c : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) : ((of R).symm ⁅x, y⁆).coeff c = ∑ ij ∈ Finset.antidiagonal ⋯ hs c, ⁅((of R).symm x).coeff ij.1, ((of R).symm y).coeff ij.2⁆

The coefficients of a bracket may be computed over any partially well-ordered set containing the support of the second argument.

theorem HahnModule.support_lie_subset {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] (x y : HahnModule Γ R L) : ((of R).symm ⁅x, y⁆).support ⊆ ((of R).symm x).support + ((of R).symm y).support

The support of a bracket lies in the sum of the supports.

@[simp]

theorem HahnModule.single_lie_single {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] (a b : Γ) (x y : L) : ⁅(of R) ((HahnSeries.single a) x), (of R) ((HahnSeries.single b) y)⁆ = (of R) ((HahnSeries.single (a + b)) ⁅x, y⁆)

The bracket of two monomials: ⁅x t ^ a, y t ^ b⁆ = ⁅x, y⁆ t ^ (a + b).

@[instance_reducible]

noncomputable instance HahnModule.instLieRing {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [SMul R L] [LieRing L] : LieRing (HahnModule Γ R L)

Hahn series with coefficients in a Lie ring form a Lie ring under the convolution bracket.

theorem HahnModule.orderTop_add_le_lie {R : Type u_2} {L : Type u_3} [SMul R L] [LieRing L] {Γ : Type u_4} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] (x y : HahnModule Γ R L) : ((of R).symm x).orderTop + ((of R).symm y).orderTop ≤ ((of R).symm ⁅x, y⁆).orderTop

Over a linearly ordered Γ, the order of a bracket is at least the sum of the orders.

@[instance_reducible]

instance HahnModule.instLieAlgebra {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra R (HahnModule Γ R L)

The convolution bracket is bilinear for the coefficientwise action of R.

@[instance_reducible]

noncomputable instance HahnModule.instLieAlgebraHahnSeries {Γ : Type u_1} {R : Type u_2} {L : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] : LieAlgebra (HahnSeries Γ R) (HahnModule Γ R L)

The convolution bracket is bilinear for the convolution action of the Hahn series HahnSeries Γ R. For Γ = ℤ this makes the formal loop algebra L((t)) a Lie algebra over the Laurent series R((t)).

Functoriality in the coefficient Lie algebra

def LieHom.hahnModuleMap (Γ : Type u_1) {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') : HahnModule Γ R L →ₗ⁅HahnSeries Γ R⁆ HahnModule Γ R L'

A morphism f : L → L' of Lie algebras over R induces, coefficient by coefficient, a morphism of Lie algebras HahnModule Γ R L → HahnModule Γ R L' over HahnSeries Γ R, sending ∑ xₐ tᵃ to ∑ f (xₐ) tᵃ. For Γ = ℤ this is the functoriality of the formal loop algebra L((t)) in L.

@[simp]

theorem LieHom.of_symm_hahnModuleMap {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (x : HahnModule Γ R L) : (HahnModule.of R).symm ((hahnModuleMap Γ f) x) = ((HahnModule.of R).symm x).map f

Reading f.hahnModuleMap Γ x through HahnModule.of applies f to every coefficient.

theorem LieHom.coeff_hahnModuleMap {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (x : HahnModule Γ R L) (a : Γ) : ((HahnModule.of R).symm ((hahnModuleMap Γ f) x)).coeff a = f (((HahnModule.of R).symm x).coeff a)

The coefficients of f.hahnModuleMap Γ x are the images under f of those of x.

theorem LieHom.hahnModuleMap_of {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (x : HahnSeries Γ L) : (hahnModuleMap Γ f) ((HahnModule.of R) x) = (HahnModule.of R) (x.map f)

On the series attached to x, the induced map applies f to every coefficient.

@[simp]

theorem LieHom.hahnModuleMap_single {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (a : Γ) (x : L) : (hahnModuleMap Γ f) ((HahnModule.of R) ((HahnSeries.single a) x)) = (HahnModule.of R) ((HahnSeries.single a) (f x))

The monomial x tᵃ goes to the monomial f (x) tᵃ.

@[simp]

theorem LieHom.hahnModuleMap_id (Γ : Type u_1) (R : Type u_2) (L : Type u_3) [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] : hahnModuleMap Γ id = id

The identity of L induces the identity of HahnModule Γ R L.

@[simp]

theorem LieHom.hahnModuleMap_comp {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} {L'' : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieRing L''] [LieAlgebra R L''] (g : L' →ₗ⁅R⁆ L'') (f : L →ₗ⁅R⁆ L') : hahnModuleMap Γ (g.comp f) = (hahnModuleMap Γ g).comp (hahnModuleMap Γ f)

The construction is compatible with composition of morphisms.

theorem LieHom.hahnModuleMap_injective {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} (hf : Function.Injective ⇑f) : Function.Injective ⇑(hahnModuleMap Γ f)

An injective morphism of Lie algebras induces an injective morphism of Hahn series.

def LieEquiv.hahnModuleCongr (Γ : Type u_1) {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') : HahnModule Γ R L ≃ₗ⁅HahnSeries Γ R⁆ HahnModule Γ R L'

An isomorphism e : L ≃ L' of Lie algebras over R induces, coefficient by coefficient, an isomorphism of Lie algebras HahnModule Γ R L ≃ HahnModule Γ R L' over HahnSeries Γ R.

@[simp]

theorem LieEquiv.coe_hahnModuleCongr {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') : (hahnModuleCongr Γ e).toLieHom = LieHom.hahnModuleMap Γ e.toLieHom

The isomorphism of Hahn series is the morphism induced by the underlying morphism.

@[simp]

theorem LieEquiv.of_symm_hahnModuleCongr {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') (x : HahnModule Γ R L) : (HahnModule.of R).symm ((hahnModuleCongr Γ e) x) = ((HahnModule.of R).symm x).map e

Reading e.hahnModuleCongr Γ x through HahnModule.of applies e to every coefficient.

@[simp]

theorem LieEquiv.hahnModuleCongr_symm {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (e : L ≃ₗ⁅R⁆ L') : (hahnModuleCongr Γ e).symm = hahnModuleCongr Γ e.symm

The inverse of the induced isomorphism is induced by the inverse isomorphism.

@[simp]

theorem LieEquiv.hahnModuleCongr_refl (Γ : Type u_1) (R : Type u_2) (L : Type u_3) [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] : hahnModuleCongr Γ refl = refl

The identity isomorphism of L induces the identity isomorphism of HahnModule Γ R L.

@[simp]

theorem LieEquiv.hahnModuleCongr_trans {Γ : Type u_1} {R : Type u_2} {L : Type u_3} {L' : Type u_4} {L'' : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] [LieRing L''] [LieAlgebra R L''] (e : L ≃ₗ⁅R⁆ L') (e' : L' ≃ₗ⁅R⁆ L'') : hahnModuleCongr Γ (e.trans e') = (hahnModuleCongr Γ e).trans (hahnModuleCongr Γ e')

The construction is compatible with composition of isomorphisms.