Module

RationalFunctionField_evalAt_placeInfty_eq.lean

Nyll.AlgebraicCurves.Places.Rational.RationalFunctionField_evalAt_placeInfty_eq

72 declarations indexed from sourceView source ↗

Module documentation

Rational Function Field eval At place Infty eq

Imports29

Imported by1

Nyll.AlgebraicCurves.Places.Rational.All

instance

(anonymous instance)

L61 ↗

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L70 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.Place.isRational_of_deg_eq_one

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L73 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.Place.deg_eq_one_of_isRational

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L84 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_finitePlace_ne_zero_iff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L93 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.inftyValuation_isEquiv_adicValuation

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L97 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeInfty_ne_ofHeightOneSpectrum

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L110 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.eq_ofHeightOneSpectrum_or_eq_placeInfty

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L124 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.exists_sub_algebraMap_intDegree_neg

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L173 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.deg_placeInfty

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L204 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.le_exp_neg_one_of_lt_one

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L218 ↗

AlgebraicCurve.Place.isUnit_algebraMap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L224 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.Place.adicValuation_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L237 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_zero_of_notMem

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L249 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_placeInfty

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L258 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_placeInfty_algebraMap

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L268 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.single_add_single_apply_eq_ord

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L297 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.degree_single_add_single

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L308 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor

Documentation

The divisor of a nonzero rational function, with coefficients given by its orders at the places.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L312 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor_apply

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L315 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor_isPrincipal

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L319 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.degree_principalDivisor

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L323 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.sum_ord_mul_deg_eq_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L341 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeOfPoint_ne_placeInfty

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L348 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_algebraMap_eq_mul

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L382 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.dvd_ord_placeOfPoint

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L396 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_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.RationalFunctionField_evalAt_placeInfty_eq
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

L413 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_placeOfPoint_algebraMap

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L419 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.exists_eq_placeOfPoint

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L435 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.eq_placeOfPoint_or_eq_placeInfty

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L443 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ofOption

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L446 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ofOption_bijective

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L460 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeEquivOption

Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L464 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L467 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L470 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L474 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L478 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.deg_eq_one_of_isAlgClosed

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L492 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.algebraMap_polynomial_ne_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L496 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.algebraMap_C

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L500 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_algebraMap

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L522 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_X_sub_C

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L531 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.mem_placeInfty_of_intDegree_nonpos

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L535 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_eq

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L564 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_X_sub_C_div

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L595 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor_X_sub_C

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L604 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_X_sub_C

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L611 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeOfPoint_of_ne

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L621 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeOfPoint_self

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L627 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_placeInfty

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L633 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.isRational_placeOfPoint

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L637 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor_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.RationalFunctionField_evalAt_placeInfty_eq
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

L659 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.evalAt_placeOfPoint_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.RationalFunctionField_evalAt_placeInfty_eq
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

L682 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.isRational_of_isAlgClosed

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L685 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.algebraMap_const_ne_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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)

L688 ↗

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L691 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_ne_zero_of_mem_support

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L695 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.sum_ord_eq_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L701 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.zpow_sum_eq_prod

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L707 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.principalDivisor_congr

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L712 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_algebraMap_right

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L726 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_mul_right

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L752 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_mul_left

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L763 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_zpow_right

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L777 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_zpow_left

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L785 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.exists_algebraMap_of_forall_ord_eq_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L829 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.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.RationalFunctionField_evalAt_placeInfty_eq
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
omit [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

L852 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_of_forall_ord_eq_zero

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L858 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_div_zpow

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L863 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.ord_X_sub_C_eq_zero_of_ne

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L869 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_linear

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

L1073 ↗

AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField.reciprocity_of_ord_placeInfty_eq_zero

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
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

evalAt_placeInfty_eq

L1210 ↗

AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Rational.Proofs.RationalFunctionField_evalAt_placeInfty_eq
open Polynomial _root_.AlgebraicCurve AlgebraicCurve _root_.AlgebraicCurve.RationalFunctionField
  AlgebraicCurve.RationalFunctionField in
open RationalFunctionField_evalAt_placeInfty_eq.AlgebraicCurve.RationalFunctionField
  renaming evalAt_placeInfty_eq → evalAtPlaceInftyProof in

Lean source · statement

theorem _root_.AlgebraicCurve.RationalFunctionField.evalAt_placeInfty_eq (K : Type*) [Field K]
  [DecidableEq (RatFunc K)] {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

Module documentation

Rational Function Field eval At place Infty eq

Declarations