NYLL
Module

DegreeOne.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.DegreeOne
1 declaration indexed from sourceView source ↗

Module documentation

Degree-one prime divisors have rational centers

This file formalizes Fried--Jarden, Lemma 6.2.2(c), for an arbitrary map from an affine plane-curve coordinate ring into a function field. Finiteness at a prime divisor gives a residue map on the coordinate ring. When the residue degree is one, every residue class is the image of a unique constant, so the residues of the two coordinates define a K-rational point whose point ideal is the center.

Imports3
Imported by1

Declarations

theorem

exists_rationalPoint_centerAlong_eq_pointIdeal_of_degree_one

L39 ↗
FieldArithmetic.Chapter06.FunctionFieldPrimeDivisor.exists_rationalPoint_centerAlong_eq_pointIdeal_of_degree_one
Documentation

Fried--Jarden, Lemma 6.2.2(c): a degree-one prime divisor which is finite along a plane-curve model map has a K-rational center.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace FunctionFieldPrimeDivisor
open AffinePlaneCurve IsLocalRing
universe u v
variable {K : Type u} {F : Type v}
  [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem exists_rationalPoint_centerAlong_eq_pointIdeal_of_degree_one
    {f : BivariatePolynomial K}
    (ι : CoordinateRing f →ₐ[K] F)
    (v : FunctionFieldPrimeDivisor K F)
    (hfinite : v.FiniteAlong ι)
    (hdegree : v.degree = 1) :
    ∃ p : RationalPoint f,
      v.centerAlong ι hfinite = pointIdeal p

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.