From 570e9f4877079b3a923135b3027ac3be8695ab8c Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Thu, 4 May 2023 13:44:28 +0000 Subject: [PATCH] feat(ring_theory/localization/away) : Add `num_denom` section (#18830) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- src/ring_theory/localization/away.lean | 142 ++++++++++++++++++ .../unique_factorization_domain.lean | 28 +++- 2 files changed, 162 insertions(+), 8 deletions(-) diff --git a/src/ring_theory/localization/away.lean b/src/ring_theory/localization/away.lean index 39d04cb19893d..0ea25713791eb 100644 --- a/src/ring_theory/localization/away.lean +++ b/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 diff --git a/src/ring_theory/unique_factorization_domain.lean b/src/ring_theory/unique_factorization_domain.lean index 471af7ef520d2..d4c443fe63a91 100644 --- a/src/ring_theory/unique_factorization_domain.lean +++ b/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