feat(ring_theory/DVR,padics/padic_integers): characterize ideals of D…

…VRs, apply to `Z_p` (#3827)

Also introduce the p-adic valuation on `Z_p`, stolen 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/algebra/group_power.lean

@@ -224,6 +224,11 @@ instance pow.is_monoid_hom (n : ℕ) : is_monoid_hom ((^ n) : M → M) :=
 instance nsmul.is_add_monoid_hom (n : ℕ) : is_add_monoid_hom (nsmul n : A → A) :=
 { map_add := λ _ _, nsmul_add _ _ _, map_zero := nsmul_zero _ }
 
+lemma dvd_pow {x y : M} :
+  ∀ {n : ℕ} (hxy : x ∣ y) (hn : n ≠ 0), x ∣ y^n
+| 0     hxy hn := (hn rfl).elim
+| (n+1) hxy hn := by { rw [pow_succ], exact dvd_mul_of_dvd_left hxy _ }
+
 end comm_monoid
 
 section group

src/data/padics/padic_integers.lean

@@ -5,6 +5,7 @@ Authors: Robert Y. Lewis, Mario Carneiro
 -/
 import data.int.modeq
 import data.padics.padic_numbers
+import ring_theory.discrete_valuation_ring
 
 /-!
 # p-adic integers
@@ -124,6 +125,11 @@ inverse is defined to be 0. -/
 def inv : ℤ_[p] → ℤ_[p]
 | ⟨k, _⟩ := if h : ∥k∥ = 1 then ⟨1/k, by simp [h]⟩ else 0
 
+instance : char_zero ℤ_[p] :=
+{ cast_injective :=
+  λ m n h, cast_injective $
+  show (m:ℚ_[p]) = n, by { rw subtype.ext_iff at h, norm_cast at h, exact h } }
+
 end padic_int
 
 section instances
@@ -210,6 +216,13 @@ by simp [padic_norm_z]
 @[simp] lemma padic_norm_z_eq_padic_norm_e {q : ℚ_[p]} (hq : ∥q∥ ≤ 1) :
   @norm ℤ_[p] _ ⟨q, hq⟩ = ∥q∥ := rfl
 
+@[simp] lemma norm_p : ∥(p : ℤ_[p])∥ = p⁻¹ :=
+show ∥((p : ℤ_[p]) : ℚ_[p])∥ = p⁻¹, by exact_mod_cast padic_norm_e.norm_p
+
+@[simp] lemma norm_p_pow (n : ℕ) : ∥(p : ℤ_[p])^n∥ = p^(-n:ℤ) :=
+show ∥((p^n : ℤ_[p]) : ℚ_[p])∥ = p^(-n:ℤ),
+by { convert padic_norm_e.norm_p_pow n, simp, }
+
 end padic_norm_z
 
 private lemma mul_lt_one {α} [decidable_linear_ordered_comm_ring α] {a b : α} (hbz : 0 < b)
@@ -227,6 +240,41 @@ namespace padic_int
 
 variables {p : ℕ} [fact p.prime]
 
+/-! ### Valuation on `ℤ_[p]` -/
+
+/-- `padic_int.valuation` lifts the p-adic valuation on `ℚ` to `ℤ_[p]`.  -/
+def valuation (x : ℤ_[p]) := padic.valuation (x : ℚ_[p])
+
+lemma norm_eq_pow_val {x : ℤ_[p]} (hx : x ≠ 0) :
+  ∥x∥ = p^(-x.valuation) :=
+begin
+  convert padic.norm_eq_pow_val _,
+  contrapose! hx,
+  exact subtype.val_injective hx
+end
+
+@[simp] lemma valuation_zero : valuation (0 : ℤ_[p]) = 0 :=
+padic.valuation_zero
+
+@[simp] lemma valuation_one : valuation (1 : ℤ_[p]) = 0 :=
+padic.valuation_one
+
+@[simp] lemma valuation_p : valuation (p : ℤ_[p]) = 1 :=
+by simp [valuation, -cast_eq_of_rat_of_nat]
+
+lemma valuation_nonneg (x : ℤ_[p]) : 0 ≤ x.valuation :=
+begin
+  by_cases hx : x = 0,
+  { simp [hx] },
+  have h : (1 : ℝ) < p := by exact_mod_cast nat.prime.one_lt ‹_›,
+  rw [← neg_nonpos, ← (fpow_strict_mono h).le_iff_le],
+  show (p : ℝ) ^ -valuation x ≤ p ^ 0,
+  rw [← norm_eq_pow_val hx],
+  simpa using x.property,
+end
+
+/-! ### Units of `ℤ_[p]` -/
+
 local attribute [reducible] padic_int
 
 lemma mul_inv : ∀ {z : ℤ_[p]}, ∥z∥ = 1 → z * z.inv = 1
@@ -260,6 +308,42 @@ calc  ∥z1 * z2∥ = ∥z1∥ * ∥z2∥ : by simp
 @[simp] lemma mem_nonunits {z : ℤ_[p]} : z ∈ nonunits ℤ_[p] ↔ ∥z∥ < 1 :=
 by rw lt_iff_le_and_ne; simp [padic_norm_z.le_one z, nonunits, is_unit_iff]
 
+/-- A `p`-adic number `u` with `∥u∥ = 1` is a unit of `ℤ_[p]`. -/
+def mk_units {u : ℚ_[p]} (h : ∥u∥ = 1) : units ℤ_[p] :=
+let z : ℤ_[p] := ⟨u, le_of_eq h⟩ in ⟨z, z.inv, mul_inv h, inv_mul h⟩
+
+@[simp]
+lemma mk_units_eq {u : ℚ_[p]} (h : ∥u∥ = 1) : ((mk_units h : ℤ_[p]) : ℚ_[p]) = u :=
+rfl
+
+@[simp] lemma norm_units (u : units ℤ_[p]) : ∥(u : ℤ_[p])∥ = 1 :=
+is_unit_iff.mp $ by simp
+
+/-- `unit_coeff hx` is the unit `u` in the unique representation `x = u * p ^ n`.
+See `unit_coeff_spec`. -/
+def unit_coeff {x : ℤ_[p]} (hx : x ≠ 0) : units ℤ_[p] :=
+let u : ℚ_[p] := x*p^(-x.valuation) in
+have hu : ∥u∥ = 1,
+by simp [hx, nat.fpow_ne_zero_of_pos (by exact_mod_cast nat.prime.pos ‹_›) x.valuation,
+         norm_eq_pow_val, fpow_neg, inv_mul_cancel, -cast_eq_of_rat_of_nat],
+mk_units hu
+
+@[simp] lemma unit_coeff_coe {x : ℤ_[p]} (hx : x ≠ 0) :
+  (unit_coeff hx : ℚ_[p]) = x * p ^ (-x.valuation) := rfl
+
+lemma unit_coeff_spec {x : ℤ_[p]} (hx : x ≠ 0) :
+  x = (unit_coeff hx : ℤ_[p]) * p ^ int.nat_abs (valuation x) :=
+begin
+  apply subtype.coe_injective,
+  push_cast,
+  have repr : (x : ℚ_[p]) = (unit_coeff hx) * p ^ x.valuation,
+  { rw [unit_coeff_coe, mul_assoc, ← fpow_add],
+    { simp },
+    { exact_mod_cast nat.prime.ne_zero ‹_› } },
+  convert repr using 2,
+  rw [← fpow_coe_nat, int.nat_abs_of_nonneg (valuation_nonneg x)],
+end
+
 instance : local_ring ℤ_[p] :=
 local_of_nonunits_ideal zero_ne_one $ λ x y, by simp; exact norm_lt_one_add
 
@@ -283,7 +367,50 @@ def coe.ring_hom : ℤ_[p] →+* ℚ_[p]  :=
   map_mul' := coe_mul,
   map_add' := coe_add }
 
-instance : algebra ℤ_[p] ℚ_[p] := (coe.ring_hom : ℤ_[p] →+* ℚ_[p]).to_algebra
+lemma p_dvd_of_norm_lt_one {x : ℤ_[p]} (hx : ∥x∥ < 1) : ↑p ∣ x :=
+begin
+  by_cases hx0 : x = 0, { simp only [hx0, dvd_zero] },
+  rw unit_coeff_spec hx0,
+  by_cases H : x.valuation.nat_abs = 0,
+  { rw [int.nat_abs_eq_zero] at H,
+    rw [norm_eq_pow_val hx0, H, neg_zero, fpow_zero] at hx,
+    exact (lt_irrefl _ hx).elim, },
+  { apply dvd_mul_of_dvd_right,
+    exact dvd_pow (dvd_refl _) H, }
+end
+
+lemma p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] :=
+have (p : ℝ)⁻¹ < 1, from inv_lt_one $ by exact_mod_cast nat.prime.one_lt ‹_›,
+by simp [this]
+
+lemma maximal_ideal_eq_span_p : local_ring.maximal_ideal ℤ_[p] = ideal.span {p} :=
+begin
+  apply le_antisymm,
+  { intros x hx,
+    rw ideal.mem_span_singleton,
+    simp only [local_ring.mem_maximal_ideal, mem_nonunits] at hx,
+    exact p_dvd_of_norm_lt_one hx, },
+  { rw [ideal.span_le, set.singleton_subset_iff], exact p_nonnunit }
+end
+
+lemma prime_p : prime (p : ℤ_[p]) :=
+begin
+  rw [← ideal.span_singleton_prime, ← maximal_ideal_eq_span_p],
+  { apply_instance },
+  { exact_mod_cast nat.prime.ne_zero ‹_› }
+end
+
+lemma irreducible_p : irreducible (p : ℤ_[p]) :=
+irreducible_of_prime prime_p
+
+instance : discrete_valuation_ring ℤ_[p] :=
+discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization
+⟨p, irreducible_p, λ x hx, ⟨x.valuation.nat_abs, unit_coeff hx,
+  by rw [mul_comm, ← unit_coeff_spec hx]⟩⟩
+
+lemma ideal_eq_span_pow_p {s : ideal ℤ_[p]} (hs : s ≠ ⊥) :
+  ∃ n : ℕ, s = ideal.span {p ^ n} :=
+discrete_valuation_ring.ideal_eq_span_pow_irreducible hs irreducible_p
 
 end padic_int