Coefficientwise extension of bilinear maps to Hahn series

A biadditive map Φ : V → W → M extends to Hahn series with coefficients in V and W by convolution of coefficients,

Φ(x, y)_c = ∑_{a + b = c} Φ(x_a, y_b),

with values in M-valued Hahn series. Each sum is finite, because the supports are partially well-ordered, and the support of Φ(x, y) lies in the sum of the supports. On monomials, Φ(v tᵃ, w tᵇ) = Φ(v, w) tᵃ⁺ᵇ, and if Φ is R-bilinear then so is its extension. For Γ = ℤ and a bilinear form on a module V over a field K, this pairs the V-valued Laurent series V((t)) with themselves to the scalar Laurent series K((t)), and coefficients of the result give residue pairings.

The arguments are module-valued series HahnModule Γ R V, the carrier on which scalar series act, and the value is a Hahn series, so that a bilinear form produces a scalar series.

Main definitions and results

• HahnModule.convolutionAddMonoidHom Γ R Φ: the coefficientwise extension of a biadditive map Φ, as a biadditive map.
• HahnModule.convolution Γ Φ: the coefficientwise extension of an R-bilinear map Φ, as an R-bilinear map.
• HahnModule.convolution_apply: the extension of a bilinear map is the extension of the underlying biadditive map.
• HahnModule.coeff_convolutionAddMonoidHom, HahnModule.coeff_convolution: the coefficient formula.
• HahnModule.support_convolutionAddMonoidHom_subset, HahnModule.support_convolution_subset: the support lies in the sum of the supports.
• HahnModule.convolutionAddMonoidHom_single_single, HahnModule.convolution_single_single: the extension on monomials.
• HahnModule.convolutionAddMonoidHom_map_map, HahnModule.map_convolutionAddMonoidHom: the extension is natural in the coefficients of the arguments and of the values.

The convolution bracket HahnModule.instBracket of Lie-valued series is the extension of the biadditive Lie bracket.

noncomputable def HahnModule.convolutionAddMonoidHom (Γ : Type u_1) (R : Type u_2) {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] (Φ : V →+ W →+ M) : HahnModule Γ R V →+ HahnModule Γ R W →+ HahnSeries Γ M

The coefficientwise extension Φ(x, y)_c = ∑_{a + b = c} Φ(x_a, y_b) of a biadditive map Φ : V → W → M to Hahn series with coefficients in V and W, as a biadditive map.

theorem HahnModule.coeff_convolutionAddMonoidHom {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] (Φ : V →+ W →+ M) (x : HahnModule Γ R V) (y : HahnModule Γ R W) (c : Γ) : (((convolutionAddMonoidHom Γ R Φ) 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_convolutionAddMonoidHom_left' {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] {Φ : V →+ W →+ M} {x : HahnModule Γ R V} {y : HahnModule Γ R W} {c : Γ} {s : Set Γ} (hs : s.IsPWO) (hxs : ((of R).symm x).support ⊆ s) : (((convolutionAddMonoidHom Γ R Φ) 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 convolutionAddMonoidHom Γ R Φ x y may be computed over any partially well-ordered set containing the support of x.

theorem HahnModule.coeff_convolutionAddMonoidHom_right' {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] {Φ : V →+ W →+ M} {x : HahnModule Γ R V} {y : HahnModule Γ R W} {c : Γ} {s : Set Γ} (hs : s.IsPWO) (hys : ((of R).symm y).support ⊆ s) : (((convolutionAddMonoidHom Γ R Φ) 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 convolutionAddMonoidHom Γ R Φ x y may be computed over any partially well-ordered set containing the support of y.

theorem HahnModule.support_convolutionAddMonoidHom_subset {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] (Φ : V →+ W →+ M) (x : HahnModule Γ R V) (y : HahnModule Γ R W) : (((convolutionAddMonoidHom Γ R Φ) x) y).support ⊆ ((of R).symm x).support + ((of R).symm y).support

The support of Φ(x, y) lies in the sum of the supports of x and y.

@[simp]

theorem HahnModule.convolutionAddMonoidHom_single_single {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] (Φ : V →+ W →+ M) (a b : Γ) (v : V) (w : W) : ((convolutionAddMonoidHom Γ R Φ) ((of R) ((HahnSeries.single a) v))) ((of R) ((HahnSeries.single b) w)) = (HahnSeries.single (a + b)) ((Φ v) w)

The extension on monomials: Φ(v tᵃ, w tᵇ) = Φ(v, w) tᵃ⁺ᵇ.

theorem HahnModule.convolutionAddMonoidHom_map_map {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] {V' : Type u_6} {W' : Type u_7} {F : Type u_8} {G : Type u_9} [AddCommMonoid V'] [AddCommMonoid W'] [SMul R V'] [SMul R W'] [FunLike F V V'] [AddMonoidHomClass F V V'] [FunLike G W W'] [AddMonoidHomClass G W W'] (Φ : V' →+ W' →+ M) (g : F) (h : G) (x : HahnModule Γ R V) (y : HahnModule Γ R W) : ((convolutionAddMonoidHom Γ R Φ) ((of R) (((of R).symm x).map g))) ((of R) (((of R).symm y).map h)) = ((convolutionAddMonoidHom Γ R ((Φ.comp ↑g).compl₂ ↑h)) x) y

Naturality in the arguments: applying additive maps g and h to the coefficients of the arguments and then extending Φ is extending (v, w) ↦ Φ (g v) (h w).

theorem HahnModule.map_convolutionAddMonoidHom {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [SMul R V] [SMul R W] {M' : Type u_6} {F : Type u_7} [AddCommMonoid M'] [FunLike F M M'] [AddMonoidHomClass F M M'] (Φ : V →+ W →+ M) (k : F) (x : HahnModule Γ R V) (y : HahnModule Γ R W) : (((convolutionAddMonoidHom Γ R Φ) x) y).map k = ((convolutionAddMonoidHom Γ R (Φ.compr₂ ↑k)) x) y

Naturality in the values: applying an additive map k to the coefficients of the extension of Φ is extending (v, w) ↦ k (Φ v w).

noncomputable def HahnModule.convolution (Γ : Type u_1) {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [CommSemiring R] [Module R V] [Module R W] [Module R M] (Φ : V →ₗ[R] W →ₗ[R] M) : HahnModule Γ R V →ₗ[R] HahnModule Γ R W →ₗ[R] HahnSeries Γ M

The coefficientwise extension Φ(x, y)_c = ∑_{a + b = c} Φ(x_a, y_b) of an R-bilinear map Φ : V → W → M to Hahn series with coefficients in V and W. It is HahnModule.convolutionAddMonoidHom of Φ, which is moreover R-bilinear.

theorem HahnModule.convolution_apply {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [CommSemiring R] [Module R V] [Module R W] [Module R M] (Φ : V →ₗ[R] W →ₗ[R] M) (x : HahnModule Γ R V) (y : HahnModule Γ R W) : ((convolution Γ Φ) x) y = ((convolutionAddMonoidHom Γ R (LinearMap.toAddMonoidHom'.comp Φ.toAddMonoidHom)) x) y

The extension of an R-bilinear map is the extension convolutionAddMonoidHom of the underlying biadditive map.

theorem HahnModule.coeff_convolution {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [CommSemiring R] [Module R V] [Module R W] [Module R M] (Φ : V →ₗ[R] W →ₗ[R] M) (x : HahnModule Γ R V) (y : HahnModule Γ R W) (c : Γ) : (((convolution Γ Φ) 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.support_convolution_subset {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [CommSemiring R] [Module R V] [Module R W] [Module R M] (Φ : V →ₗ[R] W →ₗ[R] M) (x : HahnModule Γ R V) (y : HahnModule Γ R W) : (((convolution Γ Φ) x) y).support ⊆ ((of R).symm x).support + ((of R).symm y).support

The support of Φ(x, y) lies in the sum of the supports of x and y.

@[simp]

theorem HahnModule.convolution_single_single {Γ : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} {M : Type u_5} [AddCommMonoid Γ] [PartialOrder Γ] [IsOrderedCancelAddMonoid Γ] [AddCommMonoid V] [AddCommMonoid W] [AddCommMonoid M] [CommSemiring R] [Module R V] [Module R W] [Module R M] (Φ : V →ₗ[R] W →ₗ[R] M) (a b : Γ) (v : V) (w : W) : ((convolution Γ Φ) ((of R) ((HahnSeries.single a) v))) ((of R) ((HahnSeries.single b) w)) = (HahnSeries.single (a + b)) ((Φ v) w)

The extension on monomials: Φ(v tᵃ, w tᵇ) = Φ(v, w) tᵃ⁺ᵇ.