Module

EvaluationAlgebra.lean

Nyll.AlgebraicCurves.Places.EvaluationAlgebra

16 declarations indexed from sourceView source ↗

Module documentation

Evaluation Algebra

Imports1

Nyll.AlgebraicCurves.Places.Evaluation

Imported by40

theorem

mem_toValuationSubring_of_ord_nonneg_alt

L31 ↗

AlgebraicCurve.Place.mem_toValuationSubring_of_ord_nonneg_alt

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem mem_toValuationSubring_of_ord_nonneg_alt {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

isUnit_mk_of_ord_eq_zero

L39 ↗

AlgebraicCurve.Place.isUnit_mk_of_ord_eq_zero

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem isUnit_mk_of_ord_eq_zero {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
    IsUnit (⟨f, v.mem_toValuationSubring_of_ord_nonneg_alt hf h.ge⟩ : v.toValuationSubring)

theorem

residue_ne_zero_of_ord_eq_zero

L49 ↗

AlgebraicCurve.Place.residue_ne_zero_of_ord_eq_zero

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem residue_ne_zero_of_ord_eq_zero {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
    residue v.toValuationSubring (⟨f, v.mem_toValuationSubring_of_ord_nonneg_alt hf h.ge⟩ :
      v.toValuationSubring)
      ≠ 0

theorem

evalAt_ne_zero_of_ord_eq_zero

L55 ↗

AlgebraicCurve.Place.evalAt_ne_zero_of_ord_eq_zero

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem evalAt_ne_zero_of_ord_eq_zero (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
    v.evalAt f ≠ 0

theorem

evalAt_mul_of_mem

L62 ↗

AlgebraicCurve.Place.evalAt_mul_of_mem

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem evalAt_mul_of_mem (hv : v.IsRational) {f g : F} (hf : f ∈ v.toValuationSubring)
    (hg : g ∈ v.toValuationSubring) :
    v.evalAt (f * g) = v.evalAt f * v.evalAt g

theorem

evalAt_inv

L70 ↗

AlgebraicCurve.Place.evalAt_inv

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem evalAt_inv (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
    v.evalAt f⁻¹ = (v.evalAt f)⁻¹

theorem

evalAt_zpow

L79 ↗

AlgebraicCurve.Place.evalAt_zpow

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem evalAt_zpow (hv : v.IsRational) {f : F} (hf : f ≠ 0) (h : v.ord f = 0) (n : ℤ) :
    v.evalAt (f ^ n) = v.evalAt f ^ n

theorem

evalAt_algebraMap_eq

L100 ↗

AlgebraicCurve.Place.evalAt_algebraMap_eq

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem evalAt_algebraMap_eq (a : K) : v.evalAt (algebraMap K F a) = a

theorem

deg_eq_one_of_isRational

L108 ↗

AlgebraicCurve.Place.deg_eq_one_of_isRational

Source context 6 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem deg_eq_one_of_isRational {v : Place K F} (hv : v.IsRational) : v.deg = 1

theorem

evalFun_ne_zero

L121 ↗

AlgebraicCurve.Divisor.evalFun_ne_zero

Documentation

A divisor evaluation is nonzero when every factor indexed by its support is nonzero.

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_ne_zero {f : F} {D : Divisor K F}
    (h : ∀ v ∈ D.support, Place.evalAt v f ≠ 0) :
    evalFun f D ≠ 0

theorem

evalFun_add_of_forall_ne_zero

L127 ↗

AlgebraicCurve.Divisor.evalFun_add_of_forall_ne_zero

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_add_of_forall_ne_zero (f : F) {D E : Divisor K F}
    (hD : ∀ v ∈ D.support, Place.evalAt v f ≠ 0)
    (hE : ∀ v ∈ E.support, Place.evalAt v f ≠ 0) :
    evalFun f (D + E) = evalFun f D * evalFun f E

theorem

evalFun_mul_of_forall_mem

L138 ↗

AlgebraicCurve.Divisor.evalFun_mul_of_forall_mem

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_mul_of_forall_mem {f g : F} {D : Divisor K F}
    (hrat : ∀ v ∈ D.support, Place.IsRational v)
    (hf : ∀ v ∈ D.support, f ∈ v.toValuationSubring)
    (hg : ∀ v ∈ D.support, g ∈ v.toValuationSubring) :
    evalFun (f * g) D = evalFun f D * evalFun g D

theorem

support_smul_subset

L148 ↗

AlgebraicCurve.Divisor.support_smul_subset

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem support_smul_subset (n : ℤ) (D : Divisor K F) :
    (n • D).support ⊆ D.support

theorem

evalFun_natCast_smul_divisor

L151 ↗

AlgebraicCurve.Divisor.evalFun_natCast_smul_divisor

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_natCast_smul_divisor (f : F) (D : Divisor K F) (n : ℕ) :
    evalFun f ((n : ℤ) • D) = evalFun f D ^ n

theorem

evalFun_zsmul_divisor

L161 ↗

AlgebraicCurve.Divisor.evalFun_zsmul_divisor

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_zsmul_divisor (f : F) (D : Divisor K F) (n : ℤ) :
    evalFun f (n • D) = evalFun f D ^ n

theorem

evalFun_zpow_left_of_ord_eq_zero

L169 ↗

AlgebraicCurve.Divisor.evalFun_zpow_left_of_ord_eq_zero

Source context 5 commands

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

noncomputable section
open IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Divisor

Lean source · statement

theorem evalFun_zpow_left_of_ord_eq_zero {f : F} (hf : f ≠ 0) {D : Divisor K F} (n : ℤ)
    (hrat : ∀ v ∈ D.support, Place.IsRational v)
    (hord : ∀ v ∈ D.support, Place.ord v f = 0) :
    evalFun (f ^ n) D = evalFun f D ^ n

Module documentation

Evaluation Algebra

Declarations