NYLL
Module

IsCurveOver_ratFunc.lean

Nyll.AlgebraicCurves.FunctionFields.IsCurveOver_ratFunc
40 declarations indexed from sourceView source ↗

Module documentation

Is Curve Over rat Func

Imports5
Imported by19

Declarations

theorem

inftyValuation_isEquiv_adicValuation

L47 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.inftyValuation_isEquiv_adicValuation
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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

subsingleton_setOf_forall_ne_ofHeightOneSpectrum

L55 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.subsingleton_setOf_forall_ne_ofHeightOneSpectrum
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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 subsingleton_setOf_forall_ne_ofHeightOneSpectrum :
    {v : Place K (RatFunc K) |
      ∀ w : HeightOneSpectrum K[X], v ≠ Place.ofHeightOneSpectrum w}.Subsingleton
theorem

finite_setOf_valuation_ne_one

L66 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.finite_setOf_valuation_ne_one
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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 finite_setOf_valuation_ne_one {f : RatFunc K} (hf : f ≠ 0) :
    {w : HeightOneSpectrum K[X] | w.valuation (RatFunc K) f ≠ 1}.Finite
theorem

finite_setOf_ord_ne_zero

L85 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.finite_setOf_ord_ne_zero
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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 finite_setOf_ord_ne_zero {f : RatFunc K} (hf : f ≠ 0) :
    {v : Place K (RatFunc K) | v.ord f ≠ 0}.Finite
theorem

finite_support_ord

L103 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.finite_support_ord
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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 finite_support_ord {f : RatFunc K} (hf : f ≠ 0) :
    {v : Place K (RatFunc K) | v.ord f ≠ 0}.Finite
theorem

exists_sub_algebraMap_intDegree_neg

L111 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.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.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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

L160 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.deg_placeInfty
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open 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

L200 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.le_exp_neg_one_of_lt_one
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L214 ↗
AlgebraicCurve.Place.isUnit_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L220 ↗
AlgebraicCurve.Place.adicValuation_algebraMap
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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 _root_.AlgebraicCurve.Place.adicValuation_algebraMap {c : K} (hc : c ≠ 0) :
    v.adicValuation (algebraMap K F c) = 1
theorem

ord_algebraMap

L227 ↗
AlgebraicCurve.Place.ord_algebraMap
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_algebraMap (c : K) : v.ord (algebraMap K F c) = 0
theorem

ord_eq_neg_log_of_valuationSubring_eq

L235 ↗
AlgebraicCurve.Place.ord_eq_neg_log_of_valuationSubring_eq
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_eq_neg_log_of_valuationSubring_eq (w : Valuation F
  ℤᵐ⁰)
    (hw : w.valuationSubring = v.toValuationSubring) {π : F} (hπ : w π = exp (-1 : ℤ))
    {f : F} (hf : f ≠ 0) : v.ord f = -log (w f)
theorem

ord_ofHeightOneSpectrum_eq_neg_log

L272 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_neg_log
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_neg_log (w : HeightOneSpectrum K[X]) {p : K[X]}
    (hp : p ≠ 0) (hw : w.asIdeal = Ideal.span {p}) {f : RatFunc K} (hf : f ≠ 0) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ord f
      = -log (w.valuation (RatFunc K) f)
theorem

ord_ofHeightOneSpectrum_of_span

L283 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_of_span
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_of_span (w : HeightOneSpectrum K[X]) {p : K[X]}
    (hp : p ≠ 0) (hw : w.asIdeal = Ideal.span {p}) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).ord
      (algebraMap K[X] (RatFunc K) p) = 1
theorem

ord_ofHeightOneSpectrum_eq_zero_of_notMem

L294 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.ord_ofHeightOneSpectrum_eq_zero_of_notMem
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L306 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.ord_placeInfty
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L315 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.ord_placeInfty_algebraMap
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L325 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.single_add_single_apply_eq_ord
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L354 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.degree_single_add_single
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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
theorem

degree_eq_zero_of_forall_eq_ord_algebraMap

L363 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord_algebraMap
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_eq_zero_of_forall_eq_ord_algebraMap (q : K[X]) :
    ∀ D : Divisor K (RatFunc K),
      (∀ v : Place K (RatFunc K), D v = v.ord (algebraMap K[X] (RatFunc K) q)) →
      Divisor.degree D = 0
def

principalDivisor

L404 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.principalDivisor
Documentation

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

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L408 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.principalDivisor_apply
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L411 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.principalDivisor_isPrincipal
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_eq_zero_of_forall_eq_ord

L415 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_forall_eq_ord
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_eq_zero_of_forall_eq_ord {f : RatFunc K} (D : Divisor K (RatFunc K))
    (hD : ∀ v : Place K (RatFunc K), D v = v.ord f) : Divisor.degree D = 0
theorem

degree_principalDivisor

L441 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.degree_principalDivisor
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

L445 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.sum_ord_mul_deg_eq_zero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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

degree_eq_zero_of_isPrincipal

L455 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.degree_eq_zero_of_isPrincipal
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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_eq_zero_of_isPrincipal {D : Divisor K (RatFunc K)} (hD : D.IsPrincipal) :
    Divisor.degree D = 0
theorem

principal_le_degZero

L460 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.principal_le_degZero
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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 principal_le_degZero :
    Divisor.principal (K := K) (F := RatFunc K) ≤ Divisor.degZero (K := K) (F := RatFunc K)
instance

instHasPrincipalDivisors

L464 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instHasPrincipalDivisors
Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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 · full declaration
instance instHasPrincipalDivisors : HasPrincipalDivisors K (RatFunc K) where
  exists_divisor _ hf := ⟨principalDivisor hf, fun _ => rfl, degree_principalDivisor hf⟩
theorem

finiteResidue_of_deg_pos

L486 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.Place.finiteResidue_of_deg_pos
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section DegPos
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem finiteResidue_of_deg_pos (h : 0 < v.deg) : v.FiniteResidue
theorem

deg_pos

L489 ↗
AlgebraicCurve.Place.deg_pos
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section DegPos
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.deg_pos [v.FiniteResidue] : 0 < v.deg
theorem

deg_ne_zero

L495 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.Place.deg_ne_zero
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
section DegPos
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem deg_ne_zero [v.FiniteResidue] : v.deg ≠ 0
instance

instFiniteResidueOfHeightOneSpectrum

L508 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResidueOfHeightOneSpectrum
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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
instance instFiniteResidueOfHeightOneSpectrum (w : HeightOneSpectrum K[X]) :
    (Place.ofHeightOneSpectrum (K := K) (F := RatFunc K) w).FiniteResidue
instance

instFiniteResiduePlaceInfty

L515 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResiduePlaceInfty
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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
instance instFiniteResiduePlaceInfty [DecidableEq (RatFunc K)] :
    (placeInfty K).FiniteResidue
instance

instFiniteResidue

L520 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.RationalFunctionField.instFiniteResidue
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open 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} in
Lean source · statement
instance instFiniteResidue (v : Place K (RatFunc K)) : v.FiniteResidue
def

kaehlerPolynomialBasis

L541 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.kaehlerPolynomialBasis
Documentation

The basis of polynomial differentials given by the differential of the variable.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
section Kaehler
open Polynomial TensorProduct Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
def kaehlerPolynomialBasis : Basis Unit K[X] Ω[K[X]⁄K]
instance

instFormallyEtalePolynomialRatFunc

L544 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.instFormallyEtalePolynomialRatFunc
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
section Kaehler
open Polynomial TensorProduct Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
instance instFormallyEtalePolynomialRatFunc : Algebra.FormallyEtale K[X] (RatFunc K)
def

kaehlerRatFuncBasis

L548 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.kaehlerRatFuncBasis
Documentation

The differential basis transported from polynomials to the rational function field.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
section Kaehler
open Polynomial TensorProduct Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
def kaehlerRatFuncBasis : Basis Unit (RatFunc K) Ω[(RatFunc K)⁄K]
theorem

kaehler_free_rank_one_ratFunc

L552 ↗
AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve.kaehler_free_rank_one_ratFunc
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
noncomputable section
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
open IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
section Kaehler
open Polynomial TensorProduct Module
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
variable (K : Type*) [Field K]
Lean source · statement
theorem kaehler_free_rank_one_ratFunc :
    Module.Free (RatFunc K) Ω[(RatFunc K)⁄K] ∧ Module.finrank (RatFunc K) Ω[(RatFunc K)⁄K] = 1
theorem

isCurveOver_ratFunc

L565 ↗
AlgebraicCurve.isCurveOver_ratFunc
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.FunctionFields.Proofs.IsCurveOverRatFunc.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.isCurveOver_ratFunc (K : Type*) [Field K] : IsCurveOver K (RatFunc
  K)

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