Diagonal stabilizers of plane curves

Describe diagonal scaling through polynomial coefficients and relate curve stabilizers to characters of the support.

noncomputable def BGS.CorvajaZannier.diagonalScale {F : Type u_1} [Field F] (z : Fˣ × Fˣ) (f : MvPolynomial (Fin 2) F) : MvPolynomial (Fin 2) F

Scale the two variables of a bivariate polynomial by a pair of units.

Equations

• BGS.CorvajaZannier.diagonalScale z f = ∑ m ∈ f.support, (MvPolynomial.monomial m) (f.coeff m * ↑z.1 ^ m 0 * ↑z.2 ^ m 1)

theorem BGS.CorvajaZannier.coeff_diagonalScale {F : Type u_1} [Field F] (z : Fˣ × Fˣ) (f : MvPolynomial (Fin 2) F) (m : Fin 2 →₀ ℕ) : (diagonalScale z f).coeff m = f.coeff m * ↑z.1 ^ m 0 * ↑z.2 ^ m 1

theorem BGS.CorvajaZannier.support_diagonalScale {F : Type u_1} [Field F] (z : Fˣ × Fˣ) (f : MvPolynomial (Fin 2) F) : (diagonalScale z f).support = f.support

theorem BGS.CorvajaZannier.eval₂_diagonalScale {F : Type u_1} {L : Type u_2} [Field F] [Field L] (φ : F →+* L) (z : Fˣ × Fˣ) (x y : L) (f : MvPolynomial (Fin 2) F) : MvPolynomial.eval₂ φ ![x, y] (diagonalScale z f) = MvPolynomial.eval₂ φ ![φ ↑z.1 * x, φ ↑z.2 * y] f

theorem BGS.CorvajaZannier.diagonalScale_eq_C_mul_of_dvd {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : f ≠ 0) (z : Fˣ × Fˣ) (hdvd : f ∣ diagonalScale z f) : ∃ (c : F), diagonalScale z f = MvPolynomial.C c * f

A diagonal scaling divisible by the original polynomial differs from it by a scalar. Equality of supports is what rules out a nonconstant quotient.

theorem BGS.CorvajaZannier.planeCurveSupportCharacterStabilizer_of_diagonalScale_eval_zero {F : Type u_1} [Field F] {f : MvPolynomial (Fin 2) F} (hf : Irreducible f) (z : Fˣ × Fˣ) (heval : MvPolynomial.eval₂ (algebraMap F (PlaneCurveFunctionField f)) (planeCurveFunction f) (diagonalScale z f) = 0) (r : Fin 2 →₀ ℕ) : r ∈ f.support → ∀ s ∈ f.support, z.1 ^ (↑(s 0) - ↑(r 0)) * z.2 ^ (↑(s 1) - ↑(r 1)) = 1

If a diagonal scaling of an irreducible plane curve vanishes at its generic point, the scaling lies in the character stabilizer detected by its support.