structure BezoutGenus.SmoothProjectiveCurveWithCoords (k : Type u_2) [Field k] : Type (max u_2 (u_3 + 1))

Bundle of data for a smooth projective curve over k: a Dedekind coordinate ring (as an algebra over k) together with its arithmetic genus.

• CoordinateRing : Type u_3
• instCommRing : CommRing self.CoordinateRing
• instAlgebra : Algebra k self.CoordinateRing
• instIsDomain : IsDomain self.CoordinateRing
• instIsDedekind : IsDedekindDomain self.CoordinateRing
• genus : ℕ

theorem BezoutGenus.jacobian_exists (k : Type u_2) [Field k] (X : SmoothProjectiveCurveWithCoords k) : ∃ (J : Type u_3) (x : AddCommGroup J) (x_1 : Module k J), Module.finrank k J = X.genus ∧ ∃ (Λ : Type u_4) (x_2 : AddCommGroup Λ) (ι : Λ →+ J), Function.Injective ⇑ι ∧ Nonempty (Λ ≃+ (Fin (2 * X.genus) → ℤ))

Existence of the Jacobian of a smooth projective curve X of genus g: a k-vector space J of dimension g containing a discrete abelian subgroup Λ ≅ ℤ^{2g}.

noncomputable def BezoutGenus.bivariateResultant (k : Type u_1) [Field k] (f g : Polynomial (Polynomial k)) : Polynomial k

The resultant of two bivariate polynomials f, g ∈ k[X][X], viewed as a polynomial in k[X].

def BezoutGenus.genusOfSmoothPlaneCurve (d : ℕ) : ℕ

The arithmetic genus of a smooth plane curve of degree d, equal to (d-1)(d-2)/2.