mathlib documentation

ideles / function_field

The valuation at infinity on k(t) #

For a field k, the valuation at infinity on the function field k(t) is the nonarchimedean valuation on k(t) with uniformizer 1/t. Explicitly, if f/g ∈ k(t) is a nonzero quotient of polynomials, its valuation at infinity is multiplicative.of_add(degree(f) - degree(g)).

Main definitions #

infty_valuation : The valuation at infinity on k(t).
kt_infty : The completion k((t⁻¹)) of k(t) with respect to infty_valuation.

Implementation notes #

The code in this file has already been incorporated to mathlib and can be found in the file number_theory/function_field.lean. Note that kt_infty is called Fqt_infty there for consistency with the file's notation, and that some of the names of definitions and lemmas have been modified. We keep this version of the code here so that this branch is a complete reference for the article "Formalizing the Rings of Adèles of a Global Field".

Tags #

function field, valuation

noncomputable def infty_valuation_def (k : Type) [field k] (r : ratfunc k) :

with_zero (multiplicative ℤ)

The valuation at infinity is the nonarchimedean valuation on k(t) with uniformizer 1/t.

Equations

infty_valuation_def k r = ite (r = 0) 0 ↑(⇑multiplicative.of_add (↑(r.num.nat_degree) - ↑(r.denom.nat_degree)))

theorem infty_valuation.map_zero' (k : Type) [field k] :

infty_valuation_def k 0 = 0

theorem infty_valuation.map_one' (k : Type) [field k] :

infty_valuation_def k 1 = 1

theorem infty_valuation.map_mul' (k : Type) [field k] (x y : ratfunc k) :

infty_valuation_def k (x * y) = (infty_valuation_def k x) * infty_valuation_def k y

theorem infty_valuation_well_defined {k : Type} [field k] {r₁ r₂ s₁ s₂ : k[X]} (hr₁ : r₁ ≠ 0) (hs₁ : s₁ ≠ 0) (hr₂ : r₂ ≠ 0) (hs₂ : s₂ ≠ 0) (h_eq : r₁ * s₂ = r₂ * s₁) :

↑(r₁.nat_degree) - ↑(s₁.nat_degree) = ↑(r₂.nat_degree) - ↑(s₂.nat_degree)

Equivalent fractions have the same valuation

theorem ratfunc.num_add_ne_zero {k : Type} [field k] {x y : ratfunc k} (hxy : x + y ≠ 0) :

(x.num) * y.denom + (x.denom) * y.num ≠ 0

theorem infty_valuation_add_rw {k : Type} [field k] {x y : ratfunc k} (hxy : x + y ≠ 0) :

↑((x + y).num.nat_degree) - ↑((x + y).denom.nat_degree) = ↑(((x.num) * y.denom + (x.denom) * y.num).nat_degree) - ↑(((x.denom) * y.denom).nat_degree)

theorem infty_valuation_rw {k : Type} [field k] {x : ratfunc k} (hx : x ≠ 0) {s : k[X]} (hs : s ≠ 0) :

↑(x.num.nat_degree) - ↑(x.denom.nat_degree) = ↑(((x.num) * s).nat_degree) - ↑((s * x.denom).nat_degree)

theorem infty_valuation.map_add' (k : Type) [field k] (x y : ratfunc k) :

infty_valuation_def k (x + y) ≤ max (infty_valuation_def k x) (infty_valuation_def k y)

noncomputable def infty_valuation (k : Type) [field k] :

valuation (ratfunc k) (with_zero (multiplicative ℤ))

The valuation at infinity on k(t).

Equations

infty_valuation k = {to_monoid_with_zero_hom := {to_fun := infty_valuation_def k _inst_1, map_zero' := _, map_one' := _, map_mul' := _}, map_add_le_max' := _}

noncomputable def infty_valued_kt (k : Type) [field k] :

valued (ratfunc k) (with_zero (multiplicative ℤ))

The valued field k(t) with the valuation at infinity.

Equations

infty_valued_kt k = {v := infty_valuation k _inst_1}

theorem infty_valued_kt.def (k : Type) [field k] {x : ratfunc k} :

⇑valued.v x = infty_valuation_def k x

noncomputable def tsq' (k : Type) [field k] :

topological_space (ratfunc k)

The topology structure on k(t) induced by the valuation at infinity.

Equations

tsq' k = valued.topological_space (with_zero (multiplicative ℤ))

theorem tdrq' (k : Type) [field k] :

topological_division_ring (ratfunc k)

theorem trq' (k : Type) [field k] :

topological_ring (ratfunc k)

theorem tgq' (k : Type) [field k] :

topological_add_group (ratfunc k)

noncomputable def usq' (k : Type) [field k] :

uniform_space (ratfunc k)

The uniform structure on k(t) induced by the valuation at infinity.

Equations

usq' k = topological_add_group.to_uniform_space (ratfunc k)

theorem ugq' (k : Type) [field k] :

uniform_add_group (ratfunc k)

theorem cfq' (k : Type) [field k] :

completable_top_field (ratfunc k)

theorem ssq' (k : Type) [field k] :

separated_space (ratfunc k)

def kt_infty (k : Type) [field k] :

Type

The completion k((t⁻¹)) of k(t) with respect to the valuation at infinity.

Equations

kt_infty k = uniform_space.completion (ratfunc k)

@[protected, instance]

noncomputable def kt_infty.field (k : Type) [field k] :

field (kt_infty k)

Equations

kt_infty.field k = field_completion

@[protected, instance]

noncomputable def valued_kt_infty (k : Type) [field k] :

valued (kt_infty k) (with_zero (multiplicative ℤ))

The valuation at infinity on k(t) extends to a valuation on kt_infty.

Equations

valued_kt_infty k = {v := valued.extension_valuation (infty_valued_kt k)}

theorem valued_kt_infty.def (k : Type) [field k] {x : kt_infty k} :

⇑valued.v x = valued.extension x

@[protected, instance]

noncomputable def tsq (k : Type) [field k] :

topological_space (kt_infty k)

Equations

tsq k = valued.topological_space (with_zero (multiplicative ℤ))

@[protected, instance]

def tdrq (k : Type) [field k] :

topological_division_ring (kt_infty k)

@[protected, instance]

def trq (k : Type) [field k] :

topological_ring (kt_infty k)

@[protected, instance]

def tgq (k : Type) [field k] :

topological_add_group (kt_infty k)

@[protected, instance]

noncomputable def usq (k : Type) [field k] :

uniform_space (kt_infty k)

Equations

usq k = topological_add_group.to_uniform_space (kt_infty k)

@[protected, instance]

def ugq (k : Type) [field k] :

uniform_add_group (kt_infty k)

@[protected, instance]

noncomputable def kt_infty.inhabited (k : Type) [field k] :

inhabited (kt_infty k)

Equations

kt_infty.inhabited k = {default := 0}