Basic properties of archimedean and non-archimedean ℝ-valued AbsoluteValue

Consider an ℝ-valued AbsoluteValue.

• It is called finite, if it is non-archimedean (IsNonarchimedean).
• It is called archimedean or infinite, if it is not non-archimedean.

Main results:

• AbsoluteValue.not_isNonarchimedean_iff_exists_apply_le_one_and_apply_add_one_gt_one: an absolute value v is archimedean if and only if there exists x such that v x ≤ 1 and v (x + 1) > 1.
• AbsoluteValue.isNonarchimedean_iff_exists_forall_apply_natCast_le: an absolute value v is non-archimedean if and only if v(ℕ) is bounded.
• AbsoluteValue.charZero_of_not_isNonarchimedean: if a field has an infinite place, then it must be of characteristic zero.

@[simp]

theorem AbsoluteValue.comp_apply {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) {f : T →+* R} (hf : Function.Injective ⇑f) (x : T) : (v.comp hf) x = v (f x)

TODO: go mathlib

@[simp]

theorem AbsoluteValue.comp_id {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] [PartialOrder S] (v : AbsoluteValue R S) : v.comp ⋯ = v

TODO: go mathlib

theorem AbsoluteValue.IsEquiv.comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring T] [Semiring R] [Semiring S] [PartialOrder S] {v w : AbsoluteValue R S} (h : v.IsEquiv w) {f : T →+* R} (hf : Function.Injective ⇑f) : (v.comp hf).IsEquiv (w.comp hf)

TODO: go mathlib

theorem AbsoluteValue.liesOver_iff {K : Type u_1} {L : Type u_2} {S : Type u_3} [CommRing K] [IsSimpleRing K] [CommRing L] [Algebra K L] [PartialOrder S] [Nontrivial L] [Semiring S] {w : AbsoluteValue L S} {v : AbsoluteValue K S} : w.LiesOver v ↔ w.comp ⋯ = v

TODO: use @[mk_iff] instead

instance AbsoluteValue.liesOver_comp {K : Type u_1} {L : Type u_2} {S : Type u_3} [CommRing K] [IsSimpleRing K] [CommRing L] [Algebra K L] [PartialOrder S] [Nontrivial L] [Semiring S] (w : AbsoluteValue L S) : w.LiesOver (w.comp ⋯)

TODO: go mathlib

instance AbsoluteValue.liesOver_self {K : Type u_1} {S : Type u_2} [CommRing K] [IsSimpleRing K] [PartialOrder S] [Semiring S] (v : AbsoluteValue K S) : v.LiesOver v

TODO: go mathlib

theorem AbsoluteValue.liesOver_self_iff {K : Type u_1} {S : Type u_2} [CommRing K] [IsSimpleRing K] [PartialOrder S] [Semiring S] (v w : AbsoluteValue K S) : v.LiesOver w ↔ v = w

TODO: go mathlib

theorem AbsoluteValue.LiesOver.trans {K : Type u_1} {L : Type u_2} {M : Type u_3} {S : Type u_4} [CommRing K] [CommRing L] [CommRing M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsSimpleRing K] [IsSimpleRing L] [Nontrivial M] [PartialOrder S] [Semiring S] (w : AbsoluteValue M S) (v : AbsoluteValue L S) (u : AbsoluteValue K S) [hwv : w.LiesOver v] [hvu : v.LiesOver u] : w.LiesOver u

TODO: go mathlib

theorem AbsoluteValue.LiesOver.tower_bot {K : Type u_1} {L : Type u_2} {M : Type u_3} {S : Type u_4} [CommRing K] [CommRing L] [CommRing M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsSimpleRing K] [IsSimpleRing L] [Nontrivial M] [PartialOrder S] [Semiring S] (w : AbsoluteValue M S) (v : AbsoluteValue L S) (u : AbsoluteValue K S) [hwv : w.LiesOver v] [hwu : w.LiesOver u] : v.LiesOver u

TODO: go mathlib

Criterion for a place to be non-archimedean

theorem AbsoluteValue.not_isNonarchimedean_iff_exists_apply_le_one_and_apply_add_one_gt_one {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : ¬IsNonarchimedean ⇑v ↔ ∃ (x : K), v x ≤ 1 ∧ v (x + 1) > 1

An absolute value v is archimedean if and only if there exists x such that v x ≤ 1 and v (x + 1) > 1.

theorem AbsoluteValue.isNontrivial_of_not_isNonarchimedean {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) : v.IsNontrivial

An archimedean absolute value is not trivial.

theorem AbsoluteValue.isNonarchimedean_iff_exists_forall_apply_natCast_le {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : IsNonarchimedean ⇑v ↔ ∃ (C : ℝ), ∀ (n : ℕ), v ↑n ≤ C

An absolute value v is non-archimedean if and only if v(ℕ) is bounded.

theorem AbsoluteValue.isNonarchimedean_iff_forall_apply_natCast_le_one {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) : IsNonarchimedean ⇑v ↔ ∀ (n : ℕ), v ↑n ≤ 1

An absolute value v is non-archimedean if and only if v(ℕ) is bounded by one.

theorem AbsoluteValue.isNonarchimedean_comp_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] (v : AbsoluteValue L ℝ) (f : K →+* L) : IsNonarchimedean ⇑(v.comp ⋯) ↔ IsNonarchimedean ⇑v

theorem AbsoluteValue.isNonarchimedean_iff_of_liesOver {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : IsNonarchimedean ⇑v ↔ IsNonarchimedean ⇑w

theorem AbsoluteValue.isNonarchimedean_iff_of_equiv {K : Type u_1} [Field K] {v w : AbsoluteValue K ℝ} (h0 : v ≈ w) : IsNonarchimedean ⇑v ↔ IsNonarchimedean ⇑w

theorem AbsoluteValue.isNontrivial_of_isNontrivial_comp {K : Type u_1} {L : Type u_2} [Field K] [Field L] (v : AbsoluteValue L ℝ) {f : K →+* L} (h : (v.comp ⋯).IsNontrivial) : v.IsNontrivial

theorem AbsoluteValue.isNontrivial_iff_of_liesOver {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsAlgebraic K L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : v.IsNontrivial ↔ w.IsNontrivial

theorem AbsoluteValue.charZero_of_not_isNonarchimedean {K : Type u_1} [Field K] (v : AbsoluteValue K ℝ) (h : ¬IsNonarchimedean ⇑v) : CharZero K

If a field K has an infinite place, then it must be of characteristic zero.

@[simp]

theorem Rat.AbsoluteValue.isNonarchimedean_padic (p : ℕ) [Fact (Nat.Prime p)] : IsNonarchimedean ⇑(padic p)

TODO: go mathlib

@[simp]

theorem Rat.AbsoluteValue.not_isNonarchimedean_real : ¬IsNonarchimedean ⇑real

TODO: go mathlib

@[simp]

theorem Rat.AbsoluteValue.isNontrivial_padic (p : ℕ) [Fact (Nat.Prime p)] : (padic p).IsNontrivial

TODO: go mathlib

@[simp]

theorem Rat.AbsoluteValue.isNontrivial_real : real.IsNontrivial

TODO: go mathlib

theorem Rat.AbsoluteValue.equiv_real_of_not_isNonarchimedean (v : AbsoluteValue ℚ ℝ) (h : ¬IsNonarchimedean ⇑v) : v ≈ real

TODO: go mathlib

theorem Rat.AbsoluteValue.equiv_padic_of_isNonarchimedean (v : AbsoluteValue ℚ ℝ) (h0 : v.IsNontrivial) (h : IsNonarchimedean ⇑v) : ∃! p : ℕ, ∃ (x : Fact (Nat.Prime p)), v ≈ padic p

TODO: go mathlib

def AbsoluteValue.toValuation {R : Type u_1} [Ring R] [Nontrivial R] (v : AbsoluteValue R ℝ) (h : IsNonarchimedean ⇑v) : Valuation R NNReal

A non-archimedean absolute value is a valuation.

Equations

• v.toValuation h = { toFun := fun (x : R) => ⟨v x, ⋯⟩, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

@[simp]

theorem AbsoluteValue.toValuation_toFun_coe {R : Type u_1} [Ring R] [Nontrivial R] (v : AbsoluteValue R ℝ) (h : IsNonarchimedean ⇑v) (x : R) : ↑((v.toValuation h) x) = v x

noncomputable def AbsoluteValue.rpowOfLeOneOrIsNonarchimedean {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (c : ℝ) (h1 : 0 < c) (h2 : c ≤ 1 ∨ IsNonarchimedean ⇑v) : AbsoluteValue R ℝ

If v is an ℝ-valued absolute value, c is a positive real number, either c ≤ 1 or v is non-archimedean, then v ^ c is also an absolute value.

Equations

• v.rpowOfLeOneOrIsNonarchimedean c h1 h2 = { toFun := fun (x : R) => v x ^ c, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }

@[simp]

theorem AbsoluteValue.rpowOfLeOneOrIsNonarchimedean_apply {R : Type u_1} [Semiring R] (v : AbsoluteValue R ℝ) (c : ℝ) (h1 : 0 < c) (h2 : c ≤ 1 ∨ IsNonarchimedean ⇑v) (x : R) : (v.rpowOfLeOneOrIsNonarchimedean c h1 h2) x = v x ^ c

Retrieving the p for a p-adic valuation

noncomputable def AbsoluteValue.adic {K : Type u_1} [Field K] [CharZero K] (v : AbsoluteValue K ℝ) : ℕ

If v is an ℝ-valued absolute value on a characteristic zero field, then AbsoluteValue.adic v is the natural number p such that either:

• p is a prime and the restriction of v to ℚ is equivalent to the usual p-adic valuation;
• p = 1 and the restriction of v to ℚ is equivalent to the usual ∞-adic valuation;
• p = 0 and the restriction of v to ℚ is trivial.

Equations

• v.adic = if nontriv : (v.comp ⋯).IsNontrivial then if h : v.comp ⋯ ≈ Rat.AbsoluteValue.real then 1 else ⋯.choose else 0

theorem AbsoluteValue.adic_eq_of_liesOver {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [CharZero K] [CharZero L] (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) [w.LiesOver v] : v.adic = w.adic

theorem AbsoluteValue.adic_eq_of_equiv {K : Type u_1} [Field K] [CharZero K] {v w : AbsoluteValue K ℝ} (h0 : v ≈ w) : v.adic = w.adic

theorem AbsoluteValue.adic_eq_one_iff {K : Type u_1} [Field K] [CharZero K] {v : AbsoluteValue K ℝ} : v.adic = 1 ↔ ¬IsNonarchimedean ⇑v

theorem AbsoluteValue.adic_eq_zero_iff {K : Type u_1} [Field K] [CharZero K] {v : AbsoluteValue K ℝ} : v.adic = 0 ↔ ¬(v.comp ⋯).IsNontrivial

theorem AbsoluteValue.adic_eq_zero_iff_of_isAlgebraic {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {v : AbsoluteValue K ℝ} : v.adic = 0 ↔ ¬v.IsNontrivial

theorem AbsoluteValue.prime_adic {K : Type u_1} [Field K] [CharZero K] {v : AbsoluteValue K ℝ} (h1 : (v.comp ⋯).IsNontrivial) (h2 : IsNonarchimedean ⇑v) : Nat.Prime v.adic

theorem AbsoluteValue.prime_adic_of_isAlgebraic {K : Type u_1} [Field K] [CharZero K] [Algebra.IsAlgebraic ℚ K] {v : AbsoluteValue K ℝ} (h1 : v.IsNontrivial) (h2 : IsNonarchimedean ⇑v) : Nat.Prime v.adic

@[simp]

theorem Rat.AbsoluteValue.adic_padic (p : ℕ) [Fact (Nat.Prime p)] : (padic p).adic = p

@[simp]

theorem Rat.AbsoluteValue.adic_real : real.adic = 1