feat(ring_theory/localization/away) : Add num_denom section (#18830)

Added a section `num_denom`: the main result is the lemma `exists_reduced_fraction` that shows that every non-zero element `b` in a `localization.away x` of a UFM can be written in a unique way as `b=x^n * a` with `n : ℤ` and `a` not divisible by `x`.



Co-authored-by: Vierkantor <[email protected]>

src/ring_theory/localization/away.lean

@@ -13,6 +13,8 @@ import ring_theory.localization.basic
 
  * `is_localization.away (x : R) S` expresses that `S` is a localization away from `x`, as an
    abbreviation of `is_localization (submonoid.powers x) S`
+ * `exists_reduced_fraction (hb : b ≠ 0)` produces a reduced fraction of the form `b = a * x^n` for
+   some `n : ℤ` and some `a : R` that is not divisible by `x`.
 
 ## Implementation notes
 
@@ -194,3 +196,143 @@ lemma is_localization.away.finite_presentation (r : R) {S} [comm_ring S] [algebr
   [is_localization.away r S] : algebra.finite_presentation R S :=
 (adjoin_root.finite_presentation _).equiv $ (localization.away_equiv_adjoin r).symm.trans $
   is_localization.alg_equiv (submonoid.powers r) _ _
+
+section num_denom
+
+open multiplicity unique_factorization_monoid is_localization
+
+variable (x : R)
+
+variables (B : Type*) [comm_ring B] [algebra R B] [is_localization.away x B]
+
+/-- `self_zpow x (m : ℤ)` is `x ^ m` as an element of the localization away from `x`. -/
+noncomputable def self_zpow (m : ℤ) : B :=
+if hm : 0 ≤ m
+then algebra_map _ _ x ^ m.nat_abs
+else mk' _ (1 : R) (submonoid.pow x m.nat_abs)
+
+lemma self_zpow_of_nonneg {n : ℤ} (hn : 0 ≤ n) : self_zpow x B n =
+  algebra_map R B x ^ n.nat_abs :=
+dif_pos hn
+
+@[simp] lemma self_zpow_coe_nat (d : ℕ) : self_zpow x B d = (algebra_map R B x)^d :=
+self_zpow_of_nonneg _ _ (int.coe_nat_nonneg d)
+
+@[simp] lemma self_zpow_zero : self_zpow x B 0 = 1 :=
+by simp [self_zpow_of_nonneg _ _ le_rfl]
+
+lemma self_zpow_of_neg {n : ℤ} (hn : n < 0) :
+  self_zpow x B n = mk' _ (1 : R) (submonoid.pow x n.nat_abs) :=
+dif_neg hn.not_le
+
+lemma self_zpow_of_nonpos {n : ℤ} (hn : n ≤ 0) :
+  self_zpow x B n = mk' _ (1 : R) (submonoid.pow x n.nat_abs) :=
+begin
+  by_cases hn0 : n = 0,
+  { simp [hn0, self_zpow_zero, submonoid.pow_apply] },
+  { simp [self_zpow_of_neg _ _ (lt_of_le_of_ne hn hn0)] }
+end
+
+@[simp] lemma self_zpow_neg_coe_nat (d : ℕ) :
+  self_zpow x B (-d) = mk' _ (1 : R) (submonoid.pow x d) :=
+by simp [self_zpow_of_nonpos _ _ (neg_nonpos.mpr (int.coe_nat_nonneg d))]
+
+@[simp] lemma self_zpow_sub_cast_nat {n m : ℕ} :
+  self_zpow x B (n - m) = mk' _ (x ^ n) (submonoid.pow x m) :=
+begin
+  by_cases h : m ≤ n,
+  { rw [is_localization.eq_mk'_iff_mul_eq, submonoid.pow_apply, subtype.coe_mk,
+        ← int.coe_nat_sub h, self_zpow_coe_nat, ← map_pow, ← map_mul, ← pow_add,
+        nat.sub_add_cancel h] },
+  { rw [← neg_sub, ← int.coe_nat_sub (le_of_not_le h), self_zpow_neg_coe_nat,
+        is_localization.mk'_eq_iff_eq],
+    simp [submonoid.pow_apply, ← pow_add, nat.sub_add_cancel (le_of_not_le h)] }
+end
+
+@[simp] lemma self_zpow_add {n m : ℤ} :
+  self_zpow x B (n + m) = self_zpow x B n * self_zpow x B m :=
+begin
+  cases le_or_lt 0 n with hn hn; cases le_or_lt 0 m with hm hm,
+  { rw [self_zpow_of_nonneg _ _ hn, self_zpow_of_nonneg _ _ hm,
+        self_zpow_of_nonneg _ _ (add_nonneg hn hm), int.nat_abs_add_nonneg hn hm, pow_add] },
+  { have : n + m = n.nat_abs - m.nat_abs,
+    { rw [int.nat_abs_of_nonneg hn, int.of_nat_nat_abs_of_nonpos hm.le, sub_neg_eq_add] },
+    rw [self_zpow_of_nonneg _ _ hn, self_zpow_of_neg _ _ hm,
+        this, self_zpow_sub_cast_nat, is_localization.mk'_eq_mul_mk'_one, map_pow] },
+  { have : n + m = m.nat_abs - n.nat_abs,
+    { rw [int.nat_abs_of_nonneg hm, int.of_nat_nat_abs_of_nonpos hn.le, sub_neg_eq_add, add_comm] },
+    rw [self_zpow_of_nonneg _ _ hm, self_zpow_of_neg _ _ hn,
+        this, self_zpow_sub_cast_nat, is_localization.mk'_eq_mul_mk'_one, map_pow, mul_comm] },
+  { rw [self_zpow_of_neg _ _ hn, self_zpow_of_neg _ _ hm, self_zpow_of_neg _ _ (add_neg hn hm),
+        int.nat_abs_add_neg hn hm, ← mk'_mul, one_mul],
+    congr,
+    ext,
+    simp [pow_add] },
+end
+
+lemma self_zpow_mul_neg (d : ℤ) : self_zpow x B d * self_zpow x B (-d) = 1 :=
+begin
+  by_cases hd : d ≤ 0,
+  { erw [self_zpow_of_nonpos x B hd, self_zpow_of_nonneg, ← map_pow, int.nat_abs_neg,
+      is_localization.mk'_spec, map_one],
+    apply nonneg_of_neg_nonpos,
+    rwa [neg_neg]},
+  { erw [self_zpow_of_nonneg x B (le_of_not_le hd), self_zpow_of_nonpos, ← map_pow, int.nat_abs_neg,
+     @is_localization.mk'_spec' R _ (submonoid.powers x) B _ _ _ 1 (submonoid.pow x d.nat_abs),
+      map_one],
+    refine nonpos_of_neg_nonneg (le_of_lt _),
+    rwa [neg_neg, ← not_le] },
+end
+
+lemma self_zpow_neg_mul (d : ℤ) : self_zpow x B (-d) * self_zpow x B d = 1 :=
+by rw [mul_comm, self_zpow_mul_neg x B d]
+
+
+lemma self_zpow_pow_sub (a : R) (b : B) (m d : ℤ) :
+  (self_zpow x B (m - d)) * mk' B a (1 : submonoid.powers x) = b ↔
+  (self_zpow x B m) * mk' B a (1 : submonoid.powers x) = (self_zpow x B d) * b :=
+begin
+  rw [sub_eq_add_neg, self_zpow_add, mul_assoc, mul_comm _ (mk' B a 1), ← mul_assoc],
+  split,
+  { intro h,
+    have := congr_arg (λ s : B, s * self_zpow x B d) h,
+    simp only at this,
+    rwa [mul_assoc, mul_assoc, self_zpow_neg_mul, mul_one, mul_comm b _] at this},
+  { intro h,
+    have := congr_arg (λ s : B, s * self_zpow x B (-d)) h,
+    simp only at this,
+    rwa [mul_comm _ b, mul_assoc b _ _, self_zpow_mul_neg, mul_one] at this}
+end
+
+
+variables [is_domain R] [normalization_monoid R] [unique_factorization_monoid R]
+
+
+theorem exists_reduced_fraction' {b : B} (hb : b ≠ 0) (hx : irreducible x) :
+  ∃ (a : R) (n : ℤ), ¬ x ∣ a ∧
+    self_zpow x B n * algebra_map R B a = b :=
+begin
+  classical,
+  obtain ⟨⟨a₀, y⟩, H⟩ := surj (submonoid.powers x) b,
+  obtain ⟨d, hy⟩ := (submonoid.mem_powers_iff y.1 x).mp y.2,
+  have ha₀ : a₀ ≠ 0,
+  { haveI := @is_domain_of_le_non_zero_divisors B _ R _ _ _ (submonoid.powers x) _
+      (powers_le_non_zero_divisors_of_no_zero_divisors hx.ne_zero),
+    simp only [map_zero, ← subtype.val_eq_coe, ← hy, map_pow] at H,
+    apply ((injective_iff_map_eq_zero' (algebra_map R B)).mp _ a₀).mpr.mt,
+    rw ← H,
+    apply mul_ne_zero hb (pow_ne_zero _ _),
+    exact is_localization.to_map_ne_zero_of_mem_non_zero_divisors B
+      (powers_le_non_zero_divisors_of_no_zero_divisors (hx.ne_zero))
+      (mem_non_zero_divisors_iff_ne_zero.mpr hx.ne_zero),
+    exact is_localization.injective B (powers_le_non_zero_divisors_of_no_zero_divisors
+      (hx.ne_zero)) },
+  simp only [← subtype.val_eq_coe, ← hy] at H,
+  obtain ⟨m, a, hyp1, hyp2⟩ := max_power_factor ha₀ hx,
+  refine ⟨a, m-d, _⟩,
+  rw [← mk'_one B, self_zpow_pow_sub, self_zpow_coe_nat, self_zpow_coe_nat, ← map_pow _ _ d,
+    mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m],
+  exact ⟨hyp1, (congr_arg _ (is_localization.mk'_one _ _))⟩,
+end
+
+end num_denom

src/ring_theory/unique_factorization_domain.lean

@@ -863,12 +863,12 @@ lemma pow_eq_pow_iff {a : R} (ha0 : a ≠ 0) (ha1 : ¬ is_unit a) {i j : ℕ} :
 (pow_right_injective ha0 ha1).eq_iff
 
 section multiplicity
-variables [nontrivial R] [normalization_monoid R] [decidable_eq R]
+variables [nontrivial R] [normalization_monoid R]
 variables [dec_dvd : decidable_rel (has_dvd.dvd : R → R → Prop)]
 open multiplicity multiset
 
 include dec_dvd
-lemma le_multiplicity_iff_replicate_le_normalized_factors {a b : R} {n : ℕ}
+lemma le_multiplicity_iff_replicate_le_normalized_factors [decidable_eq R] {a b : R} {n : ℕ}
   (ha : irreducible a) (hb : b ≠ 0) :
   ↑n ≤ multiplicity a b ↔ replicate n (normalize a) ≤ normalized_factors b :=
 begin
@@ -894,8 +894,8 @@ the normalized factor occurs in the `normalized_factors`.
 See also `count_normalized_factors_eq` which expands the definition of `multiplicity`
 to produce a specification for `count (normalized_factors _) _`..
 -/
-lemma multiplicity_eq_count_normalized_factors {a b : R} (ha : irreducible a) (hb : b ≠ 0) :
-  multiplicity a b = (normalized_factors b).count (normalize a) :=
+lemma multiplicity_eq_count_normalized_factors [decidable_eq R] {a b : R} (ha : irreducible a)
+ (hb : b ≠ 0) : multiplicity a b = (normalized_factors b).count (normalize a) :=
 begin
   apply le_antisymm,
   { apply part_enat.le_of_lt_add_one,
@@ -912,8 +912,8 @@ the number of times it divides `x`.
 
 See also `multiplicity_eq_count_normalized_factors` if `n` is given by `multiplicity p x`.
 -/
-lemma count_normalized_factors_eq {p x : R} (hp : irreducible p) (hnorm : normalize p = p) {n : ℕ}
-  (hle : p^n ∣ x) (hlt : ¬ (p^(n+1) ∣ x)) :
+lemma count_normalized_factors_eq [decidable_eq R] {p x : R} (hp : irreducible p)
+  (hnorm : normalize p = p) {n : ℕ} (hle : p^n ∣ x) (hlt : ¬ (p^(n+1) ∣ x)) :
   (normalized_factors x).count p = n :=
 begin
   letI : decidable_rel ((∣) : R → R → Prop) := λ _ _, classical.prop_decidable _,
@@ -931,8 +931,8 @@ the number of times it divides `x`. This is a slightly more general version of
 
 See also `multiplicity_eq_count_normalized_factors` if `n` is given by `multiplicity p x`.
 -/
-lemma count_normalized_factors_eq' {p x : R} (hp : p = 0 ∨ irreducible p) (hnorm : normalize p = p)
-  {n : ℕ} (hle : p^n ∣ x) (hlt : ¬ (p^(n+1) ∣ x)) :
+lemma count_normalized_factors_eq' [decidable_eq R] {p x : R} (hp : p = 0 ∨ irreducible p)
+  (hnorm : normalize p = p) {n : ℕ} (hle : p^n ∣ x) (hlt : ¬ (p^(n+1) ∣ x)) :
   (normalized_factors x).count p = n :=
 begin
   rcases hp with rfl|hp,
@@ -943,6 +943,18 @@ begin
   { exact count_normalized_factors_eq hp hnorm hle hlt }
 end
 
+lemma max_power_factor {a₀ : R} {x : R} (h : a₀ ≠ 0) (hx : irreducible x) :
+  ∃ n : ℕ, ∃ a : R, ¬ x ∣ a ∧ a₀ = x ^ n * a :=
+begin
+  classical,
+  let n := (normalized_factors a₀).count (normalize x),
+  obtain ⟨a, ha1, ha2⟩ := (@exists_eq_pow_mul_and_not_dvd R _ _ x a₀
+    (ne_top_iff_finite.mp (part_enat.ne_top_iff.mpr _))),
+  simp_rw [← (multiplicity_eq_count_normalized_factors hx h).symm] at ha1,
+  use [n, a, ha2, ha1],
+  use [n, (multiplicity_eq_count_normalized_factors hx h)],
+end
+
 end multiplicity
 
 section multiplicative