NYLL
Module

RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
72 declarations indexed from sourceView source ↗

Module documentation

RationalFunctionField exists algebraMap of forall ord eq zero

A nonzero rational function whose order vanishes at every place is a nonzero constant. Polynomial- prime divisors and residue evaluation give the required reciprocity calculations.

Imports30
Imported by4

Declarations

instance

(anonymous instance)

L66 ↗
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
instance {K : Type*} [Field K] : HasPrincipalDivisors K (RatFunc K)
theorem

isRational_of_deg_eq_one

L75 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.Place.isRational_of_deg_eq_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem isRational_of_deg_eq_one (h : v.deg = 1) : v.IsRational
theorem

deg_eq_one_of_isRational

L78 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.Place.deg_eq_one_of_isRational
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem deg_eq_one_of_isRational (hv : v.IsRational) : v.deg = 1
theorem

ord_finitePlace_ne_zero_iff

L89 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_finitePlace_ne_zero_iff
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
Lean source · statement
theorem ord_finitePlace_ne_zero_iff {p : K[X]} (hp : Irreducible p) {q : K[X]} (hq : q ≠ 0) :
    (finitePlace K hp).ord (algebraMap K[X] (RatFunc K) q) ≠ 0 ↔ p ∣ q
theorem

inftyValuation_isEquiv_adicValuation

L98 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.inftyValuation_isEquiv_adicValuation
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem inftyValuation_isEquiv_adicValuation :
    (RatFunc.inftyValuation K).IsEquiv (placeInfty K).adicValuation
theorem

placeInfty_ne_ofHeightOneSpectrum

L102 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeInfty_ne_ofHeightOneSpectrum
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem placeInfty_ne_ofHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    placeInfty K ≠ Place.ofHeightOneSpectrum w
theorem

eq_ofHeightOneSpectrum_or_eq_placeInfty

L115 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.eq_ofHeightOneSpectrum_or_eq_placeInfty
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem eq_ofHeightOneSpectrum_or_eq_placeInfty [DecidableEq (RatFunc K)]
    (v : Place K (RatFunc K)) :
    (∃ w : HeightOneSpectrum K[X], v = Place.ofHeightOneSpectrum w) ∨ v = placeInfty K
theorem

exists_sub_algebraMap_intDegree_neg

L129 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.exists_sub_algebraMap_intDegree_neg
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
section DegInfty
variable (K) [DecidableEq (RatFunc K)]
Lean source · statement
theorem exists_sub_algebraMap_intDegree_neg {x : RatFunc K}
    (hx : RatFunc.inftyValuation K x ≤ 1) :
    ∃ c : K, x - algebraMap K (RatFunc K) c = 0 ∨
      (x - algebraMap K (RatFunc K) c).intDegree < 0
theorem

deg_placeInfty

L178 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.deg_placeInfty
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
section DegInfty
variable (K) [DecidableEq (RatFunc K)]
Lean source · statement
theorem deg_placeInfty : (placeInfty K).deg = 1
theorem

le_exp_neg_one_of_lt_one

L209 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.le_exp_neg_one_of_lt_one
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
Lean source · statement
theorem le_exp_neg_one_of_lt_one {x : ℤᵐ⁰} (hx : x < 1) : x ≤ exp (-1 : ℤ)
theorem

isUnit_algebraMap

L223 ↗
AlgebraicCurve.Place.isUnit_algebraMap
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.isUnit_algebraMap {c : K} (hc : c ≠ 0) :
    IsUnit (algebraMap K v.toValuationSubring c)
theorem

adicValuation_algebraMap

L229 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.Place.adicValuation_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem adicValuation_algebraMap {c : K} (hc : c ≠ 0) :
    v.adicValuation (algebraMap K F c) = 1
theorem

ord_ofHeightOneSpectrum_eq_zero_of_notMem

L242 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_zero_of_notMem
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem ord_ofHeightOneSpectrum_eq_zero_of_notMem (w : HeightOneSpectrum K[X]) {q : K[X]}
    (hq : q ≠ 0) (hmem : q ∉ w.asIdeal) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ord
      (algebraMap K[X] (RatFunc K) q) = 0
theorem

ord_placeInfty

L254 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_placeInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section PlaceInftyOrd
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ord_placeInfty {f : RatFunc K} (hf : f ≠ 0) :
    (placeInfty K).ord f = -f.intDegree
theorem

ord_placeInfty_algebraMap

L263 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_placeInfty_algebraMap
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section PlaceInftyOrd
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ord_placeInfty_algebraMap {q : K[X]} (hq : q ≠ 0) :
    (placeInfty K).ord (algebraMap K[X] (RatFunc K) q) = -(q.natDegree : ℤ)
theorem

single_add_single_apply_eq_ord

L273 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.single_add_single_apply_eq_ord
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section IrreducibleDivisor
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem single_add_single_apply_eq_ord {p : K[X]} (hp : Irreducible p)
    (v : Place K (RatFunc K)) :
    (Finsupp.single (finitePlace K hp) (1 : ℤ)
        + Finsupp.single (placeInfty K) (-(p.natDegree : ℤ))) v
      = v.ord (algebraMap K[X] (RatFunc K) p)
theorem

degree_single_add_single

L302 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.degree_single_add_single
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section IrreducibleDivisor
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem degree_single_add_single {p : K[X]} (hp : Irreducible p) :
    Divisor.degree (Finsupp.single (finitePlace K hp) (1 : ℤ)
        + Finsupp.single (placeInfty K) (-(p.natDegree : ℤ))) = 0
def

principalDivisor

L312 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor
Documentation

The finitely supported divisor whose coefficients are the orders of the nonzero function.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
def principalDivisor {f : RatFunc K} (hf : f ≠ 0) : Divisor K (RatFunc K)
theorem

principalDivisor_apply

L316 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem principalDivisor_apply {f : RatFunc K} (hf : f ≠ 0) (v : Place K (RatFunc K)) :
    principalDivisor hf v = v.ord f
theorem

principalDivisor_isPrincipal

L319 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor_isPrincipal
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem principalDivisor_isPrincipal {f : RatFunc K} (hf : f ≠ 0) :
    (principalDivisor hf).IsPrincipal
theorem

degree_principalDivisor

L323 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.degree_principalDivisor
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem degree_principalDivisor {f : RatFunc K} (hf : f ≠ 0) :
    Divisor.degree (principalDivisor hf) = 0
theorem

sum_ord_mul_deg_eq_zero

L327 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.sum_ord_mul_deg_eq_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem sum_ord_mul_deg_eq_zero {f : RatFunc K} (hf : f ≠ 0) :
    ∑ v ∈ (finite_setOf_ord_ne_zero hf).toFinset, v.ord f * (v.deg : ℤ) = 0
theorem

placeOfPoint_ne_placeInfty

L345 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeOfPoint_ne_placeInfty
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
Lean source · statement
theorem placeOfPoint_ne_placeInfty [DecidableEq (RatFunc K)] (a : K) :
    placeOfPoint K a ≠ placeInfty K
theorem

ord_placeOfPoint_algebraMap_eq_mul

L352 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_algebraMap_eq_mul
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem ord_placeOfPoint_algebraMap_eq_mul (a : K) {q : K[X]} (hq : q ≠ 0) :
    (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) q)
      = (rootMultiplicity a q : ℤ)
          * (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) (X - C a))
theorem

dvd_ord_placeOfPoint

L386 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.dvd_ord_placeOfPoint
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem dvd_ord_placeOfPoint (a : K) {f : RatFunc K} (hf : f ≠ 0) :
    (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) (X - C a)) ∣ (placeOfPoint K a).ord f
theorem

ord_placeOfPoint_X_sub_C

L400 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_X_sub_C
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem ord_placeOfPoint_X_sub_C (a : K) :
    (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) (X - C a)) = 1
theorem

ord_placeOfPoint_algebraMap

L417 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
Lean source · statement
theorem ord_placeOfPoint_algebraMap (a : K) {q : K[X]} (hq : q ≠ 0) :
    (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) q) = rootMultiplicity a q
theorem

exists_eq_placeOfPoint

L423 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.exists_eq_placeOfPoint
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem exists_eq_placeOfPoint [IsAlgClosed K] (w : HeightOneSpectrum K[X]) :
    ∃ a : K, Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w = placeOfPoint K a
theorem

eq_placeOfPoint_or_eq_placeInfty

L439 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.eq_placeOfPoint_or_eq_placeInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem eq_placeOfPoint_or_eq_placeInfty [IsAlgClosed K] [DecidableEq (RatFunc K)]
    (v : Place K (RatFunc K)) :
    (∃ a : K, v = placeOfPoint K a) ∨ v = placeInfty K
def

ofOption

L447 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ofOption
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
def ofOption [DecidableEq (RatFunc K)] : Option K → Place K (RatFunc K)
theorem

ofOption_bijective

L450 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ofOption_bijective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem ofOption_bijective [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    Function.Bijective (ofOption K)
def

placeEquivOption

L464 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeEquivOption
Documentation

The classification by base-field points, with none representing the place at infinity.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
def placeEquivOption [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    Place K (RatFunc K) ≃ Option K
theorem

placeEquivOption_symm_some

L468 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem placeEquivOption_symm_some [IsAlgClosed K] [DecidableEq (RatFunc K)] (a : K) :
    (placeEquivOption K).symm (some a) = placeOfPoint K a
theorem

placeEquivOption_symm_none

L471 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem placeEquivOption_symm_none [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    (placeEquivOption K).symm none = placeInfty K
theorem

placeEquivOption_placeOfPoint

L474 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem placeEquivOption_placeOfPoint [IsAlgClosed K] [DecidableEq (RatFunc K)] (a : K) :
    placeEquivOption K (placeOfPoint K a) = some a
theorem

placeEquivOption_placeInfty

L478 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem placeEquivOption_placeInfty [IsAlgClosed K] [DecidableEq (RatFunc K)] :
    placeEquivOption K (placeInfty K) = none
theorem

deg_eq_one_of_isAlgClosed

L482 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.deg_eq_one_of_isAlgClosed
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem deg_eq_one_of_isAlgClosed [IsAlgClosed K] (v : Place K (RatFunc K)) : v.deg = 1
theorem

algebraMap_polynomial_ne_zero

L496 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.algebraMap_polynomial_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem algebraMap_polynomial_ne_zero {q : K[X]} (hq : q ≠ 0) :
    algebraMap K[X] (RatFunc K) q ≠ 0
theorem

algebraMap_C

L500 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.algebraMap_C
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem algebraMap_C (c : K) :
    algebraMap K[X] (RatFunc K) (C c) = algebraMap K (RatFunc K) c
theorem

evalAt_placeOfPoint_algebraMap

L504 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_algebraMap
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem evalAt_placeOfPoint_algebraMap (a : K) (q : K[X]) :
    (placeOfPoint K a).evalAt (algebraMap K[X] (RatFunc K) q) = q.eval a
theorem

evalAt_placeOfPoint_X_sub_C

L526 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_X_sub_C
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
Lean source · statement
theorem evalAt_placeOfPoint_X_sub_C (a b : K) :
    (placeOfPoint K a).evalAt (algebraMap K[X] (RatFunc K) (X - C b)) = a - b
theorem

mem_placeInfty_of_intDegree_nonpos

L535 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.mem_placeInfty_of_intDegree_nonpos
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem mem_placeInfty_of_intDegree_nonpos {f : RatFunc K} (hf : f ≠ 0)
    (h : f.intDegree ≤ 0) : f ∈ (placeInfty K).toValuationSubring
theorem

evalAt_placeInfty_eq

L539 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_eq
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem evalAt_placeInfty_eq {f : RatFunc K} {c : K}
    (h : f - algebraMap K (RatFunc K) c = 0
      ∨ (f - algebraMap K (RatFunc K) c).intDegree < 0) :
    (placeInfty K).evalAt f = c
theorem

evalAt_placeInfty_X_sub_C_div

L568 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_X_sub_C_div
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem evalAt_placeInfty_X_sub_C_div (a a₀ : K) :
    (placeInfty K).evalAt
        (algebraMap K[X] (RatFunc K) (X - C a) / algebraMap K[X] (RatFunc K) (X - C a₀))
      = 1
theorem

principalDivisor_X_sub_C

L599 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor_X_sub_C
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem principalDivisor_X_sub_C (b : K) :
    principalDivisor (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero b))
      = Finsupp.single (placeOfPoint K b) 1 + Finsupp.single (placeInfty K) (-1)
theorem

ord_X_sub_C

L608 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_X_sub_C
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ord_X_sub_C (b : K) (v : Place K (RatFunc K)) :
    v.ord (algebraMap K[X] (RatFunc K) (X - C b))
      = (Finsupp.single (placeOfPoint K b) (1 : ℤ)
          + Finsupp.single (placeInfty K) (-1 : ℤ)) v
theorem

ord_X_sub_C_placeOfPoint_of_ne

L615 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeOfPoint_of_ne
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem ord_X_sub_C_placeOfPoint_of_ne {a b : K} (hab : a ≠ b) :
    (placeOfPoint K a).ord (algebraMap K[X] (RatFunc K) (X - C b)) = 0
theorem

ord_X_sub_C_placeOfPoint_self

L625 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeOfPoint_self
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem ord_X_sub_C_placeOfPoint_self (b : K) :
    (placeOfPoint K b).ord (algebraMap K[X] (RatFunc K) (X - C b)) = 1
theorem

ord_X_sub_C_placeInfty

L631 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
Lean source · statement
theorem ord_X_sub_C_placeInfty (b : K) :
    (placeInfty K).ord (algebraMap K[X] (RatFunc K) (X - C b)) = -1
theorem

isRational_placeOfPoint

L638 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.isRational_placeOfPoint
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem isRational_placeOfPoint (a : K) : (placeOfPoint K a).IsRational
theorem

principalDivisor_X_sub_C_div

L642 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor_X_sub_C_div
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem principalDivisor_X_sub_C_div (a a₀ : K) :
    principalDivisor (div_ne_zero (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero a))
        (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero a₀)))
      = Finsupp.single (placeOfPoint K a) 1 + Finsupp.single (placeOfPoint K a₀) (-1)
theorem

evalAt_placeOfPoint_X_sub_C_div

L664 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_X_sub_C_div
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section CrossRatio
variable [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem evalAt_placeOfPoint_X_sub_C_div (a a₀ : K) {b : K} (hba₀ : b ≠ a₀) :
    (placeOfPoint K b).evalAt
        (algebraMap K[X] (RatFunc K) (X - C a) / algebraMap K[X] (RatFunc K) (X - C a₀))
      = (b - a) / (b - a₀)
theorem

isRational_of_isAlgClosed

L687 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.isRational_of_isAlgClosed
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem isRational_of_isAlgClosed (v : Place K (RatFunc K)) : v.IsRational
theorem

algebraMap_const_ne_zero

L691 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.algebraMap_const_ne_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem algebraMap_const_ne_zero {c : K} (hc : c ≠ 0) : algebraMap K (RatFunc K) c ≠ 0
instance

(anonymous instance)

L694 ↗
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
Lean source · statement
instance : DecidableEq (Place K (RatFunc K))
theorem

ord_ne_zero_of_mem_support

L697 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_ne_zero_of_mem_support
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem ord_ne_zero_of_mem_support {g : RatFunc K} (hg : g ≠ 0) {v : Place K (RatFunc K)}
    (hv : v ∈ (principalDivisor hg).support) : v.ord g ≠ 0
theorem

sum_ord_eq_zero

L702 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.sum_ord_eq_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem sum_ord_eq_zero {f : RatFunc K} (hf : f ≠ 0) :
    ∑ v ∈ (principalDivisor hf).support, v.ord f = 0
theorem

zpow_sum_eq_prod

L709 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.zpow_sum_eq_prod
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem zpow_sum_eq_prod {c : K} (hc : c ≠ 0) {ι : Type*} (s : Finset ι) (n : ι → ℤ) :
    ∏ i ∈ s, c ^ n i = c ^ (∑ i ∈ s, n i)
theorem

principalDivisor_congr

L716 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.principalDivisor_congr
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem principalDivisor_congr {f g : RatFunc K} (hf : f ≠ 0) (hg : g ≠ 0) (h : f = g) :
    principalDivisor hf = principalDivisor hg
theorem

reciprocity_algebraMap_right

L722 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_algebraMap_right
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_algebraMap_right {f : RatFunc K} (hf : f ≠ 0) {c : K} (hc : c ≠ 0) :
    Divisor.evalFun f (principalDivisor (algebraMap_const_ne_zero hc))
      = Divisor.evalFun (algebraMap K (RatFunc K) c) (principalDivisor hf)
theorem

reciprocity_mul_right

L737 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_mul_right
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_mul_right {f g₁ g₂ : RatFunc K} (hf : f ≠ 0) (hg₁ : g₁ ≠ 0) (hg₂ : g₂ ≠ 0)
    (hd₁ : ∀ v : Place K (RatFunc K), v.ord f = 0 ∨ v.ord g₁ = 0)
    (hd₂ : ∀ v : Place K (RatFunc K), v.ord f = 0 ∨ v.ord g₂ = 0)
    (h₁ : Divisor.evalFun f (principalDivisor hg₁) = Divisor.evalFun g₁ (principalDivisor hf))
    (h₂ : Divisor.evalFun f (principalDivisor hg₂)
      = Divisor.evalFun g₂ (principalDivisor hf)) :
    Divisor.evalFun f (principalDivisor (mul_ne_zero hg₁ hg₂))
      = Divisor.evalFun (g₁ * g₂) (principalDivisor hf)
theorem

reciprocity_mul_left

L764 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_mul_left
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_mul_left {f₁ f₂ g : RatFunc K} (hf₁ : f₁ ≠ 0) (hf₂ : f₂ ≠ 0) (hg : g ≠ 0)
    (hd₁ : ∀ v : Place K (RatFunc K), v.ord f₁ = 0 ∨ v.ord g = 0)
    (hd₂ : ∀ v : Place K (RatFunc K), v.ord f₂ = 0 ∨ v.ord g = 0)
    (h₁ : Divisor.evalFun f₁ (principalDivisor hg) = Divisor.evalFun g (principalDivisor hf₁))
    (h₂ : Divisor.evalFun f₂ (principalDivisor hg)
      = Divisor.evalFun g (principalDivisor hf₂)) :
    Divisor.evalFun (f₁ * f₂) (principalDivisor hg)
      = Divisor.evalFun g (principalDivisor (mul_ne_zero hf₁ hf₂))
theorem

reciprocity_zpow_right

L776 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_zpow_right
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_zpow_right {f g : RatFunc K} (hf : f ≠ 0) (hg : g ≠ 0) (n : ℤ)
    (hd : ∀ v : Place K (RatFunc K), v.ord f = 0 ∨ v.ord g = 0)
    (h : Divisor.evalFun f (principalDivisor hg)
      = Divisor.evalFun g (principalDivisor hf)) :
    Divisor.evalFun f (principalDivisor (zpow_ne_zero n hg))
      = Divisor.evalFun (g ^ n) (principalDivisor hf)
theorem

reciprocity_zpow_left

L791 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_zpow_left
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_zpow_left {f g : RatFunc K} (hf : f ≠ 0) (hg : g ≠ 0) (n : ℤ)
    (hd : ∀ v : Place K (RatFunc K), v.ord f = 0 ∨ v.ord g = 0)
    (h : Divisor.evalFun f (principalDivisor hg)
      = Divisor.evalFun g (principalDivisor hf)) :
    Divisor.evalFun (f ^ n) (principalDivisor hg)
      = Divisor.evalFun g (principalDivisor (zpow_ne_zero n hf))
theorem

exists_algebraMap_of_forall_ord_eq_zero

L800 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.exists_algebraMap_of_forall_ord_eq_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem exists_algebraMap_of_forall_ord_eq_zero {g : RatFunc K} (hg : g ≠ 0)
    (h : ∀ v : Place K (RatFunc K), v.ord g = 0) :
    ∃ c : K, c ≠ 0 ∧ g = algebraMap K (RatFunc K) c
theorem

crossRatio_reciprocity

L844 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.crossRatio_reciprocity
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem crossRatio_reciprocity {a a₀ b : K} (hba : b ≠ a) (hba₀ : b ≠ a₀) :
    Divisor.evalFun
        (algebraMap K[X] (RatFunc K) (X - C a) / algebraMap K[X] (RatFunc K) (X - C a₀))
        (principalDivisor (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero b)))
      = Divisor.evalFun (algebraMap K[X] (RatFunc K) (X - C b))
        (principalDivisor (div_ne_zero (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero a))
          (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero a₀))))
theorem

reciprocity_of_forall_ord_eq_zero

L868 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_of_forall_ord_eq_zero
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [DecidableEq (RatFunc K)] in
Lean source · statement
theorem reciprocity_of_forall_ord_eq_zero {f g : RatFunc K} (hf : f ≠ 0) (hg : g ≠ 0)
    (hzero : ∀ v : Place K (RatFunc K), v.ord g = 0) :
    Divisor.evalFun f (principalDivisor hg) = Divisor.evalFun g (principalDivisor hf)
theorem

ord_div_zpow

L875 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_div_zpow
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] [DecidableEq (RatFunc K)] in
Lean source · statement
theorem ord_div_zpow (v : Place K (RatFunc K)) {g h : RatFunc K} (hg : g ≠ 0) (hh : h ≠ 0)
    (m : ℤ) : v.ord (g / h ^ m) = v.ord g - m * v.ord h
theorem

ord_X_sub_C_eq_zero_of_ne

L881 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_eq_zero_of_ne
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
omit [IsAlgClosed K] in
Lean source · statement
theorem ord_X_sub_C_eq_zero_of_ne (b : K) {v : Place K (RatFunc K)}
    (hvb : v ≠ placeOfPoint K b) (hvinf : v ≠ placeInfty K) :
    v.ord (algebraMap K[X] (RatFunc K) (X - C b)) = 0
theorem

reciprocity_linear

L887 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_linear
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
Lean source · statement
theorem reciprocity_linear (b : K) :
    ∀ (n : ℕ) (f : RatFunc K) (hf : f ≠ 0),
      (placeInfty K).ord f = 0 → (placeOfPoint K b).ord f = 0 →
      (principalDivisor hf).support.card ≤ n →
      Divisor.evalFun f
          (principalDivisor (algebraMap_polynomial_ne_zero (X_sub_C_ne_zero b)))
        = Divisor.evalFun (algebraMap K[X] (RatFunc K) (X - C b)) (principalDivisor hf)
theorem

reciprocity_of_ord_placeInfty_eq_zero

L1091 ↗
AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField.reciprocity_of_ord_placeInfty_eq_zero
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
open _root_.AlgebraicCurve.RationalFunctionField
variable {K : Type*} [Field K]
section Reciprocity
variable [IsAlgClosed K] [DecidableEq (RatFunc K)]
local instance : DecidableEq (Place K (RatFunc K)) := Classical.decEq _
Lean source · statement
theorem reciprocity_of_ord_placeInfty_eq_zero :
    ∀ (n : ℕ) (f g : RatFunc K) (hf : f ≠ 0) (hg : g ≠ 0),
      (placeInfty K).ord f = 0 →
      (∀ v : Place K (RatFunc K), v.ord f = 0 ∨ v.ord g = 0) →
      ((principalDivisor hg).support.erase (placeInfty K)).card ≤ n →
      Divisor.evalFun f (principalDivisor hg) = Divisor.evalFun g (principalDivisor hf)
theorem

exists_algebraMap_of_forall_ord_eq_zero

L1233 ↗
AlgebraicCurve.RationalFunctionField.exists_algebraMap_of_forall_ord_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs
namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
open Polynomial _root_.AlgebraicCurve in
with_weak_namespace _root_.AlgebraicCurves.Places.Rational.Proofs
open RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve in
open _root_.AlgebraicCurve.RationalFunctionField in
open
  RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero.AlgebraicCurve.RationalFunctionField
in
with_weak_namespace RationalFunctionField_exists_algebraMap_of_forall_ord_eq_zero
with_weak_namespace AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.RationalFunctionField.exists_algebraMap_of_forall_ord_eq_zero {K :
  Type*} [Field K] {g : RatFunc K} (hg : g ≠ 0) (h : ∀ v : Place K (RatFunc K), v.ord g = 0) :
  ∃ c : K, c ≠ 0 ∧ g = algebraMap K (RatFunc K) c

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