Smooth affine centres and normalization residue fields

For a closed affine centre coming from the quadratic constant-field extension, its residue field embeds into that quadratic extension. Hence every residue satisfies the square-Frobenius identity required by the Stepanov vanishing argument.

At a smooth centre, the local Jacobian criterion identifies the affine local ring as a discrete valuation ring. Its valuation subring inside the function field is therefore the selected dominating normalization valuation. Thus the affine centre and its selected normalization prime have canonically equivalent residue fields; in particular, the selected place has degree at most two and satisfies square Frobenius.

The file also records that nonvanishing of the second partial derivative at a quadratic-extension point is exactly non-membership of that derivative in the corresponding affine maximal ideal.

The smooth partial-Y chart

def BGS.HasseWeil.planeCurveRelationFamily {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Unit → MvPolynomial (Fin 2) K

The singleton relation family presenting the affine plane curve.

Equations

• BGS.HasseWeil.planeCurveRelationFamily f x✝ = f

noncomputable def BGS.HasseWeil.planeCurvePresentationEquiv {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : (MvPolynomial (Fin 2) K ⧸ Ideal.span (Set.range (planeCurveRelationFamily f))) ≃ₐ[K] CorvajaZannier.PlaneCurveCoordinateRing f

The singleton-relation presentation is the usual plane-curve coordinate ring.

Equations

• BGS.HasseWeil.planeCurvePresentationEquiv f = Ideal.quotientEquivAlgOfEq K ⋯

noncomputable def BGS.HasseWeil.planeCurveYPreSubmersivePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.PreSubmersivePresentation K (CorvajaZannier.PlaneCurveCoordinateRing f) (Fin 2) Unit

The plane curve as a one-equation pre-submersive presentation, with the second coordinate chosen as the Jacobian direction.

Equations

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

instance BGS.HasseWeil.planeCurveFinitePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.FinitePresentation K (CorvajaZannier.PlaneCurveCoordinateRing f)

noncomputable def BGS.HasseWeil.planeCurvePartialY {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : CorvajaZannier.PlaneCurveCoordinateRing f

The class of the second partial derivative in the plane-curve coordinate ring.

Equations

• BGS.HasseWeil.planeCurvePartialY f = (BGS.CorvajaZannier.planeCurveQuotientMap f) ((MvPolynomial.pderiv 1) f)

theorem BGS.HasseWeil.planeCurveYPreSubmersivePresentation_jacobian {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : (planeCurveYPreSubmersivePresentation f).jacobian = planeCurvePartialY f

The Jacobian of the chosen one-equation presentation is the second partial derivative.

@[reducible, inline]

abbrev BGS.HasseWeil.PlaneCurvePartialYLocalization {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Type u_1

The principal smooth chart on which the second partial derivative is inverted.

Equations

• BGS.HasseWeil.PlaneCurvePartialYLocalization f = Localization.Away (BGS.HasseWeil.planeCurvePartialY f)

noncomputable def BGS.HasseWeil.planeCurvePartialYLocalizationPreSubmersivePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.PreSubmersivePresentation (CorvajaZannier.PlaneCurveCoordinateRing f) (PlaneCurvePartialYLocalization f) Unit Unit

The local presentation obtained by inverting the second partial derivative.

Equations

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

noncomputable def BGS.HasseWeil.planeCurvePartialYCompositePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.PreSubmersivePresentation K (PlaneCurvePartialYLocalization f) (Unit ⊕ Fin 2) (Unit ⊕ Unit)

The composite presentation from the plane curve to that localization.

Equations

• BGS.HasseWeil.planeCurvePartialYCompositePresentation f = (BGS.HasseWeil.planeCurvePartialYLocalizationPreSubmersivePresentation f).comp (BGS.HasseWeil.planeCurveYPreSubmersivePresentation f)

theorem BGS.HasseWeil.planeCurvePartialYCompositePresentation_jacobian_isUnit {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : IsUnit (planeCurvePartialYCompositePresentation f).jacobian

noncomputable def BGS.HasseWeil.planeCurvePartialYSubmersivePresentation {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.SubmersivePresentation K (PlaneCurvePartialYLocalization f) (Unit ⊕ Fin 2) (Unit ⊕ Unit)

A submersive presentation of the partial-Y smooth chart.

Equations

• BGS.HasseWeil.planeCurvePartialYSubmersivePresentation f = { toPreSubmersivePresentation := BGS.HasseWeil.planeCurvePartialYCompositePresentation f, jacobian_isUnit := ⋯ }

theorem BGS.HasseWeil.planeCurvePartialYLocalization_isStandardSmooth {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : Algebra.IsStandardSmooth K (PlaneCurvePartialYLocalization f)

theorem BGS.HasseWeil.planeCurvePartialYSubmersivePresentation_dimension {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) : (planeCurvePartialYSubmersivePresentation f).dimension = 1

theorem BGS.HasseWeil.squareExtensionClosedPoint_residue_squareFrobenius (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) (z : (↑m).asIdeal.ResidueField) : z ^ Fintype.card K ^ 2 = z

The residue field of every closed affine centre obtained from the quadratic constant-field extension satisfies square Frobenius.

theorem BGS.HasseWeil.squareExtensionPoint_pderiv_not_mem_maximalIdeal (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) (hregular : (MvPolynomial.eval ![(↑z).1, (↑z).2]) ((MvPolynomial.map (algebraMap K (SquareExtension K p))) ((MvPolynomial.pderiv 1) f)) ≠ 0) : (CorvajaZannier.planeCurveQuotientMap f) ((MvPolynomial.pderiv 1) f) ∉ (squareExtensionPointMaximalIdeal K p f z).asIdeal

The second partial derivative is nonzero at a quadratic-extension point exactly in the direction needed for the local Jacobian criterion: its class does not belong to the point's affine maximal ideal.

Smooth closed points are discrete valuation rings

theorem BGS.HasseWeil.squareExtensionClosedPoint_asIdeal_ne_bot_of_partialY (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (m : ↑(SquareExtensionClosedPoint K p f)) (hsmooth : planeCurvePartialY f ∉ (↑m).asIdeal) : (↑m).asIdeal ≠ ⊥

A closed point on the partial-Y smooth locus is not the generic point.

theorem BGS.HasseWeil.planeCurveClosedPoint_localization_isDiscreteValuationRing (K : Type u_2) [Field K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (m : MaximalSpectrum (CorvajaZannier.PlaneCurveCoordinateRing f)) [Finite m.asIdeal.ResidueField] (hm0 : m.asIdeal ≠ ⊥) (hsmooth : planeCurvePartialY f ∉ m.asIdeal) : IsDiscreteValuationRing (Localization.AtPrime m.asIdeal)

A finite-residue closed point on the partial-Y smooth locus has a discrete valuation local ring.

theorem BGS.HasseWeil.squareExtensionClosedPoint_localization_isDiscreteValuationRing (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (m : ↑(SquareExtensionClosedPoint K p f)) (hsmooth : planeCurvePartialY f ∉ (↑m).asIdeal) : IsDiscreteValuationRing (Localization.AtPrime (↑m).asIdeal)

The local ring at a closed point where the second partial derivative does not vanish is a discrete valuation ring. This is the local Jacobian boundary needed to compare the affine curve with its normalization.

noncomputable def BGS.HasseWeil.atPrimeResidueAlgEquivOfCommonLocalization {C : Type u_3} {A : Type u_4} {B : Type u_5} {R : Type u_6} [Field C] [CommRing A] [CommRing B] [CommRing R] [Algebra C A] [Algebra C B] [Algebra A R] [Algebra B R] [Algebra C R] [IsScalarTower C A R] [IsScalarTower C B R] [IsLocalRing R] (m : Ideal A) [m.IsMaximal] (q : Ideal B) [q.IsMaximal] [IsLocalization.AtPrime R m] [IsLocalization.AtPrime R q] : m.ResidueField ≃ₐ[C] q.ResidueField

If two maximal ideals have the same local ring, their residue fields are canonically equivalent over the common coefficient field.

Equations

• BGS.HasseWeil.atPrimeResidueAlgEquivOfCommonLocalization m q = (BGS.HasseWeil.atPrimeResidueAlgEquiv C A R m).trans (BGS.HasseWeil.atPrimeResidueAlgEquiv C B R q).symm

theorem BGS.HasseWeil.finrank_residueField_eq_of_commonLocalization {C : Type u_3} {A : Type u_4} {B : Type u_5} {R : Type u_6} [Field C] [CommRing A] [CommRing B] [CommRing R] [Algebra C A] [Algebra C B] [Algebra A R] [Algebra B R] [Algebra C R] [IsScalarTower C A R] [IsScalarTower C B R] [IsLocalRing R] (m : Ideal A) [m.IsMaximal] (q : Ideal B) [q.IsMaximal] [IsLocalization.AtPrime R m] [IsLocalization.AtPrime R q] : Module.finrank C m.ResidueField = Module.finrank C q.ResidueField

Residue-field degree is preserved across a common localization.

theorem BGS.HasseWeil.squareExtensionClosedPoint_commonLocalization_residue_finrank_le_two (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} {B : Type u_3} {R : Type u_4} [CommRing B] [CommRing R] [Algebra K B] [Algebra (CorvajaZannier.PlaneCurveCoordinateRing f) R] [Algebra B R] [Algebra K R] [IsScalarTower K (CorvajaZannier.PlaneCurveCoordinateRing f) R] [IsScalarTower K B R] [IsLocalRing R] (m : ↑(SquareExtensionClosedPoint K p f)) (q : Ideal B) [q.IsMaximal] [IsLocalization.AtPrime R (↑m).asIdeal] [IsLocalization.AtPrime R q] : Module.finrank K q.ResidueField ≤ 2

A normalization prime sharing its local ring with a quadratic-extension affine centre has residue degree at most two.

theorem BGS.HasseWeil.squareExtensionClosedPoint_commonLocalization_residue_squareFrobenius (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} {B : Type u_3} {R : Type u_4} [CommRing B] [CommRing R] [Algebra K B] [Algebra (CorvajaZannier.PlaneCurveCoordinateRing f) R] [Algebra B R] [Algebra K R] [IsScalarTower K (CorvajaZannier.PlaneCurveCoordinateRing f) R] [IsScalarTower K B R] [IsLocalRing R] (m : ↑(SquareExtensionClosedPoint K p f)) (q : Ideal B) [q.IsMaximal] [IsLocalization.AtPrime R (↑m).asIdeal] [IsLocalization.AtPrime R q] (z : q.ResidueField) : z ^ Fintype.card K ^ 2 = z

A normalization local ring that is also the affine local ring at a quadratic-extension centre has the square-Frobenius residue identity needed by Stepanov's method.

The selected normalization place at a smooth centre

theorem BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace_placeDegree_eq_residueDegree_of_partialY (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ↑(SquareExtensionClosedPoint K p f)) (hsmooth : planeCurvePartialY f ∉ (↑m).asIdeal) : have this := ⋯; have hx := ⋯; let this := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_1 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_2 := ⋯; have this_3 := ⋯; have this := ⋯; have this := Classical.decEq (RatFunc K); CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m)) = Module.finrank K (↑m).asIdeal.ResidueField

At a partial-Y smooth centre, normalization preserves the residue field: the degree of the selected normalization place is exactly the residue degree of its affine centre.

@[instance_reducible]

noncomputable def BGS.HasseWeil.planeSmoothPolynomialAlgebra (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : Algebra (Polynomial K) L

The algebra structure from K[X] to L used in the plane smooth point normalization construction.

Equations

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

theorem BGS.HasseWeil.planeSmoothPolynomialScalarTower (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : IsScalarTower (Polynomial K) (RatFunc K) L

@[instance_reducible]

noncomputable def BGS.HasseWeil.planeSmoothFiniteConstantAlgebra (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : Algebra K ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

The algebra structure from K to (RatFuncFiniteIntegralClosure K L) used in the plane smooth point normalization construction.

Equations

• BGS.HasseWeil.planeSmoothFiniteConstantAlgebra K L = ((algebraMap (Polynomial K) ↥(BGS.CorvajaZannier.RatFuncFiniteIntegralClosure K L)).comp (algebraMap K (Polynomial K))).toAlgebra

theorem BGS.HasseWeil.planeSmoothFiniteConstantTower (K : Type u_2) [Field K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] : IsScalarTower K (Polynomial K) ↥(CorvajaZannier.RatFuncFiniteIntegralClosure K L)

theorem BGS.HasseWeil.finiteExtensionFinitePlace_residue_squareFrobenius_of_degree_le_two (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (L : Type u_3) [Field L] [Algebra (RatFunc K) L] [FiniteDimensional (RatFunc K) L] [Algebra.IsSeparable (RatFunc K) L] [DecidableEq (RatFunc K)] (q : CorvajaZannier.FiniteExtensionFinitePlace K L) (hdegree : CorvajaZannier.finiteExtensionPlaceDegree K L (Sum.inl q) ≤ 2) (z : q.asIdeal.ResidueField) : z ^ Fintype.card K ^ 2 = z

Any finite function-field place of constant-field degree at most two has the square-Frobenius residue identity consumed by the Stepanov restriction map.

theorem BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace_placeDegree_le_two_of_partialY (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ↑(SquareExtensionClosedPoint K p f)) (hsmooth : planeCurvePartialY f ∉ (↑m).asIdeal) : have hx := ⋯; CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m)) ≤ 2

A selected normalization place above a partial-Y smooth quadratic closed point has constant-field degree at most two.

theorem BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace_residue_squareFrobenius_of_partialY (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (m : ↑(SquareExtensionClosedPoint K p f)) (hsmooth : planeCurvePartialY f ∉ (↑m).asIdeal) : have hx := ⋯; ∀ (z : (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m).asIdeal.ResidueField), z ^ Fintype.card K ^ 2 = z

The residue field of the selected normalization place above a partial-Y smooth quadratic closed point satisfies square Frobenius.

noncomputable def BGS.HasseWeil.affinePlaneCurvePointResidueAlgEquiv (K : Type u_2) [Field K] {f : MvPolynomial (Fin 2) K} (z : CorvajaZannier.AffinePlaneCurvePoint f) : (CorvajaZannier.affinePlaneCurvePointMaximalIdeal f z).asIdeal.ResidueField ≃ₐ[K] K

Evaluation identifies the residue field at a rational affine point with the ground field.

Equations

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

theorem BGS.HasseWeil.affinePointExhaustiveFinitePlace_degree_eq_one_of_partialY (K : Type u_2) [Field K] [DecidableEq K] [Finite K] {f : MvPolynomial (Fin 2) K} (hf : Irreducible f) (hpartialFirst : (MvPolynomial.pderiv 0) f ≠ 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (z : CorvajaZannier.AffinePlaneCurvePoint f) (hregular : (MvPolynomial.eval ![(↑z).1, (↑z).2]) ((MvPolynomial.pderiv 1) f) ≠ 0) : have this := ⋯; have hx := ⋯; let this := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_1 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_2 := ⋯; have this_3 := ⋯; have this := ⋯; have this := Classical.decEq (RatFunc K); CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl (affinePointExhaustiveFinitePlace hf hpartialFirst hpartialSecond z)) = 1

The normalization place selected above a rational affine point that is regular in the second-coordinate direction has degree one over the full constant field.