Valuations on F(t)

This file defines the valuation at infinity on the field of rational functions F(t).

Main definitions

• RatFunc.inftyValuation : The place at infinity on F(t) is the nonarchimedean valuation on F(t) with uniformizer 1/t.
• RatFunc.CompletionAtInfty : The completion F((t⁻¹)) of F(t) with respect to the valuation at infinity.

References

• D. Marcus, Number Fields
• J.W.S. Cassels, A. Fröhlich, Algebraic Number Theory
• P. Samuel, Algebraic Theory of Numbers

Tags

function field, ring of integers

The place at infinity on F(t)

noncomputable def RatFunc.inftyValuationDef (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (r : RatFunc F) : WithZero (Multiplicative ℤ)

The valuation at infinity is the nonarchimedean valuation on F(t) with uniformizer 1/t. Explicitly, if f/g ∈ F(t) is a nonzero quotient of polynomials, its valuation at infinity is exp (degree(f) - degree(g)).

Equations

• RatFunc.inftyValuationDef F r = if r = 0 then 0 else WithZero.exp r.intDegree

theorem RatFunc.InftyValuation.map_zero' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : inftyValuationDef F 0 = 0

theorem RatFunc.InftyValuation.map_one' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : inftyValuationDef F 1 = 1

theorem RatFunc.InftyValuation.map_mul' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (x y : RatFunc F) : inftyValuationDef F (x * y) = inftyValuationDef F x * inftyValuationDef F y

theorem RatFunc.InftyValuation.map_add_le_max' (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (x y : RatFunc F) : inftyValuationDef F (x + y) ≤ max (inftyValuationDef F x) (inftyValuationDef F y)

@[simp]

theorem RatFunc.inftyValuation_of_nonzero (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} (hx : x ≠ 0) : inftyValuationDef F x = WithZero.exp x.intDegree

noncomputable def RatFunc.inftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valuation (RatFunc F) (WithZero (Multiplicative ℤ))

The valuation at infinity on F(t).

Equations

• RatFunc.inftyValuation F = { toFun := RatFunc.inftyValuationDef F, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

theorem RatFunc.inftyValuation_apply (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} : (inftyValuation F) x = inftyValuationDef F x

@[simp]

theorem RatFunc.inftyValuation.C (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {k : F} (hk : k ≠ 0) : (inftyValuation F) (RatFunc.C k) = 1

@[simp]

theorem RatFunc.inftyValuation.X (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : (inftyValuation F) RatFunc.X = WithZero.exp 1

theorem RatFunc.inftyValuation.X_zpow (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] (m : ℤ) : (inftyValuation F) (RatFunc.X ^ m) = WithZero.exp m

theorem RatFunc.inftyValuation.X_inv (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : (inftyValuation F) (1 / RatFunc.X) = WithZero.exp (-1)

theorem RatFunc.inftyValuation.polynomial (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {p : Polynomial F} (hp : p ≠ 0) : inftyValuationDef F ((algebraMap (Polynomial F) (RatFunc F)) p) = WithZero.exp ↑p.natDegree

instance RatFunc.instIsNontrivialWithZeroMultiplicativeIntInftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : (inftyValuation F).IsNontrivial

instance RatFunc.instIsTrivialOnWithZeroMultiplicativeIntInftyValuation (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valuation.IsTrivialOn F (inftyValuation F)

@[instance_reducible]

noncomputable def RatFunc.inftyValued (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valued (RatFunc F) (WithZero (Multiplicative ℤ))

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

Equations

• RatFunc.inftyValued F = Valued.mk' (RatFunc.inftyValuation F)

theorem RatFunc.inftyValued.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : RatFunc F} : Valued.v x = inftyValuationDef F x

@[instance_reducible]

noncomputable def RatFunc.CompletionAtInfty.instUniformSpace (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : UniformSpace (RatFunc F)

The uniform space structure on RatFunc F coming from the valuation at infinity.

Equations

• RatFunc.CompletionAtInfty.instUniformSpace F = (RatFunc.inftyValued F).toUniformSpace

def RatFunc.CompletionAtInfty (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Type u_1

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

Equations

• RatFunc.CompletionAtInfty F = UniformSpace.Completion (RatFunc F)

@[instance_reducible]

noncomputable instance RatFunc.CompletionAtInfty.instField (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Field (CompletionAtInfty F)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RatFunc.CompletionAtInfty.instAlgebra (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Algebra (RatFunc F) (CompletionAtInfty F)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance RatFunc.CompletionAtInfty.instCoe (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Coe (RatFunc F) (CompletionAtInfty F)

Equations

• RatFunc.CompletionAtInfty.instCoe F = { coe := RatFunc.CompletionAtInfty.instCoe._aux_1 F }

@[instance_reducible]

noncomputable instance RatFunc.CompletionAtInfty.instInhabited (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Inhabited (CompletionAtInfty F)

Equations

• RatFunc.CompletionAtInfty.instInhabited F = { default := RatFunc.CompletionAtInfty.instInhabited._aux_1 F }

@[instance_reducible]

noncomputable instance RatFunc.CompletionAtInfty.instValuedWithZeroMultiplicativeInt (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] : Valued (CompletionAtInfty F) (WithZero (Multiplicative ℤ))

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

Equations

• One or more equations did not get rendered due to their size.

theorem RatFunc.valuedCompletionAtInfty.def (F : Type u_1) [Field F] [DecidableEq (RatFunc F)] {x : CompletionAtInfty F} : Valued.v x = Valued.extensionValuation x