Families of vectors and operators depending polynomially on a parameter

A family c ↦ ∑ m < d, c ^ m • u m of vectors of a module, or of linear maps between modules, is the general shape of a family depending polynomially on a scalar parameter. This file proves the two statements such a family is used through.

Recovering the coefficients. Let R be an infinite integral domain and M a torsion-free R-module. Then the coefficients of a power sum in M are determined by its values: if ∑ m < d, c ^ m • u m = 0 for every c : R, then u m = 0 for every m < d (TauCeti.eq_zero_of_forall_sum_range_pow_smul_eq_zero), and two power sums of the same length that agree at every c : R have the same coefficients below that length (TauCeti.eq_of_forall_sum_range_pow_smul_eq). Neither hypothesis can be dropped. Over the finite field 𝔽₂ the functions c ↦ c and c ↦ c ^ 2 agree. In the ℤ-module ℤ/2, which has torsion, c ↦ c • 1 and c ↦ c ^ 2 • 1 agree.

Producing the coefficients. Conversely, let K be a commutative semiring and f c a family of K-linear maps between modules with finite bases. If every matrix entry of f c against these bases is a fixed polynomial evaluated at c, then f is such a power sum: there are a length d and linear maps A m with f c = ∑ m < d, c ^ m • A m for every c : K (Module.Basis.exists_forall_eq_sum_pow_smul_of_toMatrix_eq_eval).

Together they are how a representation of a matrix group whose matrix entries are polynomial functions is expanded along a one-parameter subgroup and its terms then identified.

Main results

• TauCeti.eq_zero_of_forall_sum_range_pow_smul_eq_zero: the coefficients below d of an identically vanishing power sum ∑ m < d, c ^ m • u m are zero.
• TauCeti.eq_of_forall_sum_range_pow_smul_eq: two power sums of length d agreeing at every point have the same coefficients below d.
• Module.Basis.exists_forall_eq_sum_pow_smul_of_toMatrix_eq_eval: a family of linear maps with polynomial matrix entries is a finite power sum of fixed linear maps.

Recovering the coefficients from the values

theorem TauCeti.eq_zero_of_forall_sum_range_pow_smul_eq_zero {R : Type u} [CommRing R] [IsDomain R] [Infinite R] {M : Type v} [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {d : ℕ} {u : ℕ → M} (h : ∀ (c : R), ∑ m ∈ Finset.range d, c ^ m • u m = 0) {m : ℕ} (hm : m < d) : u m = 0

A power sum with vector coefficients that vanishes identically has zero coefficients. Let R be an infinite integral domain and M a torsion-free R-module. If ∑ m < d, c ^ m • u m = 0 for every c : R, then u m = 0 for every m < d.

theorem TauCeti.eq_of_forall_sum_range_pow_smul_eq {R : Type u} [CommRing R] [IsDomain R] [Infinite R] {M : Type v} [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {d : ℕ} {u v : ℕ → M} (h : ∀ (c : R), ∑ m ∈ Finset.range d, c ^ m • u m = ∑ m ∈ Finset.range d, c ^ m • v m) {m : ℕ} (hm : m < d) : u m = v m

Two power sums with vector coefficients that agree at every point have the same coefficients. Let R be an infinite integral domain and M a torsion-free R-module. If ∑ m < d, c ^ m • u m = ∑ m < d, c ^ m • v m for every c : R, then u m = v m for every m < d.

Producing the coefficients from polynomial matrix entries

theorem Module.Basis.exists_forall_eq_sum_pow_smul_of_toMatrix_eq_eval {K : Type u} [CommSemiring K] {V : Type v} {W : Type v'} [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] {ι : Type w} {κ : Type w'} [Fintype ι] [Finite κ] [DecidableEq ι] (b : Basis ι K V) (b' : Basis κ K W) (f : K → V →ₗ[K] W) (Q : κ → ι → Polynomial K) (hQ : ∀ (c : K) (a : κ) (a' : ι), (LinearMap.toMatrix b b') (f c) a a' = Polynomial.eval c (Q a a')) : ∃ (d : ℕ) (A : ℕ → V →ₗ[K] W), ∀ (c : K), f c = ∑ m ∈ Finset.range d, c ^ m • A m

A family of linear maps whose matrix entries are polynomial in the parameter is a finite power sum of fixed linear maps. Let K be a commutative semiring, b and b' finite bases of V and W, and f : K → V →ₗ[K] W. If the matrix of f c against b and b' has entries (Q a a').eval c for every c : K, then there are d : ℕ and linear maps A m : V →ₗ[K] W with f c = ∑ m < d, c ^ m • A m for every c : K.