Affine point counts over canonical finite-field extensions

For a finite field K of characteristic p, Mathlib provides a chosen degree-n extension FiniteField.Extension K p n. This file base-changes a bivariate polynomial to that field and counts its affine zeros. It also records the cardinality of the extension, compatibility with degree one, and the geometric hypotheses preserved by this base change.

@[reducible, inline]

abbrev BGS.HasseWeil.AffineBivariatePoint {F : Type u_1} [CommRing F] (f : MvPolynomial (Fin 2) F) : Type u_1

Affine zeros of a bivariate polynomial, represented by ordered pairs.

Equations

• BGS.HasseWeil.AffineBivariatePoint f = { z : F × F // (MvPolynomial.eval ![z.1, z.2]) f = 0 }

noncomputable def BGS.HasseWeil.affineBivariatePointCount {F : Type u_1} [CommRing F] (f : MvPolynomial (Fin 2) F) : ℕ

The number of affine zeros of a bivariate polynomial over a finite coefficient ring.

Equations

• BGS.HasseWeil.affineBivariatePointCount f = Nat.card (BGS.HasseWeil.AffineBivariatePoint f)

def BGS.HasseWeil.affineBivariatePointMapEquiv {E : Type u_1} {F : Type u_2} [CommRing E] [CommRing F] (e : E ≃+* F) (f : MvPolynomial (Fin 2) E) : AffineBivariatePoint f ≃ AffineBivariatePoint ((MvPolynomial.map e.toRingHom) f)

Transport affine zeros along a coefficient-ring equivalence.

Equations

• BGS.HasseWeil.affineBivariatePointMapEquiv e f = (e.prodCongr e.toEquiv).subtypeEquiv ⋯

noncomputable def BGS.HasseWeil.extensionPlaneCurvePolynomial (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) : MvPolynomial (Fin 2) (FiniteField.Extension K p n)

The plane polynomial after extension of constants from K to the chosen degree-n finite-field extension.

Equations

• BGS.HasseWeil.extensionPlaneCurvePolynomial K p n f = (MvPolynomial.map (algebraMap K (FiniteField.Extension K p n))) f

noncomputable def BGS.HasseWeil.extensionAffinePointCount (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) : ℕ

The number of affine zeros after extension of constants to degree n.

Equations

• BGS.HasseWeil.extensionAffinePointCount K p n f = BGS.HasseWeil.affineBivariatePointCount (BGS.HasseWeil.extensionPlaneCurvePolynomial K p n f)

theorem BGS.HasseWeil.extensionField_natCard (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] : Nat.card (FiniteField.Extension K p n) = Nat.card K ^ n

The chosen degree-n extension has exactly (#K)^n elements.

noncomputable def BGS.HasseWeil.extensionOneAlgEquiv (K : Type u_1) [Field K] [Finite K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : FiniteField.Extension K p 1 ≃ₐ[K] K

The chosen degree-one extension is noncanonically equivalent to its base field as a K-algebra.

Equations

• BGS.HasseWeil.extensionOneAlgEquiv K p = (FiniteField.algEquivExtension K p 1 K ⋯).symm

noncomputable def BGS.HasseWeil.extensionOneAffinePointEquiv (K : Type u_1) [Field K] [Finite K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : AffineBivariatePoint (extensionPlaneCurvePolynomial K p 1 f) ≃ AffineBivariatePoint f

Affine zeros over the chosen degree-one extension correspond exactly to affine zeros over the base field.

Equations

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

@[simp]

theorem BGS.HasseWeil.extensionAffinePointCount_one (K : Type u_1) [Field K] [Finite K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : extensionAffinePointCount K p 1 f = affineBivariatePointCount f

The degree-one extension point count is the original base-field point count.

theorem BGS.HasseWeil.extensionPlaneCurvePolynomial_absolutelyIrreducible (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible ((MvPolynomial.map (algebraMap (FiniteField.Extension K p n) (AlgebraicClosure (FiniteField.Extension K p n)))) (extensionPlaneCurvePolynomial K p n f))

Absolute irreducibility is preserved after passing to the chosen finite extension.

@[simp]

theorem BGS.HasseWeil.extensionPlaneCurvePolynomial_pderiv (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) (i : Fin 2) : (MvPolynomial.pderiv i) (extensionPlaneCurvePolynomial K p n f) = extensionPlaneCurvePolynomial K p n ((MvPolynomial.pderiv i) f)

Partial differentiation commutes with extension of constants.

theorem BGS.HasseWeil.extensionPlaneCurvePolynomial_pderiv_ne_zero (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) (i : Fin 2) (hpartial : (MvPolynomial.pderiv i) f ≠ 0) : (MvPolynomial.pderiv i) (extensionPlaneCurvePolynomial K p n f) ≠ 0

A nonzero partial derivative remains nonzero after extension of constants.

theorem BGS.HasseWeil.extensionPlaneCurveFunctionField_algebraicClosure_eq_bot (K : Type u_1) [Field K] [Finite K] (p n : ℕ) [Fact (Nat.Prime p)] [CharP K p] [NeZero n] (f : MvPolynomial (Fin 2) K) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : let fE := (MvPolynomial.map (algebraMap K (FiniteField.Extension K p n))) f; have hfE := ⋯; algebraicClosure (FiniteField.Extension K p n) (CorvajaZannier.PlaneCurveFunctionField fE) = ⊥

The function field of the base-changed absolutely irreducible plane curve has the chosen extension as its exact constant field.