Linear-algebra core of the Bombieri--Stepanov argument

This file isolates the rank-nullity step from the geometry. A finite controlled-degree space V has two restriction maps. If the second map has target dimension smaller than V, while the first map is injective, there is an auxiliary vector which vanishes under the second restriction but remains nonzero under the first. Once the first restriction is known to lie in a one-point Riemann space and to vanish at every rational intersection point, the exhaustive divisor zero count bounds the number of those points.

theorem BGS.HasseWeil.exists_auxiliary_of_finrank_lt {k : Type u_1} {V : Type u_2} {W₁ : Type u_3} {W₂ : Type u_4} [Field k] [AddCommGroup V] [Module k V] [AddCommGroup W₁] [Module k W₁] [AddCommGroup W₂] [Module k W₂] [FiniteDimensional k W₂] (first : V →ₗ[k] W₁) (second : V →ₗ[k] W₂) (hfirst : Function.Injective ⇑first) (hdim : Module.finrank k W₂ < Module.finrank k V) : ∃ (v : V), v ≠ 0 ∧ second v = 0 ∧ first v ≠ 0

Rank-nullity produces an auxiliary vector killed by second but not by the injective map first.

theorem BGS.HasseWeil.tensor_finrank_gt_of_bounds {k : Type u_1} [Field k] {A : Type u_5} {B : Type u_6} {W : Type u_7} [AddCommGroup A] [Module k A] [FiniteDimensional k A] [AddCommGroup B] [Module k B] [FiniteDimensional k B] [AddCommGroup W] [Module k W] {a b targetBound : ℕ} (hA : a ≤ Module.finrank k A) (hB : b ≤ Module.finrank k B) (hW : Module.finrank k W ≤ targetBound) (hnumeric : targetBound < a * b) : Module.finrank k W < Module.finrank k (TensorProduct k A B)

Riemann-space lower bounds and a target upper bound imply the strict dimension inequality needed by rank-nullity on a tensor product.

@[instance_reducible]

noncomputable def BGS.HasseWeil.stepanovLinearAlgebraConstantAlgebra (K : Type u_5) [Field K] (L : Type u_6) [Field L] [Algebra (RatFunc K) L] : Algebra K L

The algebra structure from K to L used in the stepanov linear algebra construction.

Equations

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

theorem BGS.HasseWeil.stepanovLinearAlgebraConstantTower (K : Type u_5) [Field K] (L : Type u_6) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (RatFunc K) L

theorem BGS.HasseWeil.card_le_mul_placeDegree_of_stepanov_restrictions (K : Type u_5) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_6) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {V : Type u_7} {W : Type u_8} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {ι : Type u_9} [Fintype ι] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (first : V →ₗ[K] L) (second : V →ₗ[K] W) (hfirst : Function.Injective ⇑first) (hdim : Module.finrank K W < Module.finrank K V) (hspace : ∀ (v : V), first v ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) (place : ι → CorvajaZannier.FiniteExtensionPlace K L) (hplace : Function.Injective place) (hvanish : ∀ (v : V), v ≠ 0 → second v = 0 → ∀ (i : ι), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L (first v)) (place i)) : Fintype.card ι ≤ n * CorvajaZannier.finiteExtensionPlaceDegree K L P

Abstract Stepanov zero-count theorem.

The hypotheses after rank-nullity are exactly the geometric obligations left to an application: the first restriction has controlled poles, the selected places are distinct, and vanishing of the second restriction forces positive order of the first restriction at each selected place.

theorem BGS.HasseWeil.card_le_of_stepanov_restrictions_degree_one (K : Type u_5) [Field K] [Fintype K] [DecidableEq K] [DecidableEq (RatFunc K)] (L : Type u_6) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] {V : Type u_7} {W : Type u_8} [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {ι : Type u_9} [Fintype ι] (P : CorvajaZannier.FiniteExtensionPlace K L) (n : ℕ) (first : V →ₗ[K] L) (second : V →ₗ[K] W) (hfirst : Function.Injective ⇑first) (hdim : Module.finrank K W < Module.finrank K V) (hspace : ∀ (v : V), first v ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace K L P n) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree K L P = 1) (place : ι → CorvajaZannier.FiniteExtensionPlace K L) (hplace : Function.Injective place) (hvanish : ∀ (v : V), v ≠ 0 → second v = 0 → ∀ (i : ι), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L (first v)) (place i)) : Fintype.card ι ≤ n

Degree-one version of the abstract Stepanov zero-count theorem.