Finite power blocks for a linear parameter. Their dimension grows with slope at most the number of field-basis vectors, giving the upper Hilbert growth bound needed to recognize a parameter of full degree.
def
CCDN.parameterPowerSpan
(K : Type u_1)
{F : Type u_2}
{ι : Type u_3}
[Field K]
[Field F]
[Algebra K F]
(u : F)
(v : ι → F)
(N : ℕ)
:
Submodule K F
Powers through N of a parameter, multiplied by a fixed finite family.
Equations
- CCDN.parameterPowerSpan K u v N = Submodule.span K (Set.range fun (t : ι × Fin (N + 1)) => u ^ ↑t.2 * v t.1)
Instances For
instance
CCDN.parameterPowerSpan_finite
{K : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[Field K]
[Field F]
[Algebra K F]
[Finite ι]
(u : F)
(v : ι → F)
(N : ℕ)
:
Module.Finite K ↥(parameterPowerSpan K u v N)
theorem
CCDN.parameterPowerSpan_finrank_le
{K : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[Field K]
[Field F]
[Algebra K F]
[Fintype ι]
(u : F)
(v : ι → F)
(N : ℕ)
:
The span of the products u ^ j * v i with j ≤ N has dimension at most
Fintype.card ι * (N + 1).
theorem
CCDN.parameterPowerSpan_mul_mem
{K : Type u_1}
{F : Type u_2}
{ι : Type u_3}
[Field K]
[Field F]
[Algebra K F]
(u : F)
(v : ι → F)
(N : ℕ)
{x : F}
(hx : x ∈ parameterPowerSpan K u v N)
:
Multiplication by the parameter u maps the span of powers up to N into the span of
powers up to N + 1.