NYLL
Module

Classification.lean

Nyll.AlgebraicCurves.Places.Rational.Classification
13 declarations indexed from sourceView source ↗

Module documentation

Classification

Places of a rational function field over an algebraically closed field are classified by finite points and the place at infinity.

Imports3
Imported by34

Declarations

instance

instNontrivialInftyValueGroup

L39 ↗
AlgebraicCurve.RationalFunctionField.instNontrivialInftyValueGroup
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
section PlaceInfty
variable [DecidableEq (RatFunc K)]
Lean source · statement
instance instNontrivialInftyValueGroup :
    Nontrivial (MonoidWithZeroHom.valueGroup (MonoidWithZeroHom.ofClass
      (RatFunc.inftyValuation K)))
theorem

placeInfty_ne_ofHeightOneSpectrum

L49 ↗
AlgebraicCurve.RationalFunctionField.placeInfty_ne_ofHeightOneSpectrum
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L62 ↗
AlgebraicCurve.RationalFunctionField.eq_ofHeightOneSpectrum_or_eq_placeInfty
Source context 7 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

placeOfPoint_ne_placeInfty

L74 ↗
AlgebraicCurve.RationalFunctionField.placeOfPoint_ne_placeInfty
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace RationalFunctionField
variable (K : Type*) [Field K]
variable {K}
variable (K)
Lean source · statement
theorem placeOfPoint_ne_placeInfty [DecidableEq (RatFunc K)] (a : K) :
    placeOfPoint K a ≠ placeInfty K
theorem

exists_eq_placeOfPoint

L79 ↗
AlgebraicCurve.RationalFunctionField.exists_eq_placeOfPoint
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L94 ↗
AlgebraicCurve.RationalFunctionField.eq_placeOfPoint_or_eq_placeInfty
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L102 ↗
AlgebraicCurve.RationalFunctionField.ofOption
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L105 ↗
AlgebraicCurve.RationalFunctionField.ofOption_bijective
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L119 ↗
AlgebraicCurve.RationalFunctionField.placeEquivOption
Documentation

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

Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L123 ↗
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_some
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L126 ↗
AlgebraicCurve.RationalFunctionField.placeEquivOption_symm_none
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L129 ↗
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeOfPoint
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

L133 ↗
AlgebraicCurve.RationalFunctionField.placeEquivOption_placeInfty
Source context 8 commands

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

noncomputable section
open Polynomial IsDedekindDomain WithZero IsLocalRing
open scoped Polynomial
namespace AlgebraicCurve
namespace 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

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