Quadratic-extension affine points and base-field places

An affine point over the quadratic constant-field extension does not in general determine a distinct place of the base function field: its Frobenius conjugate has the same affine centre. This file therefore passes through the maximal ideal of the base coordinate ring and keeps the residue-degree weight. Fibres over a closed affine centre have cardinality at most the degree of its residue field (and hence at most two).

The selected normalization place above each closed centre may have larger residue field at a singular point. This only strengthens the weighted count. The final estimate bounds all quadratic-extension affine points by the positive divisor degree, and by the height for a nonzero function.

@[reducible, inline]

abbrev BGS.HasseWeil.SquareExtension (K : Type u_1) [Field K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : Type

Mathlib's chosen quadratic extension of the finite field K.

Equations

• BGS.HasseWeil.SquareExtension K p = FiniteField.Extension K p 2

@[reducible, inline]

abbrev BGS.HasseWeil.SquareExtensionAffinePoint (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : Type

Affine zeros of the base-changed plane equation over the quadratic extension.

Equations

• BGS.HasseWeil.SquareExtensionAffinePoint K p f = BGS.HasseWeil.AffineBivariatePoint (BGS.HasseWeil.extensionPlaneCurvePolynomial K p 2 f)

noncomputable def BGS.HasseWeil.squareExtensionPointEval (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) : CorvajaZannier.PlaneCurveCoordinateRing f →ₐ[K] SquareExtension K p

Evaluation of the base coordinate ring at a quadratic-extension affine point.

Equations

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

@[simp]

theorem BGS.HasseWeil.squareExtensionPointEval_coordinate (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) (i : Fin 2) : (squareExtensionPointEval K p f z) (CorvajaZannier.planeCurveCoordinate f i) = ![(↑z).1, (↑z).2] i

noncomputable def BGS.HasseWeil.squareExtensionPointMaximalIdeal (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) : MaximalSpectrum (CorvajaZannier.PlaneCurveCoordinateRing f)

The base closed affine centre of a quadratic-extension point. The kernel is maximal because the finite image of the evaluation homomorphism is a field.

Equations

• BGS.HasseWeil.squareExtensionPointMaximalIdeal K p f z = { asIdeal := RingHom.ker (BGS.HasseWeil.squareExtensionPointEval K p f z), isMaximal := ⋯ }

@[simp]

theorem BGS.HasseWeil.squareExtensionPointMaximalIdeal_asIdeal (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) : (squareExtensionPointMaximalIdeal K p f z).asIdeal = RingHom.ker (squareExtensionPointEval K p f z)

@[reducible, inline]

abbrev BGS.HasseWeil.SquareExtensionClosedPoint (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : Set (MaximalSpectrum (CorvajaZannier.PlaneCurveCoordinateRing f))

Closed affine centres arising from quadratic-extension points.

Equations

• BGS.HasseWeil.SquareExtensionClosedPoint K p f = Set.range (BGS.HasseWeil.squareExtensionPointMaximalIdeal K p f)

@[instance_reducible]

noncomputable instance BGS.HasseWeil.squareExtensionAffinePointFintype (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : Fintype (SquareExtensionAffinePoint K p f)

Equations

• BGS.HasseWeil.squareExtensionAffinePointFintype K p f = Fintype.ofFinite (BGS.HasseWeil.SquareExtensionAffinePoint K p f)

noncomputable def BGS.HasseWeil.squareExtensionClosedPointMap (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) : ↑(SquareExtensionClosedPoint K p f)

Send a quadratic-extension point to its base closed affine centre.

Equations

• BGS.HasseWeil.squareExtensionClosedPointMap K p f z = ⟨BGS.HasseWeil.squareExtensionPointMaximalIdeal K p f z, ⋯⟩

theorem BGS.HasseWeil.squareExtensionClosedPointMap_surjective (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : Function.Surjective (squareExtensionClosedPointMap K p f)

@[instance_reducible]

noncomputable instance BGS.HasseWeil.squareExtensionClosedPointFintype (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : Fintype ↑(SquareExtensionClosedPoint K p f)

Equations

• BGS.HasseWeil.squareExtensionClosedPointFintype K p f = Fintype.ofFinite ↑(BGS.HasseWeil.SquareExtensionClosedPoint K p f)

@[reducible, inline]

abbrev BGS.HasseWeil.SquareExtensionClosedPointFiber (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) : Type

The fibre of quadratic-extension points above one base closed affine centre.

Equations

• BGS.HasseWeil.SquareExtensionClosedPointFiber K p f m = { z : BGS.HasseWeil.SquareExtensionAffinePoint K p f // BGS.HasseWeil.squareExtensionClosedPointMap K p f z = m }

@[instance_reducible]

noncomputable instance BGS.HasseWeil.squareExtensionClosedPointFiberFintype (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) : Fintype (SquareExtensionClosedPointFiber K p f m)

Equations

• BGS.HasseWeil.squareExtensionClosedPointFiberFintype K p f m = Fintype.ofFinite (BGS.HasseWeil.SquareExtensionClosedPointFiber K p f m)

noncomputable def BGS.HasseWeil.squareExtensionFiberResidueAlgHom (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) (z : SquareExtensionClosedPointFiber K p f m) : (↑m).asIdeal.ResidueField →ₐ[K] SquareExtension K p

A point in a fixed closed-centre fibre gives a K-embedding of that centre's residue field into the quadratic extension.

Equations

• BGS.HasseWeil.squareExtensionFiberResidueAlgHom K p f m z = Ideal.ResidueField.liftₐ (↑m).asIdeal (BGS.HasseWeil.squareExtensionPointEval K p f ↑z) ⋯ ⋯

theorem BGS.HasseWeil.squareExtensionFiberResidueAlgHom_injective (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) : Function.Injective (squareExtensionFiberResidueAlgHom K p f m)

theorem BGS.HasseWeil.squareExtensionClosedPointFiber_card_le_residueDegree (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) : Fintype.card (SquareExtensionClosedPointFiber K p f m) ≤ Module.finrank K (↑m).asIdeal.ResidueField

A closed-centre fibre has cardinality at most the degree of its residue field over K.

theorem BGS.HasseWeil.squareExtensionClosedPoint_residueDegree_le_two (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (m : ↑(SquareExtensionClosedPoint K p f)) : Module.finrank K (↑m).asIdeal.ResidueField ≤ 2

Every such closed affine centre has degree one or two.

noncomputable def BGS.HasseWeil.atPrimeResidueAlgEquiv (K : Type u_1) [Field K] (B : Type u_2) (R : Type u_3) [CommRing B] [Algebra K B] [CommRing R] [Algebra B R] [Algebra K R] [IsScalarTower K B R] [IsLocalRing R] (q : Ideal B) [q.IsMaximal] [IsLocalization.AtPrime R q] : q.ResidueField ≃ₐ[K] IsLocalRing.ResidueField R

The residue field of a maximal ideal is canonically the residue field of its localization at that ideal, as an algebra over any compatible base field.

Equations

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

A selected normalization place above each closed affine centre

theorem BGS.HasseWeil.squareExtensionFrobeniusElement_mem_pointMaximalIdeal (K : Type u_1) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (z : SquareExtensionAffinePoint K p f) : CorvajaZannier.planeCurveCoordinate f 0 ^ Nat.card K ^ 2 - CorvajaZannier.planeCurveCoordinate f 0 ∈ (squareExtensionPointMaximalIdeal K p f z).asIdeal

The first coordinate satisfies the quadratic-extension Frobenius polynomial at every quadratic-extension point.

theorem BGS.HasseWeil.exists_squareExtensionClosedPoint_exhaustiveFinitePlace (K : Type u_1) [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)) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; have this_6 := ⋯; have this_7 := ⋯; ∃ (q : IsDedekindDomain.HeightOneSpectrum ↥(integralClosure (Polynomial K) (CorvajaZannier.PlaneCurveFunctionField f))), IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) q = CorvajaZannier.dominatingValuationSubring ↑m

Every base closed affine centre arising from a quadratic-extension point has an exhaustive finite place above it.

noncomputable def BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace (K : Type u_1) [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)) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; CorvajaZannier.FiniteExtensionFinitePlace K (CorvajaZannier.PlaneCurveFunctionField f)

The selected exhaustive finite place above a quadratic-extension closed affine centre.

Equations

• BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m = Classical.choose ⋯

theorem BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace_spec (K : Type u_1) [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)) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; IsDedekindDomain.HeightOneSpectrum.valuationSubringAtPrime (CorvajaZannier.PlaneCurveFunctionField f) (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m) = CorvajaZannier.dominatingValuationSubring ↑m

The selected place has the prescribed dominating valuation subring.

theorem BGS.HasseWeil.squareExtensionClosedPointExhaustiveFinitePlace_injective (K : Type u_1) [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) : 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 := ⋯; Function.Injective (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond)

Distinct closed affine centres have distinct selected finite places.

theorem BGS.HasseWeil.squareExtensionClosedPoint_residueDegree_le_placeDegree (K : Type u_1) [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)) : 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); Module.finrank K (↑m).asIdeal.ResidueField ≤ CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m))

The residue degree of a closed affine centre is at most the degree of its selected normalization place. The inequality can be strict at a singular centre.

theorem BGS.HasseWeil.squareExtensionAffinePoint_card_le_selectedPlaceDegreeSum (K : Type u_1) [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) : 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); Fintype.card (SquareExtensionAffinePoint K p f) ≤ ∑ m : ↑(SquareExtensionClosedPoint K p f), CorvajaZannier.finiteExtensionPlaceDegree K (CorvajaZannier.PlaneCurveFunctionField f) (Sum.inl (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m))

Quadratic-extension affine points are bounded by the sum of the degrees of one selected normalization place above each closed affine centre. The residue degree is the weight that accounts for Frobenius-conjugate points.

theorem BGS.HasseWeil.squareExtensionAffinePoint_card_le_finiteExtensionHeight_of_selectedPlace_orders_positive (K : Type u_1) [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) (u : CorvajaZannier.PlaneCurveFunctionField f) (hu : u ≠ 0) : have this := ⋯; have hx := ⋯; let this_1 := CorvajaZannier.planeCurveFirstCoordinateRatFuncAlgebra f hx; let this_2 := ((algebraMap (RatFunc K) (CorvajaZannier.PlaneCurveFunctionField f)).comp (algebraMap (Polynomial K) (RatFunc K))).toAlgebra; have this_3 := ⋯; have this_4 := ⋯; have this_5 := ⋯; have this_6 := Classical.decEq (RatFunc K); (∀ (m : ↑(SquareExtensionClosedPoint K p f)), 0 < (CorvajaZannier.finiteExtensionPrincipalDivisor K (CorvajaZannier.PlaneCurveFunctionField f) u) (Sum.inl (squareExtensionClosedPointExhaustiveFinitePlace K p hf hpartialSecond m))) → Fintype.card (SquareExtensionAffinePoint K p f) ≤ CorvajaZannier.finiteExtensionHeight K (CorvajaZannier.PlaneCurveFunctionField f) u

If a nonzero function has positive order at one selected normalization place above every closed affine centre arising over the quadratic extension, then every such affine point is counted by the function's pole height.