def NewtonPolygon.exponentToReal (m : Fin 2 →₀ ℕ) : Fin 2 → ℝ

Coerces a finitely-supported exponent vector m : Fin 2 →₀ ℕ into a real-valued function Fin 2 → ℝ, used to place exponents in ℝ² for the Newton polygon.

def NewtonPolygon.newtonSupport {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Fin 2 → ℝ)

The Newton support of a bivariate polynomial f: the image of its monomial exponents in ℝ² (cf. Definition 1.1 of "Elliptic Curves").

def NewtonPolygon.newtonPolygon {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Fin 2 → ℝ)

The Newton polygon Δ(f) of a bivariate polynomial f: the convex hull in ℝ² of the exponents (i, j) with aᵢⱼ ≠ 0 (Definition 1.1).

def NewtonPolygon.newtonPolygonInterior {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Fin 2 → ℝ)

The topological interior Δ°(f) of the Newton polygon of f (Definition 1.1).

def NewtonPolygon.newtonPolygonBoundary {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Fin 2 → ℝ)

The topological boundary ∂Δ(f) of the Newton polygon of f (Definition 1.1).

noncomputable def NewtonPolygon.edgeRestriction {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) (γ : Set (Fin 2 → ℝ)) : MvPolynomial (Fin 2) k

The edge restriction f_γ of a polynomial f to a subset γ ⊆ ℝ²: the sum of the monomials of f whose exponents lie on γ (Definition 1.1).

def NewtonPolygon.integerLattice : Set (Fin 2 → ℝ)

The integer lattice ℤ² ⊆ ℝ² viewed as a subset of Fin 2 → ℝ.

def NewtonPolygon.interiorLatticePoints {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Fin 2 → ℝ)

The set of integer lattice points lying strictly inside the Newton polygon of f, i.e. Δ°(f) ∩ ℤ², appearing on the right-hand side of Baker's theorem.

def NewtonPolygon.innerProduct2 (n p : Fin 2 → ℝ) : ℝ

The standard inner product on Fin 2 → ℝ, used to define supporting hyperplanes for edges of the Newton polygon.

def NewtonPolygon.boundaryEdges {k : Type u_1} [CommSemiring k] (f : MvPolynomial (Fin 2) k) : Set (Set (Fin 2 → ℝ))

The collection of boundary edges of the Newton polygon of f: faces cut out by a supporting hyperplane with nonzero normal vector that contain at least two points.

noncomputable def NewtonPolygon.edgeRestrictionAlgClosure {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) (γ : Set (Fin 2 → ℝ)) : MvPolynomial (Fin 2) (AlgebraicClosure k)

The edge restriction f_γ viewed over the algebraic closure of k, used to test nondegeneracy in the algebraically closed setting.

def NewtonPolygon.IsNondegenerateWrtEdge {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) (γ : Set (Fin 2 → ℝ)) : Prop

A polynomial f is nondegenerate with respect to an edge γ if the polynomials f_γ, x · ∂f_γ/∂x, and y · ∂f_γ/∂y have no common zero in (k̄ˣ)² (Definition 1.3).

def NewtonPolygon.IsNondegenerate {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) : Prop

f is nondegenerate with respect to Δ(f) if it is nondegenerate with respect to every boundary edge and is not divisible by x or y (Definition 1.3).

noncomputable def NewtonPolygon.liftExponent (m : Fin 2 →₀ ℕ) (d : ℕ) : Fin 3 →₀ ℕ

Lift an exponent m ∈ ℕ² to a homogenizing exponent in ℕ³, padding the third component with d − (m₀ + m₁) so the resulting monomial has total degree d.

noncomputable def NewtonPolygon.homogenize {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) : MvPolynomial (Fin 3) k

Homogenize a bivariate polynomial f to a trivariate polynomial f* of the same total degree by inserting an auxiliary variable in the third coordinate.

def NewtonPolygon.IsSingularPoint {k : Type u_1} [Field k] (F : MvPolynomial (Fin 3) (AlgebraicClosure k)) (p : Fin 3 → AlgebraicClosure k) : Prop

A point p ∈ k̄³ is a singular point of a homogeneous polynomial F if it lies on the variety {F = 0} and all partial derivatives of F vanish at p.

def NewtonPolygon.IsCoordinatePoint {k : Type u_1} [Field k] (p : Fin 3 → AlgebraicClosure k) : Prop

A point p ∈ k̄³ is a "coordinate point" if all but one of its coordinates vanish, i.e. it is one of the three points (1:0:0), (0:1:0), (0:0:1).

def NewtonPolygon.HasNoSingularitiesOutsideCoordinatePoints {k : Type u_1} [Field k] (fStar : MvPolynomial (Fin 3) (AlgebraicClosure k)) : Prop

A homogenized polynomial f* has no singularities outside the three coordinate points; this is the smoothness condition appearing in Proposition 1.5.

class FunctionField.GenusData (k : Type u_1) [Field k] : Type u_1

A bundle of data witnessing the existence of a "genus" function on bivariate polynomials over k, packaging invariance under nonzero scaling, the arithmetic genus upper bound, and the equality case for smooth curves.

• genusVal : MvPolynomial (Fin 2) k → ℕ
• genus_invariant_val (f : MvPolynomial (Fin 2) k) (c : k) : c ≠ 0 → genusVal (MvPolynomial.C c * f) = genusVal f
• genus_le_arithmetic_genus_val (f : MvPolynomial (Fin 2) k) : Irreducible ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) f) → genusVal f ≤ (f.totalDegree - 1) * (f.totalDegree - 2) / 2
• genus_eq_arithmetic_genus_of_smooth_val (f : MvPolynomial (Fin 2) k) : Irreducible ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) f) → (∀ (p : Fin 3 → AlgebraicClosure k), (∃ (i : Fin 3), p i ≠ 0) → ¬NewtonPolygon.IsSingularPoint ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) (NewtonPolygon.homogenize f)) p) → genusVal f = (f.totalDegree - 1) * (f.totalDegree - 2) / 2

noncomputable def FunctionField.genusDataExists (k : Type u_1) [Field k] : GenusData k

Existence of a GenusData instance on every field; the construction is deferred.

@[implicit_reducible]

noncomputable instance instGenusData (k : Type u_1) [Field k] : FunctionField.GenusData k

Canonical GenusData instance on any field, supplied by genusDataExists.

noncomputable def FunctionField.genus (k : Type u_1) [Field k] (f : MvPolynomial (Fin 2) k) : ℕ

The genus g(F) of the function field of f, extracted from the chosen GenusData structure on k.

theorem baker_theorem {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) (hirr : Irreducible ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) f)) : FunctionField.genus k f ≤ (NewtonPolygon.interiorLatticePoints f).ncard

Baker's Theorem (Theorem 1.2): if f ∈ k[x, y] is irreducible over k̄, then the genus of its function field is at most the number of interior lattice points of the Newton polygon Δ(f).

theorem NewtonPolygon.genus_eq_interior_lattice_points {k : Type u_1} [Field k] (f : MvPolynomial (Fin 2) k) (hirr : Irreducible ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) f)) (hnd : IsNondegenerate f) (hsing : HasNoSingularitiesOutsideCoordinatePoints ((MvPolynomial.map (algebraMap k (AlgebraicClosure k))) (homogenize f))) : FunctionField.genus k f = (interiorLatticePoints f).ncard

Proposition 1.5: for an irreducible nondegenerate f whose homogenization has no singularities outside the three coordinate points, the genus equals the number of interior lattice points of Δ(f).