From 466f54eb4c69c0c4babe29c39af7442d0e902303 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 10 Dec 2024 10:02:04 +0000 Subject: [PATCH] =?UTF-8?q?refactor:=20make=20`PadicInt.valuation`=20`?= =?UTF-8?q?=E2=84=95`-valued=20It=20is=20currently=20`=E2=84=A4`-valued,?= =?UTF-8?q?=20but=20always=20nonnegative.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit From FLT --- Mathlib/NumberTheory/Padics/MahlerBasis.lean | 7 +- .../NumberTheory/Padics/PadicIntegers.lean | 150 +++++++----------- Mathlib/NumberTheory/Padics/PadicNumbers.lean | 72 ++++++--- Mathlib/NumberTheory/Padics/RingHoms.lean | 15 +- 4 files changed, 113 insertions(+), 131 deletions(-) diff --git a/Mathlib/NumberTheory/Padics/MahlerBasis.lean b/Mathlib/NumberTheory/Padics/MahlerBasis.lean index c96931b3ec854..6f4ac315c6928 100644 --- a/Mathlib/NumberTheory/Padics/MahlerBasis.lean +++ b/Mathlib/NumberTheory/Padics/MahlerBasis.lean @@ -181,9 +181,10 @@ private lemma bojanic_mahler_step2 {f : C(ℤ_[p], E)} {s t : ℕ} refine mul_le_mul_of_nonneg_right ?_ (by simp only [zero_le]) -- remains to show norm of binomial coeff is `≤ p⁻¹` have : 0 < (p ^ t).choose (i + 1) := Nat.choose_pos (by omega) - rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, Padic.norm_eq_pow_val (mod_cast this.ne'), - coe_zpow, NNReal.coe_natCast, (zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).le_iff_le, - neg_le_neg_iff, Padic.valuation_natCast, Nat.one_le_cast] + rw [← zpow_neg_one, ← coe_le_coe, coe_nnnorm, Padic.norm_eq_zpow_neg_valuation + (mod_cast this.ne'), coe_zpow, NNReal.coe_natCast, + zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt), neg_le_neg_iff, Padic.valuation_natCast, + Nat.one_le_cast] exact one_le_padicValNat_of_dvd this <| hp.out.dvd_choose_pow (by omega) (by omega) · -- Bounding the sum over `range (n + 1)`: every term is small by the choice of `t` refine norm_sum_le_of_forall_le_of_nonempty nonempty_range_succ (fun i _ ↦ ?_) diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 163ab12838048..326ef6043194c 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -50,20 +50,19 @@ open Padic Metric IsLocalRing noncomputable section +variable (p : ℕ) [hp : Fact p.Prime] + /-- The `p`-adic integers `ℤ_[p]` are the `p`-adic numbers with norm `≤ 1`. -/ -def PadicInt (p : ℕ) [Fact p.Prime] := - { x : ℚ_[p] // ‖x‖ ≤ 1 } +def PadicInt : Type := {x : ℚ_[p] // ‖x‖ ≤ 1} /-- The ring of `p`-adic integers. -/ notation "ℤ_[" p "]" => PadicInt p namespace PadicInt +variable {p} {x y : ℤ_[p]} /-! ### Ring structure and coercion to `ℚ_[p]` -/ - -variable {p : ℕ} [Fact p.Prime] - instance : Coe ℤ_[p] ℚ_[p] := ⟨Subtype.val⟩ @@ -127,9 +126,9 @@ theorem coe_one : ((1 : ℤ_[p]) : ℚ_[p]) = 1 := rfl @[simp, norm_cast] theorem coe_zero : ((0 : ℤ_[p]) : ℚ_[p]) = 0 := rfl -theorem coe_eq_zero (z : ℤ_[p]) : (z : ℚ_[p]) = 0 ↔ z = 0 := by rw [← coe_zero, Subtype.coe_inj] +@[simp] lemma coe_eq_zero : (x : ℚ_[p]) = 0 ↔ x = 0 := by rw [← coe_zero, Subtype.coe_inj] -theorem coe_ne_zero (z : ℤ_[p]) : (z : ℚ_[p]) ≠ 0 ↔ z ≠ 0 := z.coe_eq_zero.not +lemma coe_ne_zero : (x : ℚ_[p]) ≠ 0 ↔ x ≠ 0 := coe_eq_zero.not instance : AddCommGroup ℤ_[p] := (by infer_instance : AddCommGroup (subring p)) @@ -178,10 +177,6 @@ def ofIntSeq (seq : ℕ → ℤ) (h : IsCauSeq (padicNorm p) fun n => seq n) : split_ifs with hne <;> norm_cast apply padicNorm.of_int⟩ -end PadicInt - -namespace PadicInt - /-! ### Instances We now show that `ℤ_[p]` is a @@ -190,8 +185,7 @@ We now show that `ℤ_[p]` is a * integral domain -/ - -variable (p : ℕ) [Fact p.Prime] +variable (p) instance : MetricSpace ℤ_[p] := Subtype.metricSpace @@ -228,15 +222,8 @@ variable {p} instance : IsDomain ℤ_[p] := Function.Injective.isDomain (subring p).subtype Subtype.coe_injective -end PadicInt - -namespace PadicInt - /-! ### Norm -/ - -variable {p : ℕ} [Fact p.Prime] - theorem norm_le_one (z : ℤ_[p]) : ‖z‖ ≤ 1 := z.2 @[simp] @@ -291,12 +278,6 @@ instance complete : CauSeq.IsComplete ℤ_[p] norm := ⟨⟨_, hqn⟩, fun ε => by simpa [norm, norm_def] using CauSeq.equiv_lim (cauSeq_to_rat_cauSeq f) ε⟩⟩ -end PadicInt - -namespace PadicInt - -variable (p : ℕ) [hp : Fact p.Prime] - theorem exists_pow_neg_lt {ε : ℝ} (hε : 0 < ε) : ∃ k : ℕ, (p : ℝ) ^ (-(k : ℤ)) < ε := by obtain ⟨k, hk⟩ := exists_nat_gt ε⁻¹ use k @@ -329,50 +310,45 @@ theorem norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : /-! ### Valuation on `ℤ_[p]` -/ +lemma valuation_coe_nonneg : 0 ≤ (x : ℚ_[p]).valuation := by + obtain rfl | hx := eq_or_ne x 0 + · simp + have := x.2 + rwa [Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx, zpow_le_one_iff_right₀, neg_nonpos] + at this + exact mod_cast hp.out.one_lt /-- `PadicInt.valuation` lifts the `p`-adic valuation on `ℚ` to `ℤ_[p]`. -/ -def valuation (x : ℤ_[p]) := - Padic.valuation (x : ℚ_[p]) +def valuation (x : ℤ_[p]) : ℕ := (x : ℚ_[p]).valuation.toNat -theorem norm_eq_pow_val {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = (p : ℝ) ^ (-x.valuation) := by - refine @Padic.norm_eq_pow_val p hp x ?_ - contrapose! hx - exact Subtype.val_injective hx +@[simp, norm_cast] lemma valuation_coe (x : ℤ_[p]) : (x : ℚ_[p]).valuation = x.valuation := by + simp [valuation, valuation_coe_nonneg] -@[simp] -theorem valuation_zero : valuation (0 : ℤ_[p]) = 0 := Padic.valuation_zero +@[simp] lemma valuation_zero : valuation (0 : ℤ_[p]) = 0 := by simp [valuation] +@[simp] lemma valuation_one : valuation (1 : ℤ_[p]) = 0 := by simp [valuation] +@[simp] lemma valuation_p : valuation (p : ℤ_[p]) = 1 := by simp [valuation] -@[simp] -theorem valuation_one : valuation (1 : ℤ_[p]) = 0 := Padic.valuation_one +lemma le_valuation_add (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation := by + zify; simpa [← valuation_coe] using Padic.le_valuation_add <| coe_ne_zero.2 hxy + +@[simp] lemma valuation_mul (hx : x ≠ 0) (hy : y ≠ 0) : + (x * y).valuation = x.valuation + y.valuation := by + zify; simp [← valuation_coe, Padic.valuation_mul (coe_ne_zero.2 hx) (coe_ne_zero.2 hy)] @[simp] -theorem valuation_p : valuation (p : ℤ_[p]) = 1 := by simp [valuation] +lemma valuation_pow (x : ℤ_[p]) (n : ℕ) : (x ^ n).valuation = n * x.valuation := by + zify; simp [← valuation_coe] -theorem valuation_nonneg (x : ℤ_[p]) : 0 ≤ x.valuation := by - by_cases hx : x = 0 - · simp [hx] - have h : (1 : ℝ) < p := mod_cast hp.1.one_lt - rw [← neg_nonpos, ← (zpow_right_strictMono₀ h).le_iff_le] - show (p : ℝ) ^ (-valuation x) ≤ (p : ℝ) ^ (0 : ℤ) - rw [← norm_eq_pow_val hx] - simpa using x.property +lemma norm_eq_zpow_neg_valuation {x : ℤ_[p]} (hx : x ≠ 0) : ‖x‖ = p ^ (-x.valuation : ℤ) := by + simp [norm_def, Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx] + +@[deprecated (since := "2024-12-10")] alias norm_eq_pow_val := norm_eq_zpow_neg_valuation +-- TODO: Do we really need this lemma? @[simp] theorem valuation_p_pow_mul (n : ℕ) (c : ℤ_[p]) (hc : c ≠ 0) : ((p : ℤ_[p]) ^ n * c).valuation = n + c.valuation := by - have : ‖(p : ℤ_[p]) ^ n * c‖ = ‖(p : ℤ_[p]) ^ n‖ * ‖c‖ := norm_mul _ _ - have aux : (p : ℤ_[p]) ^ n * c ≠ 0 := by - contrapose! hc - rw [mul_eq_zero] at hc - cases' hc with hc hc - · refine (hp.1.ne_zero ?_).elim - exact_mod_cast pow_eq_zero hc - · exact hc - rwa [norm_eq_pow_val aux, norm_p_pow, norm_eq_pow_val hc, ← zpow_add₀, ← neg_add, - zpow_right_inj₀, neg_inj] at this - · exact mod_cast hp.1.pos - · exact mod_cast hp.1.ne_one - · exact mod_cast hp.1.ne_zero + rw [valuation_mul (NeZero.ne _) hc, valuation_pow, valuation_p, mul_one] section Units @@ -429,25 +405,22 @@ theorem norm_units (u : ℤ_[p]ˣ) : ‖(u : ℤ_[p])‖ = 1 := isUnit_iff.mp <| /-- `unitCoeff hx` is the unit `u` in the unique representation `x = u * p ^ n`. See `unitCoeff_spec`. -/ def unitCoeff {x : ℤ_[p]} (hx : x ≠ 0) : ℤ_[p]ˣ := - let u : ℚ_[p] := x * (p : ℚ_[p]) ^ (-x.valuation) + let u : ℚ_[p] := x * (p : ℚ_[p]) ^ (-x.valuation : ℤ) have hu : ‖u‖ = 1 := by - simp [u, hx, zpow_ne_zero (G₀ := ℝ) _ (Nat.cast_ne_zero.2 hp.1.pos.ne'), norm_eq_pow_val] + simp [u, hx, pow_ne_zero _ (NeZero.ne _), norm_eq_zpow_neg_valuation] mkUnits hu @[simp] theorem unitCoeff_coe {x : ℤ_[p]} (hx : x ≠ 0) : - (unitCoeff hx : ℚ_[p]) = x * (p : ℚ_[p]) ^ (-x.valuation) := rfl + (unitCoeff hx : ℚ_[p]) = x * (p : ℚ_[p]) ^ (-x.valuation : ℤ) := rfl theorem unitCoeff_spec {x : ℤ_[p]} (hx : x ≠ 0) : - x = (unitCoeff hx : ℤ_[p]) * (p : ℤ_[p]) ^ Int.natAbs (valuation x) := by + x = (unitCoeff hx : ℤ_[p]) * (p : ℤ_[p]) ^ x.valuation := by apply Subtype.coe_injective push_cast - have repr : (x : ℚ_[p]) = unitCoeff hx * (p : ℚ_[p]) ^ x.valuation := by - rw [unitCoeff_coe, mul_assoc, ← zpow_add₀] - · simp - · exact mod_cast hp.1.ne_zero - convert repr using 2 - rw [← zpow_natCast, Int.natAbs_of_nonneg (valuation_nonneg x)] + rw [unitCoeff_coe, mul_assoc, ← zpow_natCast, ← zpow_add₀] + · simp + · exact NeZero.ne _ end Units @@ -457,35 +430,22 @@ section NormLeIff theorem norm_le_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : - ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ ↑n ≤ x.valuation := by - rw [norm_eq_pow_val hx] - lift x.valuation to ℕ using x.valuation_nonneg with k - simp only [Int.ofNat_le, zpow_neg, zpow_natCast] - have aux : ∀ m : ℕ, 0 < (p : ℝ) ^ m := by - intro m - refine pow_pos ?_ m - exact mod_cast hp.1.pos - rw [inv_le_inv₀ (aux _) (aux _)] - have : p ^ n ≤ p ^ k ↔ n ≤ k := (pow_right_strictMono₀ hp.1.one_lt).le_iff_le - rw [← this] - norm_cast + ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ n ≤ x.valuation := by + rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le] + exact mod_cast hp.out.one_lt theorem mem_span_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : - x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) ↔ ↑n ≤ x.valuation := by + x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) ↔ n ≤ x.valuation := by rw [Ideal.mem_span_singleton] constructor · rintro ⟨c, rfl⟩ suffices c ≠ 0 by - rw [valuation_p_pow_mul _ _ this, le_add_iff_nonneg_right] - apply valuation_nonneg + rw [valuation_p_pow_mul _ _ this] + exact le_self_add contrapose! hx rw [hx, mul_zero] · nth_rewrite 2 [unitCoeff_spec hx] - lift x.valuation to ℕ using x.valuation_nonneg with k - simp only [Int.natAbs_ofNat, Units.isUnit, IsUnit.dvd_mul_left, Int.ofNat_le] - intro H - obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le H - simp only [pow_add, dvd_mul_right] + simpa [Units.isUnit, IsUnit.dvd_mul_left] using pow_dvd_pow _ theorem norm_le_pow_iff_mem_span_pow (x : ℤ_[p]) (n : ℕ) : ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) := by @@ -525,7 +485,7 @@ instance : IsLocalRing ℤ_[p] := IsLocalRing.of_nonunits_add <| by simp only [mem_nonunits]; exact fun x y => norm_lt_one_add theorem p_nonnunit : (p : ℤ_[p]) ∈ nonunits ℤ_[p] := by - have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt + have : (p : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ <| mod_cast hp.out.one_lt rwa [← norm_p, ← mem_nonunits] at this theorem maximalIdeal_eq_span_p : maximalIdeal ℤ_[p] = Ideal.span {(p : ℤ_[p])} := by @@ -539,14 +499,14 @@ theorem maximalIdeal_eq_span_p : maximalIdeal ℤ_[p] = Ideal.span {(p : ℤ_[p] theorem prime_p : Prime (p : ℤ_[p]) := by rw [← Ideal.span_singleton_prime, ← maximalIdeal_eq_span_p] · infer_instance - · exact mod_cast hp.1.ne_zero + · exact NeZero.ne _ theorem irreducible_p : Irreducible (p : ℤ_[p]) := Prime.irreducible prime_p instance : IsDiscreteValuationRing ℤ_[p] := IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization ⟨p, irreducible_p, fun {x hx} => - ⟨x.valuation.natAbs, unitCoeff hx, by rw [mul_comm, ← unitCoeff_spec hx]⟩⟩ + ⟨x.valuation, unitCoeff hx, by rw [mul_comm, ← unitCoeff_spec hx]⟩⟩ theorem ideal_eq_span_pow_p {s : Ideal ℤ_[p]} (hs : s ≠ ⊥) : ∃ n : ℕ, s = Ideal.span {(p : ℤ_[p]) ^ n} := @@ -565,9 +525,7 @@ instance : IsAdicComplete (maximalIdeal ℤ_[p]) ℤ_[p] where rw [← neg_sub, norm_neg] exact hx hn · refine ⟨x'.lim, fun n => ?_⟩ - have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := by - apply zpow_pos - exact mod_cast hp.1.pos + have : (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) := zpow_pos (mod_cast hp.out.pos) _ obtain ⟨i, hi⟩ := equiv_def₃ (equiv_lim x') this by_cases hin : i ≤ n · exact (hi i le_rfl n hin).le @@ -609,8 +567,8 @@ instance isFractionRing : IsFractionRing ℤ_[p] ℚ_[p] where intro h0 rw [h0, norm_zero] at hx exact hx zero_le_one - rw [ha, padicNormE.mul, padicNormE.norm_p_pow, Padic.norm_eq_pow_val hx, ← zpow_add', - hn_coe, neg_neg, neg_add_cancel, zpow_zero] + rw [ha, padicNormE.mul, padicNormE.norm_p_pow, Padic.norm_eq_zpow_neg_valuation hx, + ← zpow_add', hn_coe, neg_neg, neg_add_cancel, zpow_zero] exact Or.inl (Nat.cast_ne_zero.mpr (NeZero.ne p)) use (⟨a, le_of_eq ha_norm⟩, diff --git a/Mathlib/NumberTheory/Padics/PadicNumbers.lean b/Mathlib/NumberTheory/Padics/PadicNumbers.lean index 7e461266cf61d..e961a395e031e 100644 --- a/Mathlib/NumberTheory/Padics/PadicNumbers.lean +++ b/Mathlib/NumberTheory/Padics/PadicNumbers.lean @@ -199,7 +199,8 @@ open Classical in def valuation (f : PadicSeq p) : ℤ := if hf : f ≈ 0 then 0 else padicValRat p (f (stationaryPoint hf)) -theorem norm_eq_pow_val {f : PadicSeq p} (hf : ¬f ≈ 0) : f.norm = (p : ℚ) ^ (-f.valuation : ℤ) := by +theorem norm_eq_zpow_neg_valuation {f : PadicSeq p} (hf : ¬f ≈ 0) : + f.norm = (p : ℚ) ^ (-f.valuation : ℤ) := by rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg] intro H apply CauSeq.not_limZero_of_not_congr_zero hf @@ -209,9 +210,11 @@ theorem norm_eq_pow_val {f : PadicSeq p} (hf : ¬f ≈ 0) : f.norm = (p : ℚ) ^ rw [stationaryPoint_spec hf le_rfl hn] simpa [H] using hε +@[deprecated (since := "2024-12-10")] alias norm_eq_pow_val := norm_eq_zpow_neg_valuation + theorem val_eq_iff_norm_eq {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0) : f.valuation = g.valuation ↔ f.norm = g.norm := by - rw [norm_eq_pow_val hf, norm_eq_pow_val hg, ← neg_inj, zpow_right_inj₀] + rw [norm_eq_zpow_neg_valuation hf, norm_eq_zpow_neg_valuation hg, ← neg_inj, zpow_right_inj₀] · exact mod_cast (Fact.out : p.Prime).pos · exact mod_cast (Fact.out : p.Prime).ne_one @@ -945,10 +948,10 @@ def valuation : ℚ_[p] → ℤ := theorem valuation_zero : valuation (0 : ℚ_[p]) = 0 := dif_pos ((const_equiv p).2 rfl) -theorem norm_eq_pow_val {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = (p : ℝ) ^ (-x.valuation) := by +theorem norm_eq_zpow_neg_valuation {x : ℚ_[p]} : x ≠ 0 → ‖x‖ = (p : ℝ) ^ (-x.valuation) := by refine Quotient.inductionOn' x fun f hf => ?_ change (PadicSeq.norm _ : ℝ) = (p : ℝ) ^ (-PadicSeq.valuation _) - rw [PadicSeq.norm_eq_pow_val] + rw [PadicSeq.norm_eq_zpow_neg_valuation] · change ↑((p : ℚ) ^ (-PadicSeq.valuation f)) = (p : ℝ) ^ (-PadicSeq.valuation f) rw [Rat.cast_zpow, Rat.cast_natCast] · apply CauSeq.not_limZero_of_not_congr_zero @@ -963,7 +966,7 @@ lemma valuation_ratCast (q : ℚ) : valuation (q : ℚ_[p]) = padicValRat p q := rcases eq_or_ne q 0 with rfl | hq · simp only [Rat.cast_zero, valuation_zero, padicValRat.zero] refine neg_injective ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective - <| (norm_eq_pow_val (mod_cast hq)).symm.trans ?_) + <| (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_) rw [padicNormE.eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj] exact padicNorm.eq_zpow_of_nonzero hq @@ -989,29 +992,52 @@ lemma valuation_one : valuation (1 : ℚ_[p]) = 0 := by lemma valuation_p : valuation (p : ℚ_[p]) = 1 := by rw [valuation_natCast, padicValNat_self, cast_one] -theorem valuation_map_add {x y : ℚ_[p]} (hxy : x + y ≠ 0) : - min (valuation x) (valuation y) ≤ valuation (x + y : ℚ_[p]) := by +theorem le_valuation_add {x y : ℚ_[p]} (hxy : x + y ≠ 0) : + min x.valuation y.valuation ≤ (x + y).valuation := by by_cases hx : x = 0 · simpa only [hx, zero_add] using min_le_right _ _ by_cases hy : y = 0 · simpa only [hy, add_zero] using min_le_left _ _ have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := padicNormE.nonarchimedean x y - simpa only [norm_eq_pow_val hxy, norm_eq_pow_val hx, norm_eq_pow_val hy, le_max_iff, + simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx, + norm_eq_zpow_neg_valuation hy, le_max_iff, zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff] @[simp] -theorem valuation_map_mul {x y : ℚ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) : - valuation (x * y : ℚ_[p]) = valuation x + valuation y := by +lemma valuation_mul {x y : ℚ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) : + (x * y).valuation = x.valuation + y.valuation := by have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y - have hp_ne_one : (p : ℝ) ≠ 1 := by - rw [← Nat.cast_one, Ne, Nat.cast_inj] - exact Nat.Prime.ne_one hp.elim - have hp_pos : (0 : ℝ) < p := by - rw [← Nat.cast_zero, Nat.cast_lt] - exact Nat.Prime.pos hp.elim - rw [norm_eq_pow_val hx, norm_eq_pow_val hy, norm_eq_pow_val (mul_ne_zero hx hy), ← - zpow_add₀ (ne_of_gt hp_pos), zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm - exact h_norm + have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one + have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _ + rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy, + norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne', + zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm + +@[simp] +lemma valuation_inv (x : ℚ_[p]) : x⁻¹.valuation = -x.valuation := by + obtain rfl | hx := eq_or_ne x 0 + · simp + have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x + have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one + have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _ + rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx, + ← zpow_neg, zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm + +@[simp] +lemma valuation_pow (x : ℚ_[p]) : ∀ n : ℕ, (x ^ n).valuation = n * x.valuation + | 0 => by simp + | n + 1 => by + obtain rfl | hx := eq_or_ne x 0 + · simp + · simp [pow_succ, hx, valuation_mul, valuation_pow, _root_.add_one_mul] + +@[simp] +lemma valuation_zpow (x : ℚ_[p]) : ∀ n : ℤ, (x ^ n).valuation = n * x.valuation + | (n : ℕ) => by simp + | .negSucc n => by simp [← neg_mul]; simp [Int.negSucc_eq] + +@[deprecated (since := "2024-12-10")] alias valuation_map_add := le_valuation_add +@[deprecated (since := "2024-12-10")] alias valuation_map_mul := valuation_mul open Classical in /-- The additive `p`-adic valuation on `ℚ_[p]`, with values in `WithTop ℤ`. -/ @@ -1034,7 +1060,7 @@ theorem AddValuation.map_mul (x y : ℚ_[p]) : · by_cases hy : y = 0 · rw [hy, if_pos rfl, mul_zero, if_pos rfl, WithTop.add_top] · rw [if_neg hx, if_neg hy, if_neg (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe, - valuation_map_mul hx hy] + valuation_mul hx hy] theorem AddValuation.map_add (x y : ℚ_[p]) : min (addValuationDef x) (addValuationDef y) ≤ addValuationDef (x + y : ℚ_[p]) := by @@ -1049,7 +1075,7 @@ theorem AddValuation.map_add (x y : ℚ_[p]) : · rw [hy, if_pos rfl, min_eq_left, add_zero] exact le_top · rw [if_neg hx, if_neg hy, if_neg hxy, ← WithTop.coe_min, WithTop.coe_le_coe] - exact valuation_map_add hxy + exact le_valuation_add hxy /-- The additive `p`-adic valuation on `ℚ_[p]`, as an `addValuation`. -/ def addValuation : AddValuation ℚ_[p] (WithTop ℤ) := @@ -1071,7 +1097,7 @@ theorem norm_le_pow_iff_norm_lt_pow_add_one (x : ℚ_[p]) (n : ℤ) : have aux (n : ℤ) : 0 < ((p : ℝ) ^ n) := zpow_pos (mod_cast hp.1.pos) _ by_cases hx0 : x = 0 · simp [hx0, norm_zero, aux, le_of_lt (aux _)] - rw [norm_eq_pow_val hx0] + rw [norm_eq_zpow_neg_valuation hx0] have h1p : 1 < (p : ℝ) := mod_cast hp.1.one_lt have H := zpow_right_strictMono₀ h1p rw [H.le_iff_le, H.lt_iff_lt, Int.lt_add_one_iff] @@ -1083,7 +1109,7 @@ theorem norm_lt_pow_iff_norm_le_pow_sub_one (x : ℚ_[p]) (n : ℤ) : theorem norm_le_one_iff_val_nonneg (x : ℚ_[p]) : ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation := by by_cases hx : x = 0 · simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl] - · rw [norm_eq_pow_val hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, Right.neg_nonpos_iff] + · rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos] exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1 end NormLEIff diff --git a/Mathlib/NumberTheory/Padics/RingHoms.lean b/Mathlib/NumberTheory/Padics/RingHoms.lean index aabd86ef8f646..f16855f13878b 100644 --- a/Mathlib/NumberTheory/Padics/RingHoms.lean +++ b/Mathlib/NumberTheory/Padics/RingHoms.lean @@ -303,7 +303,7 @@ noncomputable def appr : ℤ_[p] → ℕ → ℕ if hy : y = 0 then appr x n else let u := (unitCoeff hy : ℤ_[p]) - appr x n + p ^ n * (toZMod ((u * (p : ℤ_[p]) ^ (y.valuation - n).natAbs) : ℤ_[p])).val + appr x n + p ^ n * (toZMod ((u * (p : ℤ_[p]) ^ (y.valuation - n : ℤ).natAbs) : ℤ_[p])).val theorem appr_lt (x : ℤ_[p]) (n : ℕ) : x.appr n < p ^ n := by induction' n with n ih generalizing x @@ -364,21 +364,18 @@ theorem appr_spec (n : ℕ) : ∀ x : ℤ_[p], x - appr x n ∈ Ideal.span {(p : congr simp only [hc] rw [show (x - (appr x n : ℤ_[p])).valuation = ((p : ℤ_[p]) ^ n * c).valuation by rw [hc]] - rw [valuation_p_pow_mul _ _ hc', add_sub_cancel_left, _root_.pow_succ, ← mul_sub] + rw [valuation_p_pow_mul _ _ hc', Nat.cast_add, add_sub_cancel_left, _root_.pow_succ, ← mul_sub] apply mul_dvd_mul_left - obtain hc0 | hc0 := eq_or_ne c.valuation.natAbs 0 - · simp only [hc0, mul_one, _root_.pow_zero] + obtain hc0 | hc0 := eq_or_ne c.valuation 0 + · simp only [hc0, mul_one, _root_.pow_zero, Nat.cast_zero, Int.natAbs_zero] rw [mul_comm, unitCoeff_spec h] at hc suffices c = unitCoeff h by rw [← this, ← Ideal.mem_span_singleton, ← maximalIdeal_eq_span_p] apply toZMod_spec - obtain ⟨c, rfl⟩ : IsUnit c := by - -- TODO: write a `CanLift` instance for units - rw [Int.natAbs_eq_zero] at hc0 - rw [isUnit_iff, norm_eq_pow_val hc', hc0, neg_zero, zpow_zero] + lift c to ℤ_[p]ˣ using by simp [isUnit_iff, norm_eq_zpow_neg_valuation hc', hc0] rw [IsDiscreteValuationRing.unit_mul_pow_congr_unit _ _ _ _ _ hc] exact irreducible_p - · simp only [zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero] + · simp only [Int.natAbs_ofNat, zero_pow hc0, sub_zero, ZMod.cast_zero, mul_zero] rw [unitCoeff_spec hc'] exact (dvd_pow_self (p : ℤ_[p]) hc0).mul_left _