refactor(ring_theory/unique_factorization_domain): completes the refa…

…ctor of `unique_factorization_domain` (#4156)

Refactors `unique_factorization_domain` to `unique_factorization_monoid`
`unique_factorization_monoid` is a predicate
`unique_factorization_monoid` now requires no additive/subtractive structure




Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>

docs/100.yaml

@@ -271,8 +271,8 @@
     - nat.factors_unique
     - int.euclidean_domain
     - euclidean_domain.to_principal_ideal_domain
-    - unique_factorization_domain
-    - unique_factorization_domain.unique
+    - unique_factorization_monoid
+    - unique_factorization_monoid.factors_unique
   author : mathlib (Chris Hughes)
   note   : "it also has a generalized version, by showing that every Euclidean domain is a unique factorization domain, and showing that the integers form a Euclidean domain."
 81:

docs/overview.yaml

@@ -63,7 +63,7 @@ General algebra:
   Divisibility in integral domains:
     irreducible elements: 'irreducible'
     coprime elements: 'is_coprime'
-    unique factorisation domain: 'unique_factorization_domain'
+    unique factorisation domain: 'unique_factorization_monoid'
     greatest common divisor: 'gcd_monoid.gcd'
     least common multiple: 'gcd_monoid.lcm'
     principal ideal domain: 'submodule.is_principal'

scripts/nolints.txt

@@ -1848,4 +1848,4 @@ apply_nolint uniform_space.completion.map₂ doc_blame
 
 -- topology/uniform_space/uniform_embedding.lean
 apply_nolint uniform_embedding doc_blame
-apply_nolint uniform_inducing doc_blame
+apply_nolint uniform_inducing doc_blame

src/algebra/associated.lean

@@ -632,11 +632,6 @@ instance : no_zero_divisors (associates α) :=
     have a = 0 ∨ b = 0, from mul_eq_zero.1 this,
     this.imp (assume h, h.symm ▸ rfl) (assume h, h.symm ▸ rfl))⟩
 
-theorem prod_eq_zero_iff [nontrivial α] {s : multiset (associates α)} :
-  s.prod = 0 ↔ (0 : associates α) ∈ s :=
-multiset.induction_on s (by simp) $
-  assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
-
 theorem irreducible_iff_prime_iff :
   (∀ a : α, irreducible a ↔ prime a) ↔ (∀ a : (associates α), irreducible a ↔ prime a) :=
 begin

src/algebra/gcd_monoid.lean

@@ -78,14 +78,17 @@ def normalize : α →* α :=
   classical.by_cases (λ hy : y = 0, by rw [hy, mul_zero, zero_mul, mul_zero]) $ λ hy,
   by simp only [norm_unit_mul hx hy, units.coe_mul]; simp only [mul_assoc, mul_left_comm y], }
 
-@[simp] lemma normalize_apply {x : α} : normalize x = x * norm_unit x := rfl
-
 theorem associated_normalize {x : α} : associated x (normalize x) :=
 ⟨_, rfl⟩
 
 theorem normalize_associated {x : α} : associated (normalize x) x :=
 associated_normalize.symm
 
+lemma associates.mk_normalize {x : α} : associates.mk (normalize x) = associates.mk x :=
+associates.mk_eq_mk_iff_associated.2 normalize_associated
+
+@[simp] lemma normalize_apply {x : α} : normalize x = x * norm_unit x := rfl
+
 @[simp] lemma normalize_zero : normalize (0 : α) = 0 := by simp
 
 @[simp] lemma normalize_one : normalize (1 : α) = 1 := normalize.map_one

src/data/multiset/basic.lean

@@ -839,6 +839,12 @@ quotient.induction_on s $ λ l,
 lemma dvd_prod [comm_monoid α] {a : α} {s : multiset α} : a ∈ s → a ∣ s.prod :=
 quotient.induction_on s (λ l a h, by simpa using list.dvd_prod h) a
 
+theorem prod_eq_zero_iff [comm_cancel_monoid_with_zero α] [nontrivial α]
+  {s : multiset α} :
+  s.prod = 0 ↔ (0 : α) ∈ s :=
+multiset.induction_on s (by simp) $
+  assume a s, by simp [mul_eq_zero, @eq_comm _ 0 a] {contextual := tt}
+
 lemma le_sum_of_subadditive [add_comm_monoid α] [ordered_add_comm_monoid β]
   (f : α → β) (h_zero : f 0 = 0) (h_add : ∀x y, f (x + y) ≤ f x + f y) (s : multiset α) :
   f s.sum ≤ (s.map f).sum :=

src/field_theory/splitting_field.lean

@@ -255,10 +255,10 @@ by rw [degree_eq_nat_degree p_ne_zero, nat_degree_eq_card_roots hsplit]
 
 section UFD
 
-local attribute [instance, priority 10] principal_ideal_ring.to_unique_factorization_domain
+local attribute [instance, priority 10] principal_ideal_ring.to_unique_factorization_monoid
 local infix ` ~ᵤ ` : 50 := associated
 
-open unique_factorization_domain associates
+open unique_factorization_monoid associates
 
 lemma splits_of_exists_multiset {f : polynomial α} {s : multiset β}
   (hs : f.map i = C (i f.leading_coeff) * (s.map (λ a : β, (X : polynomial β) - C a)).prod) :
@@ -268,8 +268,8 @@ else
   or.inr $ λ p hp hdp,
     have ht : multiset.rel associated
       (factors (f.map i)) (s.map (λ a : β, (X : polynomial β) - C a)) :=
-    unique
-      (λ p hp, irreducible_factors (map_ne_zero hf0) _ hp)
+    factors_unique
+      (λ p hp, irreducible_of_factor _ hp)
       (λ p' m, begin
           obtain ⟨a,m,rfl⟩ := multiset.mem_map.1 m,
           exact irreducible_of_degree_eq_one (degree_X_sub_C _),
@@ -278,15 +278,15 @@ else
         ⟨(units.map' C : units β →* units (polynomial β)) (units.mk0 (f.map i).leading_coeff
             (mt leading_coeff_eq_zero.1 (map_ne_zero hf0))),
           by conv_rhs {rw [hs, ← leading_coeff_map i, mul_comm]}; refl⟩
-        ... ~ᵤ _ : associated.symm (unique_factorization_domain.factors_prod (by simpa using hf0))),
+        ... ~ᵤ _ : associated.symm (unique_factorization_monoid.factors_prod (by simpa using hf0))),
   let ⟨q, hq, hpq⟩ := exists_mem_factors_of_dvd (by simpa) hp hdp in
   let ⟨q', hq', hqq'⟩ := multiset.exists_mem_of_rel_of_mem ht hq in
   let ⟨a, ha⟩ := multiset.mem_map.1 hq' in
   by rw [← degree_X_sub_C a, ha.2];
     exact degree_eq_degree_of_associated (hpq.trans hqq')
 
 lemma splits_of_splits_id {f : polynomial α} : splits (ring_hom.id _) f → splits i f :=
-unique_factorization_domain.induction_on_prime f (λ _, splits_zero _)
+unique_factorization_monoid.induction_on_prime f (λ _, splits_zero _)
   (λ _ hu _, splits_of_degree_le_one _
     ((is_unit_iff_degree_eq_zero.1 hu).symm ▸ dec_trivial))
   (λ a p ha0 hp ih hfi, splits_mul _

src/ring_theory/discrete_valuation_ring.lean

@@ -171,18 +171,15 @@ end
 
 /-- Implementation detail: an integral domain in which there is a unit `p`
 such that every nonzero element is associated to a power of `p` is a unique factorization domain.
-
 See `discrete_valuation_ring.of_has_unit_mul_pow_irreducible_factorization`. -/
-noncomputable def ufd : unique_factorization_domain R :=
+theorem ufd : unique_factorization_monoid R :=
 let p := classical.some hR in
 let spec := classical.some_spec hR in
-{ factors := λ x, if h : x = 0 then 0 else multiset.repeat p (classical.some (spec.2 h)),
-  factors_prod := λ x hx,
-  by { rw [dif_neg hx, multiset.prod_repeat], exact (classical.some_spec (spec.2 hx)), },
-  prime_factors :=
-  begin
-    intros x hx q hq,
-    rw dif_neg hx at hq,
+unique_factorization_monoid_of_exists_prime_of_factor $ λ x hx,
+begin
+  use multiset.repeat p (classical.some (spec.2 hx)),
+  split,
+  { intros q hq,
     have hpq := multiset.eq_of_mem_repeat hq,
     rw hpq,
     refine ⟨spec.1.ne_zero, spec.1.not_unit, _⟩,
@@ -198,21 +195,23 @@ let spec := classical.some_spec hR in
     { simp only [hm, one_mul, pow_zero] at h ⊢, right, exact h },
     left,
     obtain ⟨m, rfl⟩ := nat.exists_eq_succ_of_ne_zero hm,
-    apply dvd_mul_of_dvd_left (dvd_refl _) _,
-  end }
+    apply dvd_mul_of_dvd_left (dvd_refl _) _ },
+  { rw [multiset.prod_repeat], exact (classical.some_spec (spec.2 hx)), }
+end
 
 omit hR
 
-lemma of_ufd_of_unique_irreducible [unique_factorization_domain R]
+lemma of_ufd_of_unique_irreducible [unique_factorization_monoid R]
   (h₁ : ∃ p : R, irreducible p)
   (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :
   has_unit_mul_pow_irreducible_factorization R :=
 begin
   obtain ⟨p, hp⟩ := h₁,
   refine ⟨p, hp, _⟩,
   intros x hx,
-  refine ⟨(unique_factorization_domain.factors x).card, _⟩,
-  have H := unique_factorization_domain.factors_prod hx,
+  cases wf_dvd_monoid.exists_factors x hx with fx hfx,
+  refine ⟨fx.card, _⟩,
+  have H := hfx.2,
   rw ← associates.mk_eq_mk_iff_associated at H ⊢,
   rw [← H, ← associates.prod_mk, associates.mk_pow, ← multiset.prod_repeat],
   congr' 1,
@@ -222,13 +221,13 @@ begin
     multiset.mem_map, exists_imp_distrib],
   rintros _ q hq rfl,
   rw associates.mk_eq_mk_iff_associated,
-  apply h₂ (unique_factorization_domain.irreducible_factors hx _ hq) hp,
+  apply h₂ (hfx.1 _ hq) hp,
 end
 
 end has_unit_mul_pow_irreducible_factorization
 
 lemma aux_pid_of_ufd_of_unique_irreducible
-  (R : Type u) [integral_domain R] [unique_factorization_domain R]
+  (R : Type u) [integral_domain R] [unique_factorization_monoid R]
   (h₁ : ∃ p : R, irreducible p)
   (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :
   is_principal_ideal_ring R :=
@@ -264,7 +263,7 @@ A unique factorization domain with at least one irreducible element
 in which all irreducible elements are associated
 is a discrete valuation ring.
 -/
-lemma of_ufd_of_unique_irreducible {R : Type u} [integral_domain R] [unique_factorization_domain R]
+lemma of_ufd_of_unique_irreducible {R : Type u} [integral_domain R] [unique_factorization_monoid R]
   (h₁ : ∃ p : R, irreducible p)
   (h₂ : ∀ ⦃p q : R⦄, irreducible p → irreducible q → associated p q) :
   discrete_valuation_ring R :=
@@ -276,14 +275,14 @@ begin
   { rw submodule.ne_bot_iff,
     refine ⟨p, ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩, },
   { rwa [ideal.span_singleton_prime hp.ne_zero,
-        ← unique_factorization_domain.irreducible_iff_prime], },
+        ← unique_factorization_monoid.irreducible_iff_prime], },
   { intro I,
     rw ← submodule.is_principal.span_singleton_generator I,
     rintro ⟨I0, hI⟩,
     apply span_singleton_eq_span_singleton.mpr,
     apply h₂ _ hp,
     erw [ne.def, span_singleton_eq_bot] at I0,
-    rwa [unique_factorization_domain.irreducible_iff_prime, ← ideal.span_singleton_prime I0], },
+    rwa [unique_factorization_monoid.irreducible_iff_prime, ← ideal.span_singleton_prime I0], },
 end
 
 /--
@@ -295,7 +294,7 @@ lemma of_has_unit_mul_pow_irreducible_factorization {R : Type u} [integral_domai
   (hR : has_unit_mul_pow_irreducible_factorization R) :
   discrete_valuation_ring R :=
 begin
-  letI : unique_factorization_domain R := hR.ufd,
+  letI : unique_factorization_monoid R := hR.ufd,
   apply of_ufd_of_unique_irreducible _ hR.unique_irreducible,
   unfreezingI { obtain ⟨p, hp, H⟩ := hR, exact ⟨p, hp⟩, },
 end
@@ -309,9 +308,10 @@ variable {R}
 lemma associated_pow_irreducible {x : R} (hx : x ≠ 0) {ϖ : R} (hirr : irreducible ϖ) :
   ∃ (n : ℕ), associated x (ϖ ^ n) :=
 begin
-  have : unique_factorization_domain R := principal_ideal_ring.to_unique_factorization_domain,
-  unfreezingI { use (unique_factorization_domain.factors x).card },
-  have H := unique_factorization_domain.factors_prod hx,
+  have : wf_dvd_monoid R := is_noetherian_ring.wf_dvd_monoid,
+  cases wf_dvd_monoid.exists_factors x hx with fx hfx,
+  unfreezingI { use fx.card },
+  have H := hfx.2,
   rw ← associates.mk_eq_mk_iff_associated at H ⊢,
   rw [← H, ← associates.prod_mk, associates.mk_pow, ← multiset.prod_repeat],
   congr' 1,
@@ -321,7 +321,7 @@ begin
   rintros _ _ _ rfl,
   rw associates.mk_eq_mk_iff_associated,
   refine associated_of_irreducible _ _ hirr,
-  apply unique_factorization_domain.irreducible_factors hx,
+  apply hfx.1,
   assumption
 end
 
@@ -348,8 +348,7 @@ begin
     refine ⟨u * v⁻¹, _⟩,
     simp only [units.coe_mul],
     rw [mul_left_comm, ← mul_assoc, h, mul_right_comm, units.mul_inv, one_mul], },
-  letI := @principal_ideal_ring.to_unique_factorization_domain R _ _,
-  have := multiset.card_eq_card_of_rel (unique_factorization_domain.unique _ _ key),
+  have := multiset.card_eq_card_of_rel (unique_factorization_monoid.factors_unique _ _ key),
   { simpa only [multiset.card_repeat] },
   all_goals
   { intros x hx, replace hx := multiset.eq_of_mem_repeat hx,

src/ring_theory/localization.lean

@@ -1316,15 +1316,15 @@ end
 
 section num_denom
 
-variables [unique_factorization_domain A] (φ : fraction_map A K)
+variables [unique_factorization_monoid A] (φ : fraction_map A K)
 
 lemma exists_reduced_fraction (x : φ.codomain) :
   ∃ (a : A) (b : non_zero_divisors A),
   (∀ {d}, d ∣ a → d ∣ b → is_unit d) ∧ φ.mk' a b = x :=
 begin
   obtain ⟨⟨b, b_nonzero⟩, a, hab⟩ := φ.exists_integer_multiple x,
   obtain ⟨a', b', c', no_factor, rfl, rfl⟩ :=
-    unique_factorization_domain.exists_reduced_factors' a b
+    unique_factorization_monoid.exists_reduced_factors' a b
       (mem_non_zero_divisors_iff_ne_zero.mp b_nonzero),
   obtain ⟨c'_nonzero, b'_nonzero⟩ := mul_mem_non_zero_divisors.mp b_nonzero,
   refine ⟨a', ⟨b', b'_nonzero⟩, @no_factor, _⟩,

src/ring_theory/polynomial/rational_root.lean

@@ -42,7 +42,7 @@ begin
 end
 
 lemma num_is_root_scale_roots_of_aeval_eq_zero
-  [unique_factorization_domain A] (g : fraction_map A K)
+  [unique_factorization_monoid A] (g : fraction_map A K)
   {p : polynomial A} {x : g.codomain} (hr : aeval x p = 0) :
   is_root (scale_roots p (g.denom x)) (g.num x) :=
 begin
@@ -56,10 +56,10 @@ end scale_roots
 
 section rational_root_theorem
 
-variables {A K : Type*} [integral_domain A] [unique_factorization_domain A] [field K]
+variables {A K : Type*} [integral_domain A] [unique_factorization_monoid A] [field K]
 variables {f : fraction_map A K}
 
-open polynomial unique_factorization_domain
+open polynomial unique_factorization_monoid
 
 /-- Rational root theorem part 1:
 if `r : f.codomain` is a root of a polynomial over the ufd `A`,
@@ -74,7 +74,7 @@ begin
     { obtain ⟨u, hu⟩ := is_unit_pow p.nat_degree (f.is_unit_denom_of_num_eq_zero hr),
       rw ←hu at this,
       exact units.dvd_mul_right.mp this },
-    { refine dvd_of_dvd_mul_left_of_no_prime_factors hr _ this,
+    { refine dvd_of_dvd_mul_left_of_no_prime_of_factor hr _ this,
       intros q dvd_num dvd_denom_pow hq,
       apply hq.not_unit,
       exact f.num_denom_reduced r dvd_num (hq.dvd_of_dvd_pow dvd_denom_pow) } },
@@ -93,7 +93,7 @@ theorem denom_dvd_of_is_root {p : polynomial A} {r : f.codomain} (hr : aeval r p
   (f.denom r : A) ∣ p.leading_coeff :=
 begin
   suffices : (f.denom r : A) ∣ p.leading_coeff * f.num r ^ p.nat_degree,
-  { refine dvd_of_dvd_mul_left_of_no_prime_factors
+  { refine dvd_of_dvd_mul_left_of_no_prime_of_factor
       (mem_non_zero_divisors_iff_ne_zero.mp (f.denom r).2) _ this,
     intros q dvd_denom dvd_num_pow hq,
     apply hq.not_unit,
@@ -118,7 +118,7 @@ theorem is_integer_of_is_root_of_monic {p : polynomial A} (hp : monic p) {r : f.
   (hr : aeval r p = 0) : f.is_integer r :=
 f.is_integer_of_is_unit_denom (is_unit_of_dvd_one _ (hp ▸ denom_dvd_of_is_root hr))
 
-namespace unique_factorization_domain
+namespace unique_factorization_monoid
 
 lemma integer_of_integral {x : f.codomain} :
   is_integral A x → f.is_integer x :=
@@ -127,6 +127,6 @@ lemma integer_of_integral {x : f.codomain} :
 lemma integrally_closed : integral_closure A f.codomain = ⊥ :=
 eq_bot_iff.mpr (λ x hx, algebra.mem_bot.mpr (integer_of_integral hx))
 
-end unique_factorization_domain
+end unique_factorization_monoid
 
 end rational_root_theorem

src/ring_theory/principal_ideal_domain.lean

@@ -20,9 +20,7 @@ Theorems about PID's are in the `principal_ideal_ring` namespace.
 - `is_principal_ideal_ring`: a predicate on commutative rings, saying that every
   ideal is principal.
 - `generator`: a generator of a principal ideal (or more generally submodule)
-- `to_unique_factorization_domain`: a noncomputable definition, putting a UFD structure on a PID.
-  Note that the definition of a UFD is currently not a predicate, as it contains data
-  of factorizations of non-zero elements.
+- `to_unique_factorization_monoid`: a PID is a unique factorization domain
 
 # Main results
 
@@ -169,7 +167,7 @@ noncomputable def factors (a : R) : multiset R :=
 if h : a = 0 then ∅ else classical.some (wf_dvd_monoid.exists_factors a h)
 
 lemma factors_spec (a : R) (h : a ≠ 0) :
-  (∀b∈factors a, irreducible b) ∧ associated a (factors a).prod :=
+  (∀b∈factors a, irreducible b) ∧ associated (factors a).prod a :=
 begin
   unfold factors, rw [dif_neg h],
   exact classical.some_spec (wf_dvd_monoid.exists_factors a h)
@@ -182,7 +180,7 @@ lemma mem_submonoid_of_factors_subset_of_units_subset (s : submonoid R)
   {a : R} (ha : a ≠ 0) (hfac : ∀ b ∈ factors a, b ∈ s) (hunit : ∀ c : units R, (c : R) ∈ s) :
   a ∈ s :=
 begin
-  rcases ((factors_spec a ha).2).symm with ⟨c, hc⟩,
+  rcases ((factors_spec a ha).2) with ⟨c, hc⟩,
   rw [← hc],
   exact submonoid.mul_mem _ (submonoid.multiset_prod_mem _ _ hfac) (hunit _),
 end
@@ -196,15 +194,11 @@ lemma ring_hom_mem_submonoid_of_factors_subset_of_units_subset {R S : Type*}
   f a ∈ s :=
 mem_submonoid_of_factors_subset_of_units_subset (s.comap f.to_monoid_hom) ha h hf
 
-/-- The unique factorization domain structure given by the principal ideal domain.
-
-This is not added as type class instance, since the `factors` might be computed in a different way.
-E.g. factors could return normalized values.
--/
-noncomputable def to_unique_factorization_domain : unique_factorization_domain R :=
-{ factors := factors,
-  factors_prod := assume a ha, associated.symm (factors_spec a ha).2,
-  prime_factors := assume a ha, by simpa [irreducible_iff_prime] using (factors_spec a ha).1 }
+/-- A principal ideal domain has unique factorization -/
+@[priority 100] -- see Note [lower instance priority]
+instance to_unique_factorization_monoid : unique_factorization_monoid R :=
+{ irreducible_iff_prime := λ _, principal_ideal_ring.irreducible_iff_prime
+  .. (is_noetherian_ring.wf_dvd_monoid : wf_dvd_monoid R) }
 
 end