Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued #19858

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - refactor: make PadicInt.valuation ℕ-valued #19858

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 4 additions & 3 deletions Mathlib/NumberTheory/Padics/MahlerBasis.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ ↦ ?_)
Expand Down
150 changes: 54 additions & 96 deletions Mathlib/NumberTheory/Padics/PadicIntegers.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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⟩

Expand Down Expand Up @@ -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))

Expand Down Expand Up @@ -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
Expand All @@ -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

Expand Down Expand Up @@ -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]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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} :=
Expand All @@ -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
Expand Down Expand Up @@ -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⟩,
Expand Down
Loading
Loading