Frobenius deflation for affine plane curves

If the first partial derivative vanishes in characteristic p, every first coordinate exponent is divisible by p. This module contracts those exponents, proves that substitution X₀ ↦ X₀^p reconstructs the original polynomial, and records the exact invariants needed by the affine Hasse--Weil reduction: absolute irreducibility, the other partial derivative, the supplied bidegree bound, and the finite-field affine point count.

Unlike a coordinate shear, this operation does not enlarge the other coordinate degree, and it strictly lowers the actual first coordinate degree whenever that degree is positive.

noncomputable def BGS.HasseWeil.planeFirstInflateSubstitution (R : Type u_1) [CommRing R] (p : ℕ) : Fin 2 → MvPolynomial (Fin 2) R

Substitute X₀^p for X₀, leaving X₁ unchanged.

Equations

• BGS.HasseWeil.planeFirstInflateSubstitution R p = ![MvPolynomial.X 0 ^ p, MvPolynomial.X 1]

noncomputable def BGS.HasseWeil.planeFirstInflateHom (R : Type u_1) [CommRing R] (p : ℕ) : MvPolynomial (Fin 2) R →ₐ[R] MvPolynomial (Fin 2) R

The one-coordinate Frobenius expansion homomorphism.

Equations

• BGS.HasseWeil.planeFirstInflateHom R p = MvPolynomial.bind₁ (BGS.HasseWeil.planeFirstInflateSubstitution R p)

theorem BGS.HasseWeil.planeFirstInflateHom_C (R : Type u_1) [CommRing R] (p : ℕ) (r : R) : (planeFirstInflateHom R p) (MvPolynomial.C r) = MvPolynomial.C r

@[simp]

theorem BGS.HasseWeil.planeFirstInflateHom_X_zero (R : Type u_1) [CommRing R] (p : ℕ) : (planeFirstInflateHom R p) (MvPolynomial.X 0) = MvPolynomial.X 0 ^ p

@[simp]

theorem BGS.HasseWeil.planeFirstInflateHom_X_one (R : Type u_1) [CommRing R] (p : ℕ) : (planeFirstInflateHom R p) (MvPolynomial.X 1) = MvPolynomial.X 1

theorem BGS.HasseWeil.finSuccEquiv_planeFirstInflateHom (R : Type u_1) [CommRing R] (p : ℕ) (f : MvPolynomial (Fin 2) R) : (MvPolynomial.finSuccEquiv R 1) ((planeFirstInflateHom R p) f) = (Polynomial.expand (MvPolynomial (Fin 1) R) p) ((MvPolynomial.finSuccEquiv R 1) f)

noncomputable def BGS.HasseWeil.planeFirstDeflate (R : Type u_1) [CommRing R] (p : ℕ) (f : MvPolynomial (Fin 2) R) : MvPolynomial (Fin 2) R

Divide the exponents of X₀ by p, discarding coefficients whose exponents are not divisible by p.

Equations

• BGS.HasseWeil.planeFirstDeflate R p f = (MvPolynomial.finSuccEquiv R 1).symm (Polynomial.contract p ((MvPolynomial.finSuccEquiv R 1) f))

theorem BGS.HasseWeil.derivative_finSuccEquiv_eq_finSuccEquiv_pderiv_zero (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : Polynomial.derivative ((MvPolynomial.finSuccEquiv R 1) f) = (MvPolynomial.finSuccEquiv R 1) ((MvPolynomial.pderiv 0) f)

theorem BGS.HasseWeil.planeFirstInflateHom_planeFirstDeflate {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) [CharP R p] (hp : p ≠ 0) (f : MvPolynomial (Fin 2) R) (hderiv : (MvPolynomial.pderiv 0) f = 0) : (planeFirstInflateHom R p) (planeFirstDeflate R p f) = f

theorem BGS.HasseWeil.planeFirstInflateHom_injective {R : Type u_1} [CommRing R] (p : ℕ) (hp : 0 < p) : Function.Injective ⇑(planeFirstInflateHom R p)

theorem BGS.HasseWeil.irreducible_of_planeFirstInflateHom_irreducible {R : Type u_1} [CommRing R] [IsDomain R] (p : ℕ) (hp : p ≠ 0) {f : MvPolynomial (Fin 2) R} (hf : Irreducible ((planeFirstInflateHom R p) f)) : Irreducible f

theorem BGS.HasseWeil.eval_planeFirstInflateHom {R : Type u_1} [CommRing R] (p : ℕ) (f : MvPolynomial (Fin 2) R) (x y : R) : (MvPolynomial.eval ![x, y]) ((planeFirstInflateHom R p) f) = (MvPolynomial.eval ![x ^ p, y]) f

theorem BGS.HasseWeil.pderiv_one_planeFirstInflateHom {R : Type u_1} [CommRing R] (p : ℕ) (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 1) ((planeFirstInflateHom R p) f) = (planeFirstInflateHom R p) ((MvPolynomial.pderiv 1) f)

theorem BGS.HasseWeil.map_planeFirstInflateHom {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (p : ℕ) (φ : R →+* S) (f : MvPolynomial (Fin 2) R) : (MvPolynomial.map φ) ((planeFirstInflateHom R p) f) = (planeFirstInflateHom S p) ((MvPolynomial.map φ) f)

noncomputable def BGS.HasseWeil.scaleFirstExponent (p : ℕ) (m : Fin 2 →₀ ℕ) : Fin 2 →₀ ℕ

Multiply only the first exponent of a plane monomial by p.

Equations

• BGS.HasseWeil.scaleFirstExponent p m = Finsupp.cons (m 0 * p) m.tail

@[simp]

theorem BGS.HasseWeil.scaleFirstExponent_zero (p : ℕ) (m : Fin 2 →₀ ℕ) : (scaleFirstExponent p m) 0 = m 0 * p

@[simp]

theorem BGS.HasseWeil.scaleFirstExponent_one (p : ℕ) (m : Fin 2 →₀ ℕ) : (scaleFirstExponent p m) 1 = m 1

theorem BGS.HasseWeil.scaleFirstExponent_mem_support_planeFirstInflateHom {R : Type u_1} [CommRing R] (p : ℕ) (hp : 0 < p) {f : MvPolynomial (Fin 2) R} {m : Fin 2 →₀ ℕ} (hm : m ∈ f.support) : scaleFirstExponent p m ∈ ((planeFirstInflateHom R p) f).support

theorem BGS.HasseWeil.hasBidegreeAtMost_of_planeFirstInflateHom {R : Type u_1} [CommRing R] (p : ℕ) (hp : 0 < p) {f : MvPolynomial (Fin 2) R} {firstDegree secondDegree : ℕ} (hdegree : External.HasBidegreeAtMost ((planeFirstInflateHom R p) f) firstDegree secondDegree) : External.HasBidegreeAtMost f firstDegree secondDegree

A bidegree bound for a one-coordinate inflation descends to the unexpanded polynomial without loss.

theorem BGS.HasseWeil.degreeOf_zero_planeFirstInflateHom {R : Type u_1} [CommRing R] (p : ℕ) (f : MvPolynomial (Fin 2) R) : MvPolynomial.degreeOf 0 ((planeFirstInflateHom R p) f) = MvPolynomial.degreeOf 0 f * p

theorem BGS.HasseWeil.absolutelyIrreducible_of_planeFirstInflateHom_eq {K : Type u_2} [Field K] (p : ℕ) (hp : p ≠ 0) {f g : MvPolynomial (Fin 2) K} (hfg : (planeFirstInflateHom K p) g = f) (hf : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) g)

theorem BGS.HasseWeil.pderiv_one_ne_zero_of_planeFirstInflateHom_eq {K : Type u_2} [Field K] (p : ℕ) {f g : MvPolynomial (Fin 2) K} (hfg : (planeFirstInflateHom K p) g = f) (hf : (MvPolynomial.pderiv 1) f ≠ 0) : (MvPolynomial.pderiv 1) g ≠ 0

theorem BGS.HasseWeil.degreeOf_zero_lt_of_planeFirstInflateHom_eq {K : Type u_2} [Field K] (p : ℕ) (hp : 1 < p) {f g : MvPolynomial (Fin 2) K} (hfg : (planeFirstInflateHom K p) g = f) (hfpos : 0 < MvPolynomial.degreeOf 0 f) : MvPolynomial.degreeOf 0 g < MvPolynomial.degreeOf 0 f

noncomputable def BGS.HasseWeil.planeFirstFrobeniusPointEquiv (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] : K × K ≃ K × K

Frobenius in the first coordinate, identity in the second.

Equations

• BGS.HasseWeil.planeFirstFrobeniusPointEquiv K p = (frobeniusEquiv K p).prodCongr (Equiv.refl K)

@[simp]

theorem BGS.HasseWeil.planeFirstFrobeniusPointEquiv_apply (K : Type u_2) [Field K] [Fintype K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (z : K × K) : (planeFirstFrobeniusPointEquiv K p) z = (z.1 ^ p, z.2)

noncomputable def BGS.HasseWeil.planeFirstInflateAffineZeroEquiv (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : ↥(External.affinePlaneCurveZeros K ((planeFirstInflateHom K p) f)) ≃ ↥(External.affinePlaneCurveZeros K f)

Frobenius bijects the affine zero set of an inflation with the affine zero set of the unexpanded polynomial.

Equations

• BGS.HasseWeil.planeFirstInflateAffineZeroEquiv K p f = (BGS.HasseWeil.planeFirstFrobeniusPointEquiv K p).subtypeEquiv ⋯

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_planeFirstInflateHom (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) : (External.affinePlaneCurveZeros K ((planeFirstInflateHom K p) f)).card = (External.affinePlaneCurveZeros K f).card

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_eq_of_planeFirstInflateHom_eq (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (p : ℕ) [Fact (Nat.Prime p)] [CharP K p] {f g : MvPolynomial (Fin 2) K} (hfg : (planeFirstInflateHom K p) g = f) : (External.affinePlaneCurveZeros K g).card = (External.affinePlaneCurveZeros K f).card

theorem BGS.HasseWeil.exists_planeFirstFrobeniusDeflationStep (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialFirst : (MvPolynomial.pderiv 0) f = 0) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) (hfirstDegree : 0 < MvPolynomial.degreeOf 0 f) : ∃ (g : MvPolynomial (Fin 2) K), (planeFirstInflateHom K (ringChar K)) g = f ∧ External.HasBidegreeAtMost g firstDegree secondDegree ∧ Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) g) ∧ (MvPolynomial.pderiv 1) g ≠ 0 ∧ MvPolynomial.degreeOf 0 g < MvPolynomial.degreeOf 0 f ∧ (External.affinePlaneCurveZeros K g).card = (External.affinePlaneCurveZeros K f).card

One strict Frobenius-deflation step in the first coordinate. The second partial derivative is retained, absolute irreducibility and the affine point count descend, and no supplied bidegree bound is enlarged.

theorem BGS.HasseWeil.exists_planeFirstSeparatingDeflation_or_degreeOf_zero (K : Type u_2) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) (firstDegree secondDegree : ℕ) (hdegree : External.HasBidegreeAtMost f firstDegree secondDegree) (habsolute : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) (hpartialSecond : (MvPolynomial.pderiv 1) f ≠ 0) : MvPolynomial.degreeOf 0 f = 0 ∨ ∃ (g : MvPolynomial (Fin 2) K), External.HasBidegreeAtMost g firstDegree secondDegree ∧ Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) g) ∧ (MvPolynomial.pderiv 0) g ≠ 0 ∧ (MvPolynomial.pderiv 1) g ≠ 0 ∧ (External.affinePlaneCurveZeros K g).card = (External.affinePlaneCurveZeros K f).card

Iterating the strict first-coordinate step terminates. Unless the original polynomial has actual first degree zero, it produces a polynomial with both coordinate partials nonzero, without increasing the supplied bidegree bounds or changing the affine point count.