feat(data/padics): more valuations, facts about norms (#3790)

Assorted lemmas about the `p`-adics. @jcommelin and I are adding algebraic structure here as part of the Witt vector development.

Some of these declarations are stolen shamelessly from the perfectoid project.

Coauthored by: Johan Commelin <johan@commelin.net>



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/data/padics/padic_norm.lean

@@ -491,9 +491,45 @@ The p-adic norm of 1 is 1.
 @[simp] protected lemma one : padic_norm p 1 = 1 := by simp [padic_norm]
 
 /--
-The image of `padic_norm p` is {0} ∪ {p^(-n) | n ∈ ℤ}.
+The p-adic norm of `p` is `1/p` if `p > 1`.
+
+See also `padic_norm.padic_norm_p_of_prime` for a version that assumes `p` is prime.
+-/
+lemma padic_norm_p {p : ℕ} (hp : 1 < p) : padic_norm p p = 1 / p :=
+by simp [padic_norm, (show p ≠ 0, by linarith), padic_val_rat.padic_val_rat_self hp]
+
+/--
+The p-adic norm of `p` is `1/p` if `p` is prime.
+
+See also `padic_norm.padic_norm_p` for a version that assumes `1 < p`.
+-/
+@[simp] lemma padic_norm_p_of_prime (p : ℕ) [fact p.prime] : padic_norm p p = 1 / p :=
+padic_norm_p $ nat.prime.one_lt ‹_›
+
+/--
+The p-adic norm of `p` is less than 1 if `1 < p`.
+
+See also `padic_norm.padic_norm_p_lt_one_of_prime` for a version assuming `prime p`.
+-/
+lemma padic_norm_p_lt_one {p : ℕ} (hp : 1 < p) : padic_norm p p < 1 :=
+begin
+  rw [padic_norm_p hp, div_lt_iff, one_mul],
+  { exact_mod_cast hp },
+  { exact_mod_cast zero_lt_one.trans hp },
+end
+
+/--
+The p-adic norm of `p` is less than 1 if `p` is prime.
+
+See also `padic_norm.padic_norm_p_lt_one` for a version assuming `1 < p`.
+-/
+lemma padic_norm_p_lt_one_of_prime (p : ℕ) [fact p.prime] : padic_norm p p < 1 :=
+padic_norm_p_lt_one $ nat.prime.one_lt ‹_›
+
+/--
+`padic_norm p q` takes discrete values `p ^ -z` for `z : ℤ`.
 -/
-protected theorem image {q : ℚ} (hq : q ≠ 0) : ∃ n : ℤ, padic_norm p q = p ^ (-n) :=
+protected theorem values_discrete {q : ℚ} (hq : q ≠ 0) : ∃ z : ℤ, padic_norm p q = p ^ (-z) :=
 ⟨ (padic_val_rat p q), by simp [padic_norm, hq] ⟩
 
 variable [hp : fact p.prime]

src/data/padics/padic_numbers.lean

@@ -10,37 +10,40 @@ import analysis.normed_space.basic
 /-!
 # p-adic numbers
 
-This file defines the p-adic numbers (rationals) ℚ_p as the completion of ℚ with respect to the
-p-adic norm. We show that the p-adic norm on ℚ extends to ℚ_p, that ℚ is embedded in ℚ_p, and that
-ℚ_p is Cauchy complete.
+This file defines the p-adic numbers (rationals) `ℚ_p` as the completion of `ℚ` with respect to the
+p-adic norm. We show that the p-adic norm on ℚ extends to `ℚ_p`, that `ℚ` is embedded in `ℚ_p`, and that
+`ℚ_p` is Cauchy complete.
 
 ## Important definitions
 
 * `padic` : the type of p-adic numbers
-* `padic_norm_e` : the rational valued p-adic norm on ℚ_p
+* `padic_norm_e` : the rational valued p-adic norm on `ℚ_p`
 
 ## Notation
 
-We introduce the notation ℚ_[p] for the p-adic numbers.
+We introduce the notation `ℚ_[p]` for the p-adic numbers.
 
 ## Implementation notes
 
 Much, but not all, of this file assumes that `p` is prime. This assumption is inferred automatically
 by taking `[fact (prime p)]` as a type class argument.
 
-We use the same concrete Cauchy sequence construction that is used to construct ℝ. ℚ_p inherits a
-field structure from this construction. The extension of the norm on ℚ to ℚ_p is *not* analogous to
-extending the absolute value to ℝ, and hence the proof that ℚ_p is complete is different from the
+We use the same concrete Cauchy sequence construction that is used to construct ℝ. `ℚ_p` inherits a
+field structure from this construction. The extension of the norm on ℚ to `ℚ_p` is *not* analogous to
+extending the absolute value to ℝ, and hence the proof that `ℚ_p` is complete is different from the
 proof that ℝ is complete.
 
 A small special-purpose simplification tactic, `padic_index_simp`, is used to manipulate sequence
 indices in the proof that the norm extends.
 
-`padic_norm_e` is the rational-valued p-adic norm on ℚ_p. To instantiate ℚ_p as a normed field, we
-must cast this into a ℝ-valued norm. The ℝ-valued norm, using notation ∥ ∥ from normed spaces, is
-the canonical representation of this norm.
+`padic_norm_e` is the rational-valued p-adic norm on `ℚ_p`. To instantiate `ℚ_p` as a normed field,
+we must cast this into a ℝ-valued norm. The `ℝ`-valued norm, using notation `∥ ∥` from normed spaces,
+is the canonical representation of this norm.
 
-Coercions from ℚ to ℚ_p are set up to work with the `norm_cast` tactic.
+`simp` prefers `padic_norm` to `padic_norm_e` when possible.
+Since `padic_norm_e` and `∥ ∥` have different types, `simp` does not rewrite one to the other.
+
+Coercions from `ℚ` to `ℚ_p` are set up to work with the `norm_cast` tactic.
 
 ## References
 
@@ -190,6 +193,42 @@ end
 
 end embedding
 
+section valuation
+open cau_seq
+variables {p : ℕ} [fact p.prime]
+
+/-! ### Valuation on `padic_seq` -/
+
+/--
+The `p`-adic valuation on `ℚ` lifts to `padic_seq p`.
+`valuation f` is defined to be the valuation of the (`ℚ`-valued) stationary point of `f`.
+-/
+def valuation (f : padic_seq p) : ℤ :=
+if hf : f ≈ 0 then 0 else padic_val_rat p (f (stationary_point hf))
+
+lemma norm_eq_pow_val {f : padic_seq p} (hf : ¬ f ≈ 0) :
+  f.norm = p^(-f.valuation : ℤ) :=
+begin
+  rw [norm, valuation, dif_neg hf, dif_neg hf, padic_norm, if_neg],
+  intro H,
+  apply cau_seq.not_lim_zero_of_not_congr_zero hf,
+  intros ε hε,
+  use (stationary_point hf),
+  intros n hn,
+  rw stationary_point_spec hf (le_refl _) hn,
+  simpa [H] using hε,
+end
+
+lemma val_eq_iff_norm_eq {f g : padic_seq p} (hf : ¬ f ≈ 0) (hg : ¬ g ≈ 0) :
+  f.valuation = g.valuation ↔ f.norm = g.norm :=
+begin
+  rw [norm_eq_pow_val hf, norm_eq_pow_val hg, ← neg_inj, fpow_inj],
+  { exact_mod_cast nat.prime.pos ‹_› },
+  { exact_mod_cast nat.prime.ne_one ‹_› },
+end
+
+end valuation
+
 end padic_seq
 
 section
@@ -254,10 +293,10 @@ else
   have ¬ (const (padic_norm p) q) ≈ 0, from not_equiv_zero_const_of_nonzero hq,
   by simp [norm, this]
 
-lemma norm_image (a : padic_seq p) (ha : ¬ a ≈ 0) :
-  (∃ (n : ℤ), a.norm = ↑p ^ (-n)) :=
+lemma norm_values_discrete (a : padic_seq p) (ha : ¬ a ≈ 0) :
+  (∃ (z : ℤ), a.norm = ↑p ^ (-z)) :=
 let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha in
-by simpa [hk] using padic_norm.image p hk'
+by simpa [hk] using padic_norm.values_discrete p hk'
 
 lemma norm_one : norm (1 : padic_seq p) = 1 :=
 have h1 : ¬ (1 : padic_seq p) ≈ 0, from one_not_equiv_zero _,
@@ -400,7 +439,7 @@ namespace padic
 section completion
 variables {p : ℕ} [fact p.prime]
 
-/-- The discrete field structure on ℚ_p is inherited from the Cauchy completion construction. -/
+/-- The discrete field structure on `ℚ_p` is inherited from the Cauchy completion construction. -/
 instance field : field (ℚ_[p]) :=
 cau_seq.completion.field
 
@@ -449,21 +488,21 @@ cau_seq.completion.of_rat_div
 
 @[simp] lemma of_rat_zero : of_rat p 0 = 0 := rfl
 
-@[simp] lemma cast_eq_of_rat_of_nat (n : ℕ) : (↑n : ℚ_[p]) = of_rat p n :=
+lemma cast_eq_of_rat_of_nat (n : ℕ) : (↑n : ℚ_[p]) = of_rat p n :=
 begin
   induction n with n ih,
   { refl },
   { simpa using ih }
 end
 
-@[simp] lemma cast_eq_of_rat_of_int (n : ℤ) : ↑n = of_rat p n :=
-by induction n; simp
+lemma cast_eq_of_rat_of_int (n : ℤ) : ↑n = of_rat p n :=
+by induction n; simp [cast_eq_of_rat_of_nat]
 
 lemma cast_eq_of_rat : ∀ (q : ℚ), (↑q : ℚ_[p]) = of_rat p q
 | ⟨n, d, h1, h2⟩ :=
   show ↑n / ↑d = _, from
     have (⟨n, d, h1, h2⟩ : ℚ) = rat.mk n d, from rat.num_denom',
-    by simp [this, rat.mk_eq_div, of_rat_div]
+    by simp [this, rat.mk_eq_div, of_rat_div, cast_eq_of_rat_of_int, cast_eq_of_rat_of_nat]
 
 @[norm_cast] lemma coe_add : ∀ {x y : ℚ}, (↑(x + y) : ℚ_[p]) = ↑x + ↑y := by simp [cast_eq_of_rat]
 @[norm_cast] lemma coe_neg : ∀ {x : ℚ}, (↑(-x) : ℚ_[p]) = -↑x := by simp [cast_eq_of_rat]
@@ -491,7 +530,7 @@ instance : char_zero ℚ_[p] :=
 end completion
 end padic
 
-/-- The rational-valued p-adic norm on ℚ_p is lifted from the norm on Cauchy sequences. The
+/-- The rational-valued p-adic norm on `ℚ_p` is lifted from the norm on Cauchy sequences. The
 canonical form of this function is the normed space instance, with notation `∥ ∥`. -/
 def padic_norm_e {p : ℕ} [hp : fact p.prime] : ℚ_[p] → ℚ :=
 quotient.lift padic_seq.norm $ @padic_seq.norm_equiv _ _
@@ -582,7 +621,7 @@ norm_const _
 protected theorem image' {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, padic_norm_e q = p ^ (-n) :=
 quotient.induction_on q $ λ f hf,
   have ¬ f ≈ 0, from (ne_zero_iff_nequiv_zero f).1 hf,
-  norm_image f this
+  norm_values_discrete f this
 
 lemma sub_rev (q r : ℚ_[p]) : padic_norm_e (q - r) = padic_norm_e (r - q) :=
 by rw ←(padic_norm_e.neg); simp
@@ -785,11 +824,27 @@ instance : nondiscrete_normed_field ℚ_[p] :=
     exact_mod_cast h1,
   end⟩ }
 
+@[simp] lemma norm_p : ∥(p : ℚ_[p])∥ = p⁻¹ :=
+begin
+  have p₀ : p ≠ 0 := nat.prime.ne_zero ‹_›,
+  have p₁ : p ≠ 1 := nat.prime.ne_one ‹_›,
+  simp [p₀, p₁, norm, padic_norm, padic_val_rat, fpow_neg, padic.cast_eq_of_rat_of_nat],
+end
+
+lemma norm_p_lt_one : ∥(p : ℚ_[p])∥ < 1 :=
+begin
+  rw [norm_p, inv_eq_one_div, div_lt_iff, one_mul],
+  { exact_mod_cast nat.prime.one_lt ‹_› },
+  { exact_mod_cast nat.prime.pos ‹_› }
+end
+
+@[simp] lemma norm_p_pow (n : ℤ) : ∥(p^n : ℚ_[p])∥ = p^-n :=
+by rw [normed_field.norm_fpow, norm_p]; field_simp
 
 protected theorem image {q : ℚ_[p]} : q ≠ 0 → ∃ n : ℤ, ∥q∥ = ↑((↑p : ℚ) ^ (-n)) :=
 quotient.induction_on q $ λ f hf,
   have ¬ f ≈ 0, from (padic_seq.ne_zero_iff_nequiv_zero f).1 hf,
-  let ⟨n, hn⟩ := padic_seq.norm_image f this in
+  let ⟨n, hn⟩ := padic_seq.norm_values_discrete f this in
   ⟨n, congr_arg coe hn⟩
 
 protected lemma is_rat (q : ℚ_[p]) : ∃ q' : ℚ, ∥q∥ = ↑q' :=
@@ -865,4 +920,61 @@ calc ∥f.lim∥ = ∥f.lim - f N + f N∥ : by simp
                 ... ≤ max (∥f.lim - f N∥) (∥f N∥) : padic_norm_e.nonarchimedean _ _
                 ... ≤ a : max_le (le_of_lt (hN _ (le_refl _))) (hf _)
 
+/-!
+### Valuation on `ℚ_[p]`
+-/
+
+/--
+`padic.valuation` lifts the p-adic valuation on rationals to `ℚ_[p]`.
+-/
+def valuation : ℚ_[p] → ℤ :=
+quotient.lift (@padic_seq.valuation p _) (λ f g h,
+begin
+  by_cases hf : f ≈ 0,
+  { have hg : g ≈ 0, from setoid.trans (setoid.symm h) hf,
+    simp [hf, hg, padic_seq.valuation] },
+  { have hg : ¬ g ≈ 0, from (λ hg, hf (setoid.trans h hg)),
+    rw padic_seq.val_eq_iff_norm_eq hf hg,
+    exact padic_seq.norm_equiv h },
+end)
+
+@[simp] lemma valuation_zero : valuation (0 : ℚ_[p]) = 0 :=
+dif_pos ((const_equiv p).2 rfl)
+
+@[simp] lemma valuation_one : valuation (1 : ℚ_[p]) = 0 :=
+begin
+  change dite (cau_seq.const (padic_norm p) 1 ≈ _) _ _ = _,
+  have h : ¬ cau_seq.const (padic_norm p) 1 ≈ 0,
+  { assume H, erw const_equiv p at H, exact one_ne_zero H },
+  rw dif_neg h,
+  simp,
+end
+
+lemma norm_eq_pow_val {x : ℚ_[p]} : x ≠ 0 → ∥x∥ = p^(-x.valuation) :=
+begin
+  apply quotient.induction_on' x, clear x,
+  intros f hf,
+  change (padic_seq.norm _ : ℝ) = (p : ℝ) ^ -padic_seq.valuation _,
+  rw padic_seq.norm_eq_pow_val,
+  change ↑((p : ℚ) ^ -padic_seq.valuation f) = (p : ℝ) ^ -padic_seq.valuation f,
+  { rw rat.cast_fpow,
+    congr' 1,
+    norm_cast },
+  { apply cau_seq.not_lim_zero_of_not_congr_zero,
+    contrapose! hf,
+    apply quotient.sound,
+    simpa using hf, }
+end
+
+@[simp] lemma valuation_p : valuation (p : ℚ_[p]) = 1 :=
+begin
+  have h : (1 : ℝ) < p := by exact_mod_cast nat.prime.one_lt ‹_›,
+  rw ← neg_inj,
+  apply (fpow_strict_mono h).injective,
+  dsimp only,
+  rw ← norm_eq_pow_val,
+  { simp },
+  { exact_mod_cast nat.prime.ne_zero ‹_›, }
+end
+
 end padic