Polynomial families of vectors (toward Proposition 12.8) #
A family t ↦ f t of vectors indexed by parameter values t : I → k is polynomial
(IsPoly) if it is a finite sum Σ_j t^{e_j} v_j of monomials with vector coefficients. These
are the specializations of the k[t_i]-valued data of deformation-refinements.tex.
Polynomial families are closed under sums, linear and bilinear maps; over an infinite field a
polynomial family vanishing on the torus t_i ≠ 0 vanishes identically
(IsPoly.eq_zero_of_torus).
def
MultiplicativeBasisDeformations.mono
{k : Type u_1}
[Field k]
{I : Type}
[Fintype I]
(n : I → ℕ)
(t : I → k)
:
k
The monomial t^n = Π_i t_i^{n_i}.
Instances For
theorem
MultiplicativeBasisDeformations.mono_zero
{k : Type u_1}
[Field k]
{I : Type}
[Fintype I]
[DecidableEq I]
(t : I → k)
:
mono 0 t = 1
theorem
MultiplicativeBasisDeformations.mono_one
{k : Type u_1}
[Field k]
{I : Type}
[Fintype I]
[DecidableEq I]
(n : I → ℕ)
:
(mono n fun (x : I) => 1) = 1
theorem
MultiplicativeBasisDeformations.IsPoly.bilin
{k : Type u_1}
[Field k]
{I : Type}
[Fintype I]
[DecidableEq I]
{V : Type u_2}
{W : Type u_3}
{X : Type u_4}
[AddCommGroup V]
[Module k V]
[AddCommGroup W]
[Module k W]
[AddCommGroup X]
[Module k X]
(B : V →ₗ[k] W →ₗ[k] X)
{f : (I → k) → V}
{g : (I → k) → W}
(hf : IsPoly f)
(hg : IsPoly g)
:
IsPoly fun (t : I → k) => (B (f t)) (g t)
theorem
MultiplicativeBasisDeformations.IsPoly.eq_zero_of_torus
{k : Type u_1}
[Field k]
{I : Type}
[Fintype I]
[DecidableEq I]
{V : Type u_2}
[AddCommGroup V]
[Module k V]
[Infinite k]
{f : (I → k) → V}
(hf : IsPoly f)
(h : ∀ (t : I → k), (∀ (i : I), t i ≠ 0) → f t = 0)
(t : I → k)
:
f t = 0
Polynomial identities extend from the torus.