Scalar extension and module-valued Hahn series

The canonical map R⟦Γ⟧ ⊗[R] V → HahnModule Γ R V sends f ⊗ v to the series with coefficients f.coeff g • v, or equivalently to f times the constant series v. For a finite free coefficient module this is an isomorphism over R⟦Γ⟧: expansion in any finite basis of V writes a module-valued series as a finite sum of scalar series times constant basis vectors. The map itself is independent of that basis.

In particular, for a finite-dimensional vector space V over a field K, this identifies K((t)) ⊗[K] V with V((t)) on Mathlib's HahnModule ℤ K V carrier, with its convolution action of scalar Laurent series. This supplies the scalar-extension interpretation of module-valued Laurent series used in residue duality.

In arbitrary dimension the comparison is injective for free coefficients. Over a field its image consists exactly of series whose coefficients lie in a single finite-dimensional subspace. For integer exponents and free coefficients over a commutative ring, it is surjective if and only if the coefficient module is finitely generated (equivalently, finite-dimensional over a field): a series with an independent sequence of coefficients cannot be a finite sum of scalar series times vectors. This distinguishes tensor currents from their coefficientwise completion.

References

• E. Frenkel, Langlands Correspondence for Loop Groups, §1.3.1, for tensor currents and the finite-dimensional comparison.

noncomputable def HahnModule.tensorProductToHahnModule (Γ : Type u_1) (R : Type u_2) (V : Type u_3) [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] : TensorProduct R (HahnSeries Γ R) V →ₗ[HahnSeries Γ R] HahnModule Γ R V

The canonical scalar-extension map to module-valued Hahn series, sending f ⊗ v to f times the constant series v.

@[simp]

theorem HahnModule.tensorProductToHahnModule_tmul {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] (f : HahnSeries Γ R) (v : V) : (tensorProductToHahnModule Γ R V) (f ⊗ₜ[R] v) = f • (of R) ((HahnSeries.single 0) v)

The scalar-extension map on a pure tensor is multiplication by a constant series.

theorem HahnModule.coeff_tensorProductToHahnModule_map {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] {W : Type u_4} [AddCommMonoid W] [Module R W] (ℓ : V →ₗ[R] W) (z : TensorProduct R (HahnSeries Γ R) V) (g : Γ) : ((of R).symm ((tensorProductToHahnModule Γ R W) ((TensorProduct.map LinearMap.id ℓ) z))).coeff g = ℓ (((of R).symm ((tensorProductToHahnModule Γ R V) z)).coeff g)

Scalar extension commutes with linear maps on the coefficient module, coefficient by coefficient. No finiteness assumption is needed for this naturality identity.

theorem HahnModule.sum_map_coord_smul_single {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι R V) (x : HahnModule Γ R V) : ∑ i : ι, ((of R).symm x).map (b.coord i) • (of R) ((HahnSeries.single 0) (b i)) = x

A finite basis expands a module-valued Hahn series into scalar coordinate series times constant basis vectors.

theorem HahnModule.tensorProductToHahnModule_bijective_of_basis {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] {ι : Type u_4} [Finite ι] (b : Module.Basis ι R V) : Function.Bijective ⇑(tensorProductToHahnModule Γ R V)

The scalar-extension map is bijective whenever the coefficient module has a finite basis.

noncomputable def HahnModule.tensorProductEquiv (Γ : Type u_1) (R : Type u_2) (V : Type u_3) [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] [Module.Finite R V] : TensorProduct R (HahnSeries Γ R) V ≃ₗ[HahnSeries Γ R] HahnModule Γ R V

Finite free coefficient modules commute with scalar extension to Hahn series. In particular this is K((t)) ⊗[K] V ≃ V((t)) for finite-dimensional V.

@[simp]

theorem HahnModule.tensorProductEquiv_apply {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] [Module.Finite R V] (z : TensorProduct R (HahnSeries Γ R) V) : (tensorProductEquiv Γ R V) z = (tensorProductToHahnModule Γ R V) z

The equivalence has the canonical scalar-extension map as its forward map.

theorem HahnModule.tensorProductEquiv_symm_apply {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] [Module.Finite R V] {ι : Type u_4} [Fintype ι] (b : Module.Basis ι R V) (x : HahnModule Γ R V) : (tensorProductEquiv Γ R V).symm x = ∑ i : ι, ((of R).symm x).map (b.coord i) ⊗ₜ[R] b i

In any finite basis, the inverse comparison is the sum of the scalar coordinate series tensored with the corresponding basis vectors.

@[simp]

theorem HahnModule.tensorProductEquiv_symm_single {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] [Module.Finite R V] (g : Γ) (v : V) : (tensorProductEquiv Γ R V).symm ((of R) ((HahnSeries.single g) v)) = (HahnSeries.single g) 1 ⊗ₜ[R] v

The inverse comparison sends a vector-valued monomial to a pure tensor.

theorem HahnModule.exists_sum_smul_single_zero {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Finite R V] (x : HahnModule Γ R V) : ∃ (s : Finset V) (a : V → HahnSeries Γ R), ∑ v ∈ s, a v • (of R) ((HahnSeries.single 0) v) = x

Over a finitely generated coefficient module, every module-valued Hahn series is a finite sum of scalar series times constant vectors.

theorem TauCeti.HahnModule.linearMap_ext_smul_single_zero {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Finite R V] {M : Type u_4} [AddCommMonoid M] [Module R M] {f g : HahnModule Γ R V →ₗ[R] M} (h : ∀ (a : HahnSeries Γ R) (v : V), f (a • (HahnModule.of R) ((HahnSeries.single 0) v)) = g (a • (HahnModule.of R) ((HahnSeries.single 0) v))) : f = g

For finitely generated coefficients, linear maps on module-valued Hahn series are determined by scalar series times constant vectors.

theorem HahnModule.coeff_equivFinsuppOfBasisRight {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] {ι : Type u_4} [DecidableEq ι] (b : Module.Basis ι R V) (z : TensorProduct R (HahnSeries Γ R) V) (i : ι) (g : Γ) : (((TensorProduct.equivFinsuppOfBasisRight b) z) i).coeff g = (b.repr (((of R).symm ((tensorProductToHahnModule Γ R V) z)).coeff g)) i

In any basis of the coefficient module, scalar-series coordinates agree with the coordinates of the coefficients of the scalar-extension comparison.

theorem HahnModule.tensorProductToHahnModule_injective {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] [Module.Free R V] : Function.Injective ⇑(tensorProductToHahnModule Γ R V)

The scalar-extension comparison is injective for free coefficient modules, without any finiteness assumption on a basis.

theorem HahnModule.exists_fg_coeff_tensorProductToHahnModule {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommSemiring R] [AddCommMonoid V] [Module R V] (z : TensorProduct R (HahnSeries Γ R) V) : ∃ (S : Submodule R V), S.FG ∧ ∀ (g : Γ), ((of R).symm ((tensorProductToHahnModule Γ R V) z)).coeff g ∈ S

All coefficients of a tensor current lie in one finitely generated submodule. This is the finite-rank obstruction to representing arbitrary vector-valued series by tensor currents.

theorem HahnModule.mem_range_tensorProductToHahnModule_iff {Γ : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [Field K] [AddCommGroup V] [Module K V] (x : HahnModule Γ K V) : x ∈ Set.range ⇑(tensorProductToHahnModule Γ K V) ↔ ∃ (S : Submodule K V), FiniteDimensional K ↥S ∧ ∀ (g : Γ), ((of K).symm x).coeff g ∈ S

A vector-valued Hahn series comes from scalar extension exactly when all its coefficients lie in a single finite-dimensional subspace.

theorem HahnModule.notMem_range_tensorProductToHahnModule_of_linearIndependent {Γ : Type u_1} {R : Type u_2} {V : Type u_3} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [CommRing R] [Nontrivial R] [AddCommGroup V] [Module R V] {ι : Type u_4} [Infinite ι] (x : HahnModule Γ R V) (e : ι → Γ) (h : LinearIndependent R fun (i : ι) => ((of R).symm x).coeff (e i)) : x ∉ Set.range ⇑(tensorProductToHahnModule Γ R V)

A series with an infinite independent family of coefficients is not a tensor current.

theorem HahnModule.tensorProductToHahnModule_int_surjective_iff {R : Type u_2} {V : Type u_3} [CommRing R] [AddCommGroup V] [Module R V] [Module.Free R V] : Function.Surjective ⇑(tensorProductToHahnModule ℤ R V) ↔ Module.Finite R V

For free coefficients over a commutative ring, scalar extension to Laurent series is surjective exactly when the coefficient module is finitely generated. Over a field this is finite-dimensionality, with no characteristic-zero hypothesis.