Stepanov restriction maps on a finite coefficient grid

For finite families f : α → L and g : β → L, the coefficient space is the free K-module (α × β →₀ K). Its two restriction maps evaluate the same coefficient grid against

• f i * (g j) ^ s, and
• (f i) ^ s * g j.

The maps are defined with Finsupp.linearCombination. One-point pole bounds give codomain restrictions with budgets ell + s * m and s * ell + m. The final results expose exactly the injectivity and finrank interfaces used by exists_auxiliary_of_finrank_lt.

@[instance_reducible]

noncomputable def BGS.HasseWeil.stepanovRestrictionConstantAlgebra (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 stepanov restriction maps construction.

Equations

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

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

noncomputable def BGS.HasseWeil.onePointStepanovFirstRestrictionMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) : (α × β →₀ K) →ₗ[K] L

The first Stepanov restriction: evaluate the coefficient grid against f i * (g j) ^ s.

Equations

• BGS.HasseWeil.onePointStepanovFirstRestrictionMap K L f g s = Finsupp.linearCombination K fun (ij : α × β) => f ij.1 * g ij.2 ^ s

noncomputable def BGS.HasseWeil.onePointStepanovSecondRestrictionMap (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) : (α × β →₀ K) →ₗ[K] L

The second Stepanov restriction: evaluate the coefficient grid against (f i) ^ s * g j.

Equations

• BGS.HasseWeil.onePointStepanovSecondRestrictionMap K L f g s = Finsupp.linearCombination K fun (ij : α × β) => f ij.1 ^ s * g ij.2

@[simp]

theorem BGS.HasseWeil.onePointStepanovFirstRestrictionMap_single (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) (ij : α × β) (c : K) : (onePointStepanovFirstRestrictionMap K L f g s) (Finsupp.single ij c) = c • (f ij.1 * g ij.2 ^ s)

@[simp]

theorem BGS.HasseWeil.onePointStepanovSecondRestrictionMap_single (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) (ij : α × β) (c : K) : (onePointStepanovSecondRestrictionMap K L f g s) (Finsupp.single ij c) = c • (f ij.1 ^ s * g ij.2)

theorem BGS.HasseWeil.finiteExtensionOnePointRiemannSpace_pow_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) {m : ℕ} {x : L} (hx : x ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (s : ℕ) : x ^ s ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (s * m)

Powers multiply a one-point pole budget.

theorem BGS.HasseWeil.onePointStepanovFirstGrid_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (ij : α × β) : f ij.1 * g ij.2 ^ s ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (ell + s * m)

Every basis value of the first restriction has pole budget ell + s * m.

theorem BGS.HasseWeil.onePointStepanovSecondGrid_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (ij : α × β) : f ij.1 ^ s * g ij.2 ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (s * ell + m)

Every basis value of the second restriction has pole budget s * ell + m.

theorem BGS.HasseWeil.onePointStepanovFirstRestrictionMap_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (c : α × β →₀ K) : (onePointStepanovFirstRestrictionMap K L f g s) c ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (ell + s * m)

The whole first linear combination has pole budget ell + s * m.

theorem BGS.HasseWeil.onePointStepanovSecondRestrictionMap_mem (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (c : α × β →₀ K) : (onePointStepanovSecondRestrictionMap K L f g s) c ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (s * ell + m)

The whole second linear combination has pole budget s * ell + m.

noncomputable def BGS.HasseWeil.onePointStepanovFirstCodRestrictionMap (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) : (α × β →₀ K) →ₗ[K] ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (ell + s * m))

The first restriction with its one-point codomain made explicit.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGS.HasseWeil.onePointStepanovSecondCodRestrictionMap (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) : (α × β →₀ K) →ₗ[K] ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (s * ell + m))

The second restriction with its one-point codomain made explicit.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem BGS.HasseWeil.onePointStepanovFirstCodRestrictionMap_coe (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (c : α × β →₀ K) : ↑((onePointStepanovFirstCodRestrictionMap K L P f g ell m s hf hg) c) = (onePointStepanovFirstRestrictionMap K L f g s) c

@[simp]

theorem BGS.HasseWeil.onePointStepanovSecondCodRestrictionMap_coe (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (c : α × β →₀ K) : ↑((onePointStepanovSecondCodRestrictionMap K L P f g ell m s hf hg) c) = (onePointStepanovSecondRestrictionMap K L f g s) c

theorem BGS.HasseWeil.onePointStepanovFirstRestrictionMap_injective_of_linearIndependent (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra (RatFunc K) L] {α : Type u_3} {β : Type u_4} (f : α → L) (g : β → L) (s : ℕ) (hLI : LinearIndependent K fun (ij : α × β) => f ij.1 * g ij.2 ^ s) : Function.Injective ⇑(onePointStepanovFirstRestrictionMap K L f g s)

Linear independence of the first product grid is exactly injectivity of the first restriction map.

theorem BGS.HasseWeil.onePointStepanovFirstRestrictionMap_injective_of_grid (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) : Function.Injective ⇑(onePointStepanovFirstRestrictionMap K L f g s)

The mixed-order Stepanov-grid criterion proves injectivity of the first restriction.

theorem BGS.HasseWeil.onePointStepanovFirstCodRestrictionMap_injective_of_linearIndependent (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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) (ell m s : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (hLI : LinearIndependent K fun (ij : α × β) => f ij.1 * g ij.2 ^ s) : Function.Injective ⇑(onePointStepanovFirstCodRestrictionMap K L P f g ell m s hf hg)

The first codomain restriction remains injective.

theorem BGS.HasseWeil.onePointStepanovCoefficientSpace_finrank (K : Type u_1) [Field K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] : Module.finrank K (α × β →₀ K) = Fintype.card α * Fintype.card β

The coefficient space has dimension equal to the cardinality of its finite product index.

theorem BGS.HasseWeil.onePointStepanovTarget_finrank_lt_coefficientSpace (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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} [Fintype α] [Fintype β] (P : CorvajaZannier.FiniteExtensionPlace K L) (n targetBound : ℕ) (hupper : Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) ≤ targetBound) (hnumeric : targetBound < Fintype.card α * Fintype.card β) : Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) < Module.finrank K (α × β →₀ K)

A target finrank upper bound and a numerical strict inequality give the dimension inequality required by rank-nullity.

theorem BGS.HasseWeil.exists_onePointStepanovAuxiliary_of_target_finrank_upper (K : Type u_1) [Field K] [Fintype K] [DecidableEq 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} [Fintype α] [Fintype β] (P : CorvajaZannier.FiniteExtensionPlace K L) (f : α → L) (g : β → L) (ell m s targetBound : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P m) (hLI : LinearIndependent K fun (ij : α × β) => f ij.1 * g ij.2 ^ s) (hupper : Module.finrank K ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P (s * ell + m)) ≤ targetBound) (hnumeric : targetBound < Fintype.card α * Fintype.card β) : ∃ (c : α × β →₀ K), c ≠ 0 ∧ (onePointStepanovSecondCodRestrictionMap K L P f g ell m s hf hg) c = 0 ∧ (onePointStepanovFirstRestrictionMap K L f g s) c ≠ 0

Concrete rank-nullity interface for the two Stepanov restrictions.

An upper bound for the second one-point target, strictly below the product index cardinality, produces a nonzero coefficient grid killed by the second restriction and detected by the first.