Ostrowski’s Theorem #
The goal of this file is to prove Ostrowski’s Theorem which gives a list of all the nontrivial absolute values on a number field up to equivalence. (TODO)
References #
- K. Conrad, Ostroski's Theorem for Q
- K. Conrad, Ostroski for number fields
- J. W. S. Cassels, Local fields
Tags #
ring_norm, ostrowski
Values of a multiplicative norm of the rationals coincide on ℕ if and only if they coincide
on ℤ
.
Values of a multiplicative norm of the rationals are determined by the values on the natural numbers.
The equivalence class of a multiplicative norm on the rationals is determined by its values on the natural numbers.
The mulRingNorm corresponding to the p-adic norm on ℚ
.
Equations
- Rat.MulRingNorm.mulRingNorm_padic p = { toFun := fun (x : ℚ) => ↑(padicNorm p x), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, map_one' := ⋯, map_mul' := ⋯, eq_zero_of_map_eq_zero' := ⋯ }
Instances For
@[simp]
theorem
Rat.MulRingNorm.mulRingNorm_eq_padic_norm
(p : ℕ)
[Fact (Nat.Prime p)]
(r : ℚ)
:
(Rat.MulRingNorm.mulRingNorm_padic p) r = ↑(padicNorm p r)
theorem
Rat.MulRingNorm.mulRingNorm_equiv_padic_of_bounded
{f : MulRingNorm ℚ}
(hf_nontriv : f ≠ 1)
(bdd : ∀ (n : ℕ), f ↑n ≤ 1)
:
∃! p : ℕ, ∃ (hp : Fact (Nat.Prime p)), f.equiv (Rat.MulRingNorm.mulRingNorm_padic p)
If f
is bounded and not trivial, then it is equivalent to a p-adic absolute value.