Module

Value.lean

Nyll.AlgebraicCurves.Places.Value

15 declarations indexed from sourceView source ↗

Module documentation

Value

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by24

theorem

residue_algebraMap

L30 ↗

AlgebraicCurve.Place.residue_algebraMap

Source context 5 commands

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

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

Lean source · statement

theorem residue_algebraMap (c : K) :
    residue v.toValuationSubring (algebraMap K v.toValuationSubring c)
      = algebraMap K v.ResidueField c

def

HasValue

L37 ↗

AlgebraicCurve.Place.HasValue

Documentation

The function is integral at the place and its residue is the specified base-field value.

Source context 5 commands

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

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

Lean source · statement

def HasValue (g : F) (a : K) : Prop

theorem

hasValue_iff

L41 ↗

AlgebraicCurve.Place.hasValue_iff

Source context 5 commands

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

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

Lean source · statement

theorem hasValue_iff (g : F) (a : K) :
    v.HasValue g a ↔ ∃ h : g ∈ v.toValuationSubring,
      residue v.toValuationSubring ⟨g, h⟩ = algebraMap K v.ResidueField a

theorem

mem

L48 ↗

AlgebraicCurve.Place.HasValue.mem

Source context 6 commands

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

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

Lean source · statement

theorem HasValue.mem {g : F} {a : K} (h : v.HasValue g a) : g ∈ v.toValuationSubring

theorem

residue_eq

L51 ↗

AlgebraicCurve.Place.HasValue.residue_eq

Source context 6 commands

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

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

Lean source · statement

theorem HasValue.residue_eq {g : F} {a : K} (h : v.HasValue g a) :
    residue v.toValuationSubring ⟨g, h.mem⟩ = algebraMap K v.ResidueField a

theorem

hasValue_one

L56 ↗

AlgebraicCurve.Place.hasValue_one

Source context 7 commands

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

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

Lean source · statement

theorem hasValue_one : v.HasValue (1 : F) 1

theorem

hasValue_algebraMap

L60 ↗

AlgebraicCurve.Place.hasValue_algebraMap

Source context 8 commands

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

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

Lean source · statement

theorem hasValue_algebraMap (c : K) : v.HasValue (algebraMap K F c) c

theorem

mul

L63 ↗

AlgebraicCurve.Place.HasValue.mul

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.mul {g g' : F} {a a' : K} (h : v.HasValue g a) (h' : v.HasValue g' a') :
    v.HasValue (g * g') (a * a')

theorem

isUnit

L71 ↗

AlgebraicCurve.Place.HasValue.isUnit

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.isUnit {g : F} {a : K} (h : v.HasValue g a) (ha : a ≠ 0) :
    IsUnit (⟨g, h.mem⟩ : v.toValuationSubring)

theorem

ne_zero

L76 ↗

AlgebraicCurve.Place.HasValue.ne_zero

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.ne_zero {g : F} {a : K} (h : v.HasValue g a) (ha : a ≠ 0) : g ≠ 0

theorem

inv

L81 ↗

AlgebraicCurve.Place.HasValue.inv

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.inv {g : F} {a : K} (h : v.HasValue g a) (ha : a ≠ 0) :
    v.HasValue g⁻¹ a⁻¹

theorem

unique

L97 ↗

AlgebraicCurve.Place.HasValue.unique

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.unique {g : F} {a a' : K} (h : v.HasValue g a) (h' : v.HasValue g a') :
    a = a'

theorem

ord_eq_zero

L101 ↗

AlgebraicCurve.Place.HasValue.ord_eq_zero

Source context 8 commands

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

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

Lean source · statement

theorem HasValue.ord_eq_zero {g : F} {a : K} (h : v.HasValue g a) (ha : a ≠ 0) : v.ord g = 0

theorem

exists_isUnit_of_ord_eq_zero

L106 ↗

AlgebraicCurve.Place.exists_isUnit_of_ord_eq_zero

Source context 9 commands

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

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

Lean source · statement

theorem exists_isUnit_of_ord_eq_zero {f : F} (hf : f ≠ 0) (h : v.ord f = 0) :
    ∃ hm : f ∈ v.toValuationSubring, IsUnit (⟨f, hm⟩ : v.toValuationSubring)

theorem

exists_hasValue_of_surjective

L115 ↗

AlgebraicCurve.Place.exists_hasValue_of_surjective

Source context 10 commands

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

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

Lean source · statement

theorem exists_hasValue_of_surjective (hv : Function.Surjective (algebraMap K v.ResidueField))
    {g : F} (hg : g ∈ v.toValuationSubring) :
    ∃ a : K, v.HasValue g a ∧ (IsUnit (⟨g, hg⟩ : v.toValuationSubring) → a ≠ 0)

Module documentation

Value

Declarations