noncomputable def ConicRational.invertPoly (R : Type u_1) [CommRing R] (r : R) : Polynomial R

The polynomial r·X - 1, whose root in an extension inverts r.

noncomputable def ConicRational.localizationEquivAdjoinRoot (R : Type u_1) [CommRing R] (r : R) : Localization.Away r ≃ₐ[R] AdjoinRoot (invertPoly R r)

The localization R[1/r] is R-algebra isomorphic to R[X]/(rX - 1).

instance ConicRational.adjoinRoot_isLocalization (R : Type u_1) [CommRing R] (r : R) : IsLocalization.Away r (AdjoinRoot (invertPoly R r))

R[X]/(rX-1) is a localization of R away from r.

theorem ConicRational.adjoinRoot_inv_relation (R : Type u_1) [CommRing R] (r : R) : (AdjoinRoot.of (invertPoly R r)) r * AdjoinRoot.root (invertPoly R r) = 1

The image of r times the adjoined root is 1 in R[X]/(rX - 1).

noncomputable def ConicRational.hyperbolaPoly (k : Type u_1) [CommRing k] : Polynomial (Polynomial k)

The hyperbola defining polynomial X·Y - 1 as a polynomial in Y over k[X].

instance ConicRational.hyperbolaIsLocalization (k : Type u_1) [CommRing k] : IsLocalization.Away Polynomial.X (AdjoinRoot (hyperbolaPoly k))

The hyperbola coordinate ring is the localization of k[X] at X.

theorem ConicRational.hyperbola_xy_eq_one (k : Type u_1) [CommRing k] : (AdjoinRoot.of (hyperbolaPoly k)) Polynomial.X * AdjoinRoot.root (hyperbolaPoly k) = 1

The defining relation xy = 1 in the hyperbola coordinate ring.

theorem ConicRational.powers_X_le_nonZeroDivisors (k : Type u_1) [Field k] : Submonoid.powers Polynomial.X ≤ nonZeroDivisors (Polynomial k)

Over a field, the powers of X are non-zero-divisors in k[X].

instance ConicRational.hyperbolaIsDomain (k : Type u_1) [Field k] : IsDomain (AdjoinRoot (hyperbolaPoly k))

Over a field, the hyperbola coordinate ring k[X, X⁻¹] is an integral domain.

noncomputable def ConicRational.conicPoly (k : Type u_1) [CommRing k] : MvPolynomial (Fin 3) k

The defining polynomial of the projective conic X·Y = Z² in P^2.

def ConicRational.genusDeg (d : ℕ) : ℕ

The genus-degree formula for a smooth plane curve of degree d: g = (d-1)(d-2)/2.

theorem ConicRational.genus_conic_eq_zero : genusDeg 2 = 0

A smooth conic (degree 2 plane curve) has genus zero.

theorem ConicRational.conic_genus_bridge : genusDeg 2 = RiemannRoch.genus 2

Bridge identifying the conic's genus (from the degree formula) with the Riemann-Roch genus RiemannRoch.genus 2.