The quadratic Frobenius vanishing step

Let q = #K. The two Stepanov restrictions use the grids

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

At a place whose residue field satisfies z ^ (q ^ 2) = z, the residue of the first grid is the q-Frobenius of the residue of the second grid. Consequently, if the second restriction vanishes and all grid entries are regular at the place, the first restriction either vanishes or has positive order there.

The square-Frobenius identity is an explicit hypothesis. In particular, this file does not assert that every normalization place above a quadratic extension point has residue degree at most two.

def BGS.HasseWeil.stepanovLocalResidueAlgHom (K : Type u_1) (R : Type u_2) [Field K] [CommRing R] [IsLocalRing R] [Algebra K R] : R →ₐ[K] IsLocalRing.ResidueField R

The residue map of a local K-algebra, bundled as a K-algebra map.

Equations

• BGS.HasseWeil.stepanovLocalResidueAlgHom K R = Ideal.Quotient.mkₐ K (IsLocalRing.maximalIdeal R)

@[simp]

theorem BGS.HasseWeil.stepanovLocalResidueAlgHom_apply (K : Type u_1) (R : Type u_2) [Field K] [CommRing R] [IsLocalRing R] [Algebra K R] (r : R) : (stepanovLocalResidueAlgHom K R) r = (algebraMap R (IsLocalRing.ResidueField R)) r

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

The first Stepanov residue is the q-Frobenius of the second residue when every residue satisfies the quadratic Frobenius identity.

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

Local DVR form of square-Frobenius vanishing. If the second local linear combination is zero, the first is either zero in the fraction field or has positive order at the maximal ideal.

theorem BGS.HasseWeil.onePointStepanovFirstRestrictionMap_eq_zero_or_principalDivisor_pos_at_finitePlace (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} (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (f : α → L) (g : β → L) (c : α × β →₀ K) (hfRegular : ∀ (i : α), 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L (f i)) (Sum.inl q)) (hgRegular : ∀ (j : β), 0 ≤ (CorvajaZannier.finiteExtensionPrincipalDivisor K L (g j)) (Sum.inl q)) (hsquare : ∀ (z : q.asIdeal.ResidueField), z ^ Fintype.card K ^ 2 = z) (hsecond : (onePointStepanovSecondRestrictionMap K L f g (Fintype.card K)) c = 0) : (onePointStepanovFirstRestrictionMap K L f g (Fintype.card K)) c = 0 ∨ 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K L ((onePointStepanovFirstRestrictionMap K L f g (Fintype.card K)) c)) (Sum.inl q)

Finite-place form used after the two Stepanov restriction maps.

The families are assumed regular at q. The residue hypothesis is stated on the canonical residue field q.asIdeal.ResidueField; it is transported internally to the residue field of the localized DVR.