NYLL
Module

KummerRootEvaluation.lean

Nyll.AlgebraicCurves.Divisors.KummerRootEvaluation
2 declarations indexed from sourceView source ↗

Module documentation

Actual roots from Weil reciprocity

Division divisors produce explicit roots by evaluation. The pointed formula retains the basepoint normalization, with no condition on the characteristic.

Imports7
Imported by2

Declarations

theorem

evaluation_quotient_pow

L36 ↗
AlgebraicCurve.Divisor.evaluation_quotient_pow
Documentation

The explicit evaluation root associated with a divisor division relation. The assumptions prescribe divisors of actual functions; reciprocity proves the root equation.

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Divisor
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ClosedCurve
variable [IsAlgClosed K] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
  [FiniteDimensional (RatFunc K) F] [HasPrincipalDivisors K F]
Lean source · statement
theorem evaluation_quotient_pow
    (n : ℕ) (D E B : Divisor K F) (f g : F) (hf : f ≠ 0) (hg : g ≠ 0)
    (hfdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (hgdiv : ∀ v : Place K F, v.ord g = (n : ℤ) * E v - B v)
    (hDE : ∀ v : Place K F, D v = 0 ∨ E v = 0)
    (hDB : ∀ v : Place K F, D v = 0 ∨ B v = 0) :
    (evalFun f E / evalFun g D) ^ n = evalFun f B
theorem

evaluation_quotient_pow_points

L82 ↗
AlgebraicCurve.Divisor.evaluation_quotient_pow_points
Documentation

For the difference of two actual rational places, the evaluation root has the exact basepoint normalization f(x) / f(ε).

Source context 5 commands

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

noncomputable section
namespace AlgebraicCurve.Divisor
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section ClosedCurve
variable [IsAlgClosed K] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
  [FiniteDimensional (RatFunc K) F] [HasPrincipalDivisors K F]
Lean source · statement
theorem evaluation_quotient_pow_points
    (n : ℕ) (D E : Divisor K F) (x ε : Place K F) (f g : F)
    (hf : f ≠ 0) (hg : g ≠ 0)
    (hfdiv : ∀ v : Place K F, v.ord f = (n : ℤ) * D v)
    (hgdiv : ∀ v : Place K F, v.ord g = (n : ℤ) * E v -
      (Finsupp.single x 1 + Finsupp.single ε (-1) : Divisor K F) v)
    (hDE : ∀ v : Place K F, D v = 0 ∨ E v = 0)
    (hDx : D x = 0) (hDε : D ε = 0) :
    (evalFun f E / evalFun g D) ^ n = x.evalAt f / ε.evalAt f

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