Rank-two character kernels in a two-dimensional torus

Two independent integer characters cut out a finite subgroup of a two-dimensional torus. This file proves the sharp elementary bound: the number of common kernel points is at most the absolute determinant of the two character vectors. The proof is valid over an arbitrary field and does not assume that all roots of unity are present.

Applied to three monomials in the support of a plane curve, this bounds the diagonal support stabilizer by the corresponding support determinant and hence by twice the product of the two coordinate degrees.

def BGS.CorvajaZannier.unitPowerFiber {F : Type u_1} [Field F] (g : ℕ) (c : Fˣ) : Type u_1

The fiber of the g-th power map on units.

Equations

• BGS.CorvajaZannier.unitPowerFiber g c = { z : Fˣ // z ^ g = c }

instance BGS.CorvajaZannier.unitPowerFiber_finite {F : Type u_1} [Field F] (g : ℕ) [NeZero g] (c : Fˣ) : Finite (unitPowerFiber g c)

theorem BGS.CorvajaZannier.natCard_unitPowerFiber_le {F : Type u_1} [Field F] (g : ℕ) (hg : 0 < g) (c : Fˣ) : Nat.card (unitPowerFiber g c) ≤ g

A nonzero power equation in one unit has at most its exponent many solutions.

def BGS.CorvajaZannier.torusCharacterKernel (F : Type u_1) [Field F] (a b c d : ℤ) : Type u_1

The common kernel of two integer characters of a two-dimensional algebraic torus.

Equations

• BGS.CorvajaZannier.torusCharacterKernel F a b c d = { z : Fˣ × Fˣ // z.1 ^ a * z.2 ^ b = 1 ∧ z.1 ^ c * z.2 ^ d = 1 }

theorem BGS.CorvajaZannier.finite_torusCharacterKernel_of_det_ne_zero {F : Type u_1} [Field F] (a b c d : ℤ) (hdet : a * d - b * c ≠ 0) : Finite (torusCharacterKernel F a b c d)

A nonzero determinant makes the common character kernel finite. This coarse finiteness proof embeds it into a product of two root-of-unity groups; the sharper cardinal estimate below uses Hermite reduction.

theorem BGS.CorvajaZannier.natCard_torusCharacterKernel_le_det {F : Type u_1} [Field F] (a b c d : ℤ) (hdet : a * d - b * c ≠ 0) : Nat.card (torusCharacterKernel F a b c d) ≤ (a * d - b * c).natAbs

The sharp determinant bound for the common kernel of two characters.

def BGS.CorvajaZannier.planeCurveSupportCharacterStabilizer (F : Type u_1) [Field F] {K : Type u_2} [Field K] (f : MvPolynomial (Fin 2) K) : Type u_1

Diagonal scalings on which every support character of f has the same value. These are precisely the possible diagonal stabilizers detected from the monomial support.

Equations

• BGS.CorvajaZannier.planeCurveSupportCharacterStabilizer F f = { z : Fˣ × Fˣ // ∀ r ∈ f.support, ∀ s ∈ f.support, z.1 ^ (↑(s 0) - ↑(r 0)) * z.2 ^ (↑(s 1) - ↑(r 1)) = 1 }

theorem BGS.CorvajaZannier.natCard_planeCurveSupportCharacterStabilizer_le_supportDet {F : Type u_1} {K : Type u_2} [Field F] [Field K] {f : MvPolynomial (Fin 2) K} {r s t : Fin 2 →₀ ℕ} (hr : r ∈ f.support) (hs : s ∈ f.support) (ht : t ∈ f.support) (hdet : planeCurveSupportDifferenceDet r s t ≠ 0) : Nat.card (planeCurveSupportCharacterStabilizer F f) ≤ (planeCurveSupportDifferenceDet r s t).natAbs

A nonzero support determinant bounds every diagonal support stabilizer.

theorem BGS.CorvajaZannier.natCard_planeCurveSupportCharacterStabilizer_le_twice_bidegree {F : Type u_1} {K : Type u_2} [Field F] [Field K] {f : MvPolynomial (Fin 2) K} (hrank : PlaneCurveSupportHasRankTwo f) : Nat.card (planeCurveSupportCharacterStabilizer F f) ≤ 2 * MvPolynomial.degreeOf 0 f * MvPolynomial.degreeOf 1 f

Rank-two support gives the public bidegree bound for every diagonal support stabilizer.