Stepanov restrictions over a square constant field

Let S/K be a quadratic extension of finite fields and put s = #K. The square-field Stepanov argument is linear over the full constant field S, but its two restrictions are related by the s-power automorphism. Consequently the coefficients of the first restriction must be transformed by that automorphism. This is the semilinear point which is lost if an S-rational point is treated merely as a degree-two place over K.

This file packages the coefficient transform and proves the local residue identity. It makes no point-count or smoothness assertion.

noncomputable def BGS.HasseWeil.squareRootFrobeniusCoefficients (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Algebra K S] {ι : Type u_3} (c : ι →₀ S) : ι →₀ S

Apply the #K-power automorphism coefficientwise to a finite grid over the square constant field.

Equations

• BGS.HasseWeil.squareRootFrobeniusCoefficients K S c = Finsupp.mapRange ⇑(BGS.HasseWeil.powCardAlgHom K S 1) ⋯ c

@[simp]

theorem BGS.HasseWeil.squareRootFrobeniusCoefficients_apply (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Algebra K S] {ι : Type u_3} (c : ι →₀ S) (i : ι) : (squareRootFrobeniusCoefficients K S c) i = c i ^ Fintype.card K

theorem BGS.HasseWeil.squareRootFrobeniusCoefficients_ne_zero (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Algebra K S] {ι : Type u_3} {c : ι →₀ S} (hc : c ≠ 0) : squareRootFrobeniusCoefficients K S c ≠ 0

@[instance_reducible]

noncomputable def BGS.HasseWeil.squareFieldRestrictionConstantAlgebra (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : Algebra S L

The algebra structure from S to L used in the square field stepanov restriction construction.

Equations

• BGS.HasseWeil.squareFieldRestrictionConstantAlgebra S L = ((algebraMap (RatFunc S) L).comp (algebraMap S (RatFunc S))).toAlgebra

theorem BGS.HasseWeil.squareFieldRestrictionConstantTower (S : Type u_2) [Field S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] : IsScalarTower S (RatFunc S) L

noncomputable def BGS.HasseWeil.squareFieldStepanovFirstRestriction (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Algebra K S] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] {α : Type u_4} {β : Type u_5} (f : α → L) (g : β → L) (c : α × β →₀ S) : L

The first square-field restriction. The function grid is f_i g_j^s, while the coefficients are transformed by c ↦ c^s.

Equations

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

theorem BGS.HasseWeil.squareFieldStepanovFirstRestriction_mem (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Fintype S] [DecidableEq S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] {α : Type u_4} {β : Type u_5} (P : CorvajaZannier.FiniteExtensionPlace S L) (f : α → L) (g : β → L) (ell m : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P m) (c : α × β →₀ S) : squareFieldStepanovFirstRestriction K S L f g c ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P (ell + Fintype.card K * m)

The transformed first restriction has the same one-point pole budget as the ordinary first restriction.

theorem BGS.HasseWeil.exists_squareFieldStepanovAuxiliary_of_target_finrank_upper (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Fintype S] [DecidableEq S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (P : CorvajaZannier.FiniteExtensionPlace S L) (f : α → L) (g : β → L) (ell m targetBound : ℕ) (hf : ∀ (i : α), f i ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P ell) (hg : ∀ (j : β), g j ∈ CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P m) (hLI : LinearIndependent S fun (ij : α × β) => f ij.1 * g ij.2 ^ Fintype.card K) (hupper : Module.finrank S ↥(CorvajaZannier.finiteExtensionOnePointRiemannSpace S L P (Fintype.card K * ell + m)) ≤ targetBound) (hnumeric : targetBound < Fintype.card α * Fintype.card β) : ∃ (c : α × β →₀ S), c ≠ 0 ∧ (onePointStepanovSecondRestrictionMap S L f g (Fintype.card K)) c = 0 ∧ squareFieldStepanovFirstRestriction K S L f g c ≠ 0

Rank-nullity over the full square constant field produces a coefficient grid killed by the second restriction. Frobenius injectivity and linear independence of the first grid make the transformed first restriction nonzero.

theorem BGS.HasseWeil.squareFieldStepanovLocalResidue_first_eq_frobenius_second (K : Type u_1) (S : Type u_2) (R : Type u_3) [Field K] [Fintype K] [Field S] [Algebra K S] [CommRing R] [IsLocalRing R] [Algebra S R] [Algebra K R] {α : Type u_4} {β : Type u_5} (F : α → R) (G : β → R) (c : α × β →₀ S) (hsquare : ∀ (z : IsLocalRing.ResidueField R), z ^ Fintype.card K ^ 2 = z) : (stepanovLocalResidueAlgHom S R) ((Finsupp.linearCombination S fun (ij : α × β) => F ij.1 * G ij.2 ^ Fintype.card K) (squareRootFrobeniusCoefficients K S c)) = (powCardAlgHom K (IsLocalRing.ResidueField R) 1) ((stepanovLocalResidueAlgHom S R) ((Finsupp.linearCombination S fun (ij : α × β) => F ij.1 ^ Fintype.card K * G ij.2) c))

With Frobenius-transformed coefficients, the residue of the first restriction is the #K-power of the residue of the second restriction.

theorem BGS.HasseWeil.squareFieldStepanovLocal_first_eq_zero_or_order_pos (K : Type u_1) (S : Type u_2) (R : Type u_3) (L : Type u_4) [Field K] [Fintype K] [Field S] [Algebra K S] [CommRing R] [IsDedekindDomain R] [IsDiscreteValuationRing R] [Algebra S R] [Algebra K R] [Field L] [Algebra R L] [IsFractionRing R L] {α : Type u_5} {β : Type u_6} (F : α → R) (G : β → R) (c : α × β →₀ S) (hsquare : ∀ (z : IsLocalRing.ResidueField R), z ^ Fintype.card K ^ 2 = z) (hsecond : (Finsupp.linearCombination S fun (ij : α × β) => F ij.1 ^ Fintype.card K * G ij.2) c = 0) : (algebraMap R L) ((Finsupp.linearCombination S fun (ij : α × β) => F ij.1 * G ij.2 ^ Fintype.card K) (squareRootFrobeniusCoefficients K S c)) = 0 ∨ 0 < CorvajaZannier.finitePlaceOrder (IsDiscreteValuationRing.maximalIdeal R) ((algebraMap R L) ((Finsupp.linearCombination S fun (ij : α × β) => F ij.1 * G ij.2 ^ Fintype.card K) (squareRootFrobeniusCoefficients K S c)))

Local DVR form of the semilinear square-field vanishing step.

theorem BGS.HasseWeil.squareFieldStepanovFirstRestriction_eq_zero_or_principalDivisor_pos_at_finitePlace (K : Type u_1) (S : Type u_2) [Field K] [Fintype K] [Field S] [Algebra K S] [DecidableEq (RatFunc S)] (L : Type u_3) [Field L] [Algebra (RatFunc S) L] [FiniteDimensional (RatFunc S) L] [Algebra.IsSeparable (RatFunc S) L] {α : Type u_4} {β : Type u_5} (q : CorvajaZannier.FiniteExtensionFinitePlace S L) (f : α → L) (g : β → L) (c : α × β →₀ S) (hfRegular : ∀ (i : α), 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor S L (f i)) (Sum.inl q)) (hgRegular : ∀ (j : β), 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor S L (g j)) (Sum.inl q)) (hsquare : ∀ (z : q.asIdeal.ResidueField), z ^ Fintype.card K ^ 2 = z) (hsecond : (onePointStepanovSecondRestrictionMap S L f g (Fintype.card K)) c = 0) : squareFieldStepanovFirstRestriction K S L f g c = 0 ∨ 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor S L (squareFieldStepanovFirstRestriction K S L f g c)) (Sum.inl q)

Finite-place form of semilinear square-field vanishing. The function field and its places are over the full constant field S; K supplies the half-Frobenius exponent.