One-point Stepanov grids

At an arbitrary exhaustive place, a finite family of nonzero functions with pairwise distinct principal-divisor orders is linearly independent over the constant field. Applying this to products whose pole orders use a mixed-radix encoding gives the one-point Stepanov grid.

The distinguished place is not assumed to have degree one.

@[instance_reducible]

noncomputable def BGS.HasseWeil.onePointStepanovGridConstantAlgebra (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the one point stepanov grid construction.

Equations

• BGS.HasseWeil.onePointStepanovGridConstantAlgebra K L = ((algebraMap (RatFunc K) L).comp (algebraMap K (RatFunc K))).toAlgebra

theorem BGS.HasseWeil.onePointStepanovGridConstantTower (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_smul_apply (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] (P : CorvajaZannier.FiniteExtensionPlace K L) (c : K) (x : L) (hc : c ≠ 0) (hx : x ≠ 0) : (CorvajaZannier.finiteExtensionPrincipalDivisor K L (c • x)) P = (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) P

Multiplication by a nonzero constant does not change the order at an exhaustive place.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_add_eq_left_of_lt (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] (P : CorvajaZannier.FiniteExtensionPlace K L) (x y : L) (hx : x ≠ 0) (hy : y ≠ 0) (hxyOrder : (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) P < (CorvajaZannier.finiteExtensionPrincipalDivisor K L y) P) : x + y ≠ 0 ∧ (CorvajaZannier.finiteExtensionPrincipalDivisor K L (x + y)) P = (CorvajaZannier.finiteExtensionPrincipalDivisor K L x) P

If one summand has strictly smaller order than the other, then the sum is nonzero and has the smaller order.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_sum_eq_zero_or_gt (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {ι : Type u_3} (P : CorvajaZannier.FiniteExtensionPlace K L) (S : Finset ι) (f : ι → L) (a : ℤ) (hf : ∀ i ∈ S, f i ≠ 0) (horder : ∀ i ∈ S, a < (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P) : ∑ i ∈ S, f i = 0 ∨ ∑ i ∈ S, f i ≠ 0 ∧ a < (CorvajaZannier.finiteExtensionPrincipalDivisor K L (∑ i ∈ S, f i)) P

If every summand has order strictly above a, then their finite sum is either zero or also has order strictly above a.

theorem BGS.HasseWeil.finiteExtensionPrincipalDivisor_sum_eq_of_unique_min (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {ι : Type u_3} (P : CorvajaZannier.FiniteExtensionPlace K L) (S : Finset ι) (f : ι → L) (i : ι) (hi : i ∈ S) (hf : ∀ j ∈ S, f j ≠ 0) (hmin : ∀ j ∈ S, j ≠ i → (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P < (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f j)) P) : ∑ j ∈ S, f j ≠ 0 ∧ (CorvajaZannier.finiteExtensionPrincipalDivisor K L (∑ j ∈ S, f j)) P = (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P

A unique least-order term controls a finite sum.

theorem BGS.HasseWeil.linearIndependent_of_injective_finiteExtensionPrincipalDivisor_order (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] {ι : Type u_3} [Finite ι] (P : CorvajaZannier.FiniteExtensionPlace K L) (f : ι → L) (hf : ∀ (i : ι), f i ≠ 0) (horder : Function.Injective fun (i : ι) => (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P) : LinearIndependent K f

A finite family of nonzero functions with pairwise distinct orders at one exhaustive place is linearly independent over the constant field.

def BGS.HasseWeil.onePointStepanovMixedOrder {ι : Type u_3} {κ : Type u_4} (d : ι → ℕ) (e : κ → ℕ) (s : ℕ) (ij : ι × κ) : ℕ

Mixed-radix encoding of two pole-order digits.

Equations

• BGS.HasseWeil.onePointStepanovMixedOrder d e s ij = d ij.1 + s * e ij.2

theorem BGS.HasseWeil.onePointStepanovMixedOrder_injective {ι : Type u_3} {κ : Type u_4} (d : ι → ℕ) (e : κ → ℕ) (s : ℕ) (hd : Function.Injective d) (he : Function.Injective e) (hdigit : ∀ (i : ι), d i < s) : Function.Injective (onePointStepanovMixedOrder d e s)

If the first digit is strictly below the radix, the mixed pole-order encoding is injective.

theorem BGS.HasseWeil.onePointStepanovGrid_order (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {ι : Type u_3} {κ : Type u_4} (P : CorvajaZannier.FiniteExtensionPlace K L) (f : ι → L) (g : κ → L) (d : ι → ℕ) (e : κ → ℕ) (s : ℕ) (hf : ∀ (i : ι), f i ≠ 0) (hg : ∀ (j : κ), g j ≠ 0) (hfOrder : ∀ (i : ι), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P = -↑(d i)) (hgOrder : ∀ (j : κ), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (g j)) P = -↑(e j)) (ij : ι × κ) : (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f ij.1 * g ij.2 ^ s)) P = -↑(onePointStepanovMixedOrder d e s ij)

Exact order of a product in the one-point Stepanov grid.

theorem BGS.HasseWeil.onePointStepanovGrid_linearIndependent (K : Type u_1) [Field K] [DecidableEq (RatFunc K)] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [Finite K] {ι : Type u_3} {κ : Type u_4} [Finite ι] [Finite κ] (P : CorvajaZannier.FiniteExtensionPlace K L) (f : ι → L) (g : κ → L) (d : ι → ℕ) (e : κ → ℕ) (s : ℕ) (hf : ∀ (i : ι), f i ≠ 0) (hg : ∀ (j : κ), g j ≠ 0) (hfOrder : ∀ (i : ι), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) P = -↑(d i)) (hgOrder : ∀ (j : κ), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (g j)) P = -↑(e j)) (hd : Function.Injective d) (he : Function.Injective e) (hdigit : ∀ (i : ι), d i < s) : LinearIndependent K fun (ij : ι × κ) => f ij.1 * g ij.2 ^ s

Two strict-level families whose first pole-order digit is below s produce a linearly independent Stepanov product grid.