feat(number_theory/padics/padic_numbers): add is_fraction_ring instance (#16981)

`ℚ_[p]` is the fraction ring of `ℤ_[p]`.

Author: mariainesdff

src/number_theory/padics/padic_integers.lean

@@ -112,6 +112,9 @@ instance : has_one ℤ_[p] := ⟨⟨1, by norm_num⟩⟩
 @[simp, norm_cast] lemma coe_one : ((1 : ℤ_[p]) : ℚ_[p]) = 1 := rfl
 @[simp, norm_cast] lemma coe_zero : ((0 : ℤ_[p]) : ℚ_[p]) = 0 := rfl
 
+lemma coe_eq_zero (z : ℤ_[p]) : (z : ℚ_[p]) = 0 ↔ z = 0 :=
+⟨λ h, by {rw ← coe_zero at h, exact subtype.coe_inj.mp h}, λ h, by {rw h, exact coe_zero}⟩
+
 instance : add_comm_group ℤ_[p] :=
 (by apply_instance : add_comm_group (subring p))
 
@@ -531,4 +534,52 @@ instance : is_adic_complete (maximal_ideal ℤ_[p]) ℤ_[p] :=
 
 end dvr
 
+section fraction_ring
+
+instance algebra : algebra ℤ_[p] ℚ_[p] := ring_hom.to_algebra (padic_int.coe.ring_hom)
+
+@[simp] lemma algebra_map_apply (x : ℤ_[p]) : algebra_map ℤ_[p] ℚ_[p] x = x := rfl
+
+instance is_fraction_ring : is_fraction_ring ℤ_[p] ℚ_[p] :=
+{ map_units := λ ⟨x, hx⟩,
+  begin
+    rw [set_like.coe_mk, algebra_map_apply, is_unit_iff_ne_zero, ne.def, padic_int.coe_eq_zero],
+    exact mem_non_zero_divisors_iff_ne_zero.mp hx,
+  end,
+  surj := λ x,
+  begin
+    by_cases hx : ∥ x ∥ ≤ 1,
+    { use (⟨x, hx⟩, 1),
+      rw [submonoid.coe_one, map_one, mul_one],
+      refl, },
+    { set n := int.to_nat(- x.valuation) with hn,
+      have hn_coe : (n : ℤ) = -x.valuation,
+      { rw [hn, int.to_nat_of_nonneg],
+        rw right.nonneg_neg_iff,
+        rw padic.norm_le_one_iff_val_nonneg at hx,
+        exact le_of_lt (not_le.mp hx) },
+      set a := x * p^n with ha,
+      have ha_norm : ∥ a ∥ = 1,
+      { have hx : x ≠ 0,
+        { intro h0,
+          rw [h0, norm_zero] at hx,
+          exact hx (zero_le_one) },
+          rw [ha, padic_norm_e.mul, ← zpow_coe_nat, padic_norm_e.norm_p_pow,
+            padic.norm_eq_pow_val hx, ← zpow_add' , hn_coe, neg_neg, add_left_neg, zpow_zero],
+          exact or.inl (nat.cast_ne_zero.mpr (ne_zero.ne p)), },
+      use (⟨a, le_of_eq ha_norm⟩,
+        ⟨(p^n : ℤ_[p]), mem_non_zero_divisors_iff_ne_zero.mpr (ne_zero.ne _)⟩),
+      simp only [set_like.coe_mk, map_pow, map_nat_cast, algebra_map_apply,
+        padic_int.coe_pow, padic_int.coe_nat_cast, subtype.coe_mk] }
+  end,
+  eq_iff_exists := λ x y,
+  begin
+    rw [algebra_map_apply, algebra_map_apply, subtype.coe_inj],
+    refine ⟨λ h, ⟨1, by rw h⟩, _⟩,
+    rintro ⟨⟨c, hc⟩, h⟩,
+    exact (mul_eq_mul_right_iff.mp h).resolve_right (mem_non_zero_divisors_iff_ne_zero.mp hc)
+  end }
+
+end fraction_ring
+
 end padic_int

src/number_theory/padics/padic_numbers.lean

@@ -1021,5 +1021,14 @@ end
 lemma norm_lt_pow_iff_norm_le_pow_sub_one (x : ℚ_[p]) (n : ℤ) : ∥x∥ < p ^ n ↔ ∥x∥ ≤ p ^ (n - 1) :=
 by rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]
 
+lemma norm_le_one_iff_val_nonneg (x : ℚ_[p]) : ∥ x ∥ ≤ 1 ↔ 0 ≤ x.valuation :=
+begin
+  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_iff_le
+      (nat.one_lt_cast.mpr (nat.prime.one_lt' p).1), right.neg_nonpos_iff],
+    apply_instance, }
+end
+
 end norm_le_iff
 end padic