Absolute values from valuations

This file constructs an absolute value by composing a valuation with a monotone, zero-reflecting monoid-with-zero homomorphism.

noncomputable def Valuation.toAbsoluteValue {K : Type u_1} {S : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] [Semiring S] [PartialOrder S] [addLeftMono : AddLeftMono S] [addRightMono : AddRightMono S] (v : Valuation K Γ₀) (f : Γ₀ →*₀ S) (hf : ∀ ⦃a b : Γ₀⦄, a ≤ b → f a ≤ f b) (hf_zero : ∀ (a : Γ₀), f a = 0 ↔ a = 0) : AbsoluteValue K S

Compose a valuation with a monotone, zero-reflecting monoid-with-zero homomorphism to obtain an absolute value.

Equations

• v.toAbsoluteValue f hf hf_zero = { toMulHom := ↑(f.comp ↑v), nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

@[simp]

theorem Valuation.toAbsoluteValue_apply {K : Type u_1} {S : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] [Semiring S] [PartialOrder S] [addLeftMono : AddLeftMono S] [addRightMono : AddRightMono S] (v : Valuation K Γ₀) (f : Γ₀ →*₀ S) (hf : ∀ ⦃a b : Γ₀⦄, a ≤ b → f a ≤ f b) (hf_zero : ∀ (a : Γ₀), f a = 0 ↔ a = 0) (x : K) : (v.toAbsoluteValue f hf hf_zero) x = f (v x)

Evaluation of the absolute value obtained by composing a valuation with a monotone, zero-reflecting monoid-with-zero homomorphism.

theorem Valuation.toAbsoluteValue_add_le_right {K : Type u_1} {S : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] [Semiring S] [PartialOrder S] [addLeftMono : AddLeftMono S] [addRightMono : AddRightMono S] (v : Valuation K Γ₀) (f : Γ₀ →*₀ S) (hf : ∀ ⦃a b : Γ₀⦄, a ≤ b → f a ≤ f b) (hf_zero : ∀ (a : Γ₀), f a = 0 ↔ a = 0) {x y : K} (h : v x ≤ v y) : (v.toAbsoluteValue f hf hf_zero) (x + y) ≤ (v.toAbsoluteValue f hf hf_zero) y

If one input has no larger valuation than another, their sum has absolute value at most that of the latter.

theorem Valuation.isNonarchimedean_toAbsoluteValue {K : Type u_1} {S : Type u_2} {Γ₀ : Type u_3} [DivisionRing K] [LinearOrderedCommMonoidWithZero Γ₀] [Nontrivial Γ₀] [Semiring S] [LinearOrder S] [addLeftMono : AddLeftMono S] [addRightMono : AddRightMono S] (v : Valuation K Γ₀) (f : Γ₀ →*₀ S) (hf : ∀ ⦃a b : Γ₀⦄, a ≤ b → f a ≤ f b) (hf_zero : ∀ (a : Γ₀), f a = 0 ↔ a = 0) : IsNonarchimedean ⇑(v.toAbsoluteValue f hf hf_zero)

An absolute value obtained from a valuation through a monotone realization is nonarchimedean.