One-point Stepanov grids from a full Riemann-space basis

The usual mixed-order grid chooses both tensor factors at distinct strict levels. For a place of degree greater than one, that discards most of the second Riemann space. This file proves that the second family may instead be any linearly independent family.

Group a relation by the first index. Frobenius linearity turns each row into u i * Frobenius (row i). Every nonzero such term has order

-d i + (#K) * order (row i).

The digits d i < #K are distinct, so these orders remain distinct modulo #K, independently of the orders of the rows. A unique least-order term then rules out a nontrivial relation.

theorem BGS.HasseWeil.powCardLinearMap_injective (K : Type u_1) (A : Type u_2) [Field K] [Fintype K] [Field A] [Algebra K A] (n : ℕ) : Function.Injective ⇑(powCardLinearMap K A n)

Frobenius iteration is injective on a field.

@[instance_reducible]

noncomputable def BGS.HasseWeil.basisGridConstantAlgebra (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 basis grid construction.

Equations

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

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

theorem BGS.HasseWeil.onePointStepanovBasisGrid_linearIndependent (K : Type u_1) [Field K] [Fintype 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} [Finite α] [Finite β] (P : CorvajaZannier.FiniteExtensionPlace K L) (u : α → L) (d : α → ℕ) (v : β → L) (hu : ∀ (i : α), u i ≠ 0) (huOrder : ∀ (i : α), (CorvajaZannier.finiteExtensionPrincipalDivisor K L (u i)) P = -↑(d i)) (hdInjective : Function.Injective d) (hdigit : ∀ (i : α), d i < Fintype.card K) (hvLI : LinearIndependent K v) : LinearIndependent K fun (ij : α × β) => u ij.1 * v ij.2 ^ Fintype.card K

A bounded distinct first pole-order digit and an arbitrary linearly independent second family produce a linearly independent Frobenius product grid.