A separating coordinate shear for affine plane curves

This file formalizes the invertible linear change of variables (x, y) ↦ (x, x + y). If the first partial derivative of f vanishes but the second does not, the transformed equation has both partial derivatives nonzero. The shear preserves affine point counts and geometric irreducibility, including after extension to an algebraic closure.

The case in which both partial derivatives vanish is deliberately not hidden here: over a finite field it requires the separate characteristic-p argument that an absolutely irreducible nonconstant polynomial cannot be a polynomial in x^p and y^p.

noncomputable def BGS.HasseWeil.divideExponents {σ : Type u_2} (p : ℕ) (m : σ →₀ ℕ) : σ →₀ ℕ

Divide every exponent of a multivariate monomial by p. On the support of a polynomial whose partial derivatives vanish in characteristic p, this is an exact inverse to multiplication of exponents by p.

Equations

• BGS.HasseWeil.divideExponents p m = Finsupp.mapRange (fun (n : ℕ) => n / p) ⋯ m

theorem BGS.HasseWeil.dvd_exponent_of_pderiv_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] (p : ℕ) [CharP R p] {f : MvPolynomial σ R} {i : σ} (hderiv : (MvPolynomial.pderiv i) f = 0) {m : σ →₀ ℕ} (hm : m ∈ f.support) : p ∣ m i

In characteristic p, every exponent occurring in a variable with vanishing partial derivative is divisible by p.

theorem BGS.HasseWeil.smul_divideExponents_eq {R : Type u_1} {σ : Type u_2} [Field R] (p : ℕ) [CharP R p] {f : MvPolynomial σ R} (hderiv : ∀ (i : σ), (MvPolynomial.pderiv i) f = 0) {m : σ →₀ ℕ} (hm : m ∈ f.support) : p • divideExponents p m = m

theorem BGS.HasseWeil.exists_pow_eq_of_forall_pderiv_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] (p : ℕ) [CharP R p] [Fact (Nat.Prime p)] [PerfectRing R p] (f : MvPolynomial σ R) (hderiv : ∀ (i : σ), (MvPolynomial.pderiv i) f = 0) : ∃ (g : MvPolynomial σ R), g ^ p = f

Over a perfect field of positive characteristic, a multivariate polynomial with every partial derivative zero is a p-th power.

theorem BGS.HasseWeil.not_irreducible_of_forall_pderiv_eq_zero {R : Type u_1} {σ : Type u_2} [Field R] (p : ℕ) [Fact (Nat.Prime p)] [CharP R p] [PerfectRing R p] (f : MvPolynomial σ R) (hderiv : ∀ (i : σ), (MvPolynomial.pderiv i) f = 0) : ¬Irreducible f

Hence a polynomial with every partial derivative zero cannot be irreducible over a perfect field of characteristic p.

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

The substitution (x, y) ↦ (x, x + y).

Equations

• BGS.HasseWeil.planeYShearSubstitution R = ![MvPolynomial.X 0, MvPolynomial.X 0 + MvPolynomial.X 1]

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

The inverse substitution (x, y) ↦ (x, y - x).

Equations

• BGS.HasseWeil.planeYUnShearSubstitution R = ![MvPolynomial.X 0, MvPolynomial.X 1 - MvPolynomial.X 0]

@[simp]

theorem BGS.HasseWeil.planeYShearSubstitution_zero (R : Type u_1) [CommRing R] : planeYShearSubstitution R 0 = MvPolynomial.X 0

@[simp]

theorem BGS.HasseWeil.planeYShearSubstitution_one (R : Type u_1) [CommRing R] : planeYShearSubstitution R 1 = MvPolynomial.X 0 + MvPolynomial.X 1

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

The algebra map substituting the sum of the two coordinates for the second coordinate.

Equations

• BGS.HasseWeil.planeYShearHom R = MvPolynomial.bind₁ (BGS.HasseWeil.planeYShearSubstitution R)

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

The algebra map undoing the shear of the second coordinate.

Equations

• BGS.HasseWeil.planeYUnShearHom R = MvPolynomial.bind₁ (BGS.HasseWeil.planeYUnShearSubstitution R)

theorem BGS.HasseWeil.planeYShearHom_comp_planeYUnShearHom (R : Type u_1) [CommRing R] : (planeYShearHom R).comp (planeYUnShearHom R) = AlgHom.id R (MvPolynomial (Fin 2) R)

theorem BGS.HasseWeil.planeYUnShearHom_comp_planeYShearHom (R : Type u_1) [CommRing R] : (planeYUnShearHom R).comp (planeYShearHom R) = AlgHom.id R (MvPolynomial (Fin 2) R)

noncomputable def BGS.HasseWeil.planeYShearAlgEquiv (R : Type u_1) [CommRing R] : MvPolynomial (Fin 2) R ≃ₐ[R] MvPolynomial (Fin 2) R

The polynomial automorphism induced by (x, y) ↦ (x, x + y).

Equations

• BGS.HasseWeil.planeYShearAlgEquiv R = AlgEquiv.ofAlgHom (BGS.HasseWeil.planeYShearHom R) (BGS.HasseWeil.planeYUnShearHom R) ⋯ ⋯

@[simp]

theorem BGS.HasseWeil.planeYShearAlgEquiv_apply (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (planeYShearAlgEquiv R) f = (MvPolynomial.bind₁ (planeYShearSubstitution R)) f

def BGS.HasseWeil.planeYShearPointEquiv (R : Type u_1) [CommRing R] : R × R ≃ R × R

The corresponding bijection of affine points.

Equations

• BGS.HasseWeil.planeYShearPointEquiv R = { toFun := fun (z : R × R) => (z.1, z.1 + z.2), invFun := fun (z : R × R) => (z.1, z.2 - z.1), left_inv := ⋯, right_inv := ⋯ }

theorem BGS.HasseWeil.eval_planeYShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) (z : R × R) : (MvPolynomial.eval ![z.1, z.2]) ((planeYShearAlgEquiv R) f) = (MvPolynomial.eval ![((planeYShearPointEquiv R) z).1, ((planeYShearPointEquiv R) z).2]) f

theorem BGS.HasseWeil.planeYShearAlgEquiv_irreducible_iff (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : Irreducible ((planeYShearAlgEquiv R) f) ↔ Irreducible f

theorem BGS.HasseWeil.pderiv_zero_planeYShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 0) ((planeYShearAlgEquiv R) f) = (planeYShearAlgEquiv R) ((MvPolynomial.pderiv 0) f + (MvPolynomial.pderiv 1) f)

Chain rule in the first coordinate for the shear.

theorem BGS.HasseWeil.pderiv_one_planeYShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 1) ((planeYShearAlgEquiv R) f) = (planeYShearAlgEquiv R) ((MvPolynomial.pderiv 1) f)

Chain rule in the second coordinate for the shear.

theorem BGS.HasseWeil.planeYShearAlgEquiv_pderivs_ne_zero_of_zero_ne (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) (hzero : (MvPolynomial.pderiv 0) f = 0) (hne : (MvPolynomial.pderiv 1) f ≠ 0) : (MvPolynomial.pderiv 0) ((planeYShearAlgEquiv R) f) ≠ 0 ∧ (MvPolynomial.pderiv 1) ((planeYShearAlgEquiv R) f) ≠ 0

If only the second coordinate is separating, the shear makes both coordinates separating.

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

The shear commutes with extension of coefficients.

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

The symmetric substitution (x, y) ↦ (x + y, y).

Equations

• BGS.HasseWeil.planeXShearSubstitution R = ![MvPolynomial.X 0 + MvPolynomial.X 1, MvPolynomial.X 1]

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

The inverse symmetric substitution (x, y) ↦ (x - y, y).

Equations

• BGS.HasseWeil.planeXUnShearSubstitution R = ![MvPolynomial.X 0 - MvPolynomial.X 1, MvPolynomial.X 1]

@[simp]

theorem BGS.HasseWeil.planeXShearSubstitution_zero (R : Type u_1) [CommRing R] : planeXShearSubstitution R 0 = MvPolynomial.X 0 + MvPolynomial.X 1

@[simp]

theorem BGS.HasseWeil.planeXShearSubstitution_one (R : Type u_1) [CommRing R] : planeXShearSubstitution R 1 = MvPolynomial.X 1

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

The algebra map shearing the first coordinate by the second.

Equations

• BGS.HasseWeil.planeXShearHom R = MvPolynomial.bind₁ (BGS.HasseWeil.planeXShearSubstitution R)

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

The algebra map undoing the shear of the first coordinate.

Equations

• BGS.HasseWeil.planeXUnShearHom R = MvPolynomial.bind₁ (BGS.HasseWeil.planeXUnShearSubstitution R)

theorem BGS.HasseWeil.planeXShearHom_comp_planeXUnShearHom (R : Type u_1) [CommRing R] : (planeXShearHom R).comp (planeXUnShearHom R) = AlgHom.id R (MvPolynomial (Fin 2) R)

theorem BGS.HasseWeil.planeXUnShearHom_comp_planeXShearHom (R : Type u_1) [CommRing R] : (planeXUnShearHom R).comp (planeXShearHom R) = AlgHom.id R (MvPolynomial (Fin 2) R)

noncomputable def BGS.HasseWeil.planeXShearAlgEquiv (R : Type u_1) [CommRing R] : MvPolynomial (Fin 2) R ≃ₐ[R] MvPolynomial (Fin 2) R

The polynomial automorphism induced by (x, y) ↦ (x + y, y).

Equations

• BGS.HasseWeil.planeXShearAlgEquiv R = AlgEquiv.ofAlgHom (BGS.HasseWeil.planeXShearHom R) (BGS.HasseWeil.planeXUnShearHom R) ⋯ ⋯

@[simp]

theorem BGS.HasseWeil.planeXShearAlgEquiv_apply (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (planeXShearAlgEquiv R) f = (MvPolynomial.bind₁ (planeXShearSubstitution R)) f

def BGS.HasseWeil.planeXShearPointEquiv (R : Type u_1) [CommRing R] : R × R ≃ R × R

The symmetric shear on affine points.

Equations

• BGS.HasseWeil.planeXShearPointEquiv R = { toFun := fun (z : R × R) => (z.1 + z.2, z.2), invFun := fun (z : R × R) => (z.1 - z.2, z.2), left_inv := ⋯, right_inv := ⋯ }

theorem BGS.HasseWeil.eval_planeXShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) (z : R × R) : (MvPolynomial.eval ![z.1, z.2]) ((planeXShearAlgEquiv R) f) = (MvPolynomial.eval ![((planeXShearPointEquiv R) z).1, ((planeXShearPointEquiv R) z).2]) f

theorem BGS.HasseWeil.planeXShearAlgEquiv_irreducible_iff (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : Irreducible ((planeXShearAlgEquiv R) f) ↔ Irreducible f

theorem BGS.HasseWeil.pderiv_zero_planeXShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 0) ((planeXShearAlgEquiv R) f) = (planeXShearAlgEquiv R) ((MvPolynomial.pderiv 0) f)

Chain rule in the first coordinate for the symmetric shear.

theorem BGS.HasseWeil.pderiv_one_planeXShearAlgEquiv (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) : (MvPolynomial.pderiv 1) ((planeXShearAlgEquiv R) f) = (planeXShearAlgEquiv R) ((MvPolynomial.pderiv 0) f + (MvPolynomial.pderiv 1) f)

Chain rule in the second coordinate for the symmetric shear.

theorem BGS.HasseWeil.planeXShearAlgEquiv_pderivs_ne_zero_of_ne_zero (R : Type u_1) [CommRing R] (f : MvPolynomial (Fin 2) R) (hne : (MvPolynomial.pderiv 0) f ≠ 0) (hzero : (MvPolynomial.pderiv 1) f = 0) : (MvPolynomial.pderiv 0) ((planeXShearAlgEquiv R) f) ≠ 0 ∧ (MvPolynomial.pderiv 1) ((planeXShearAlgEquiv R) f) ≠ 0

If only the first coordinate is separating, the symmetric shear makes both coordinates separating.

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

The symmetric shear commutes with extension of coefficients.

theorem BGS.HasseWeil.planeYShearAlgEquiv_absolutelyIrreducible_iff (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) ((planeYShearAlgEquiv K) f)) ↔ Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)

Absolute irreducibility is invariant under the coordinate shear.

theorem BGS.HasseWeil.planeXShearAlgEquiv_absolutelyIrreducible_iff (K : Type u_1) [Field K] (f : MvPolynomial (Fin 2) K) : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) ((planeXShearAlgEquiv K) f)) ↔ Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)

Absolute irreducibility is invariant under the symmetric shear.

theorem BGS.HasseWeil.pderiv_zero_ne_zero_or_pderiv_one_ne_zero_of_absolutelyIrreducible (K : Type u_1) [Field K] [Finite K] (f : MvPolynomial (Fin 2) K) (hirr : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : (MvPolynomial.pderiv 0) f ≠ 0 ∨ (MvPolynomial.pderiv 1) f ≠ 0

An absolutely irreducible bivariate polynomial over a field of positive characteristic cannot have both partial derivatives zero. The proof passes to the algebraic closure, where perfectness turns simultaneous vanishing into a p-th power.

theorem BGS.HasseWeil.pderivs_ne_zero_or_planeYShear_or_planeXShear_of_absolutelyIrreducible (K : Type u_1) [Field K] [Finite K] (f : MvPolynomial (Fin 2) K) (hirr : Irreducible ((MvPolynomial.map (algebraMap K (AlgebraicClosure K))) f)) : (MvPolynomial.pderiv 0) f ≠ 0 ∧ (MvPolynomial.pderiv 1) f ≠ 0 ∨ (MvPolynomial.pderiv 0) ((planeYShearAlgEquiv K) f) ≠ 0 ∧ (MvPolynomial.pderiv 1) ((planeYShearAlgEquiv K) f) ≠ 0 ∨ (MvPolynomial.pderiv 0) ((planeXShearAlgEquiv K) f) ≠ 0 ∧ (MvPolynomial.pderiv 1) ((planeXShearAlgEquiv K) f) ≠ 0

For an absolutely irreducible plane polynomial over a finite field, either both coordinates already separate or one of the two elementary shears makes both partial derivatives nonzero.

def BGS.HasseWeil.planeYShearAffineZeroEquiv (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : ↥(External.affinePlaneCurveZeros K ((planeYShearAlgEquiv K) f)) ≃ ↥(External.affinePlaneCurveZeros K f)

The shear bijects the affine zero sets before and after substitution.

Equations

• BGS.HasseWeil.planeYShearAffineZeroEquiv K f = (BGS.HasseWeil.planeYShearPointEquiv K).subtypeEquiv ⋯

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_planeYShearAlgEquiv (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : (External.affinePlaneCurveZeros K ((planeYShearAlgEquiv K) f)).card = (External.affinePlaneCurveZeros K f).card

def BGS.HasseWeil.planeXShearAffineZeroEquiv (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : ↥(External.affinePlaneCurveZeros K ((planeXShearAlgEquiv K) f)) ≃ ↥(External.affinePlaneCurveZeros K f)

The symmetric shear bijects the affine zero sets.

Equations

• BGS.HasseWeil.planeXShearAffineZeroEquiv K f = (BGS.HasseWeil.planeXShearPointEquiv K).subtypeEquiv ⋯

theorem BGS.HasseWeil.card_affinePlaneCurveZeros_planeXShearAlgEquiv (K : Type u_1) [Field K] [Fintype K] [DecidableEq K] (f : MvPolynomial (Fin 2) K) : (External.affinePlaneCurveZeros K ((planeXShearAlgEquiv K) f)).card = (External.affinePlaneCurveZeros K f).card