refactor(unique_factorization_domain): simplify definition of UFD

Author: Chris Hughes

data/multiset.lean

@@ -774,6 +774,9 @@ lemma prod_hom [comm_monoid α] [comm_monoid β] (f : α → β) [is_monoid_hom
 multiset.induction_on s (by simp [is_monoid_hom.map_one f])
   (by simp [is_monoid_hom.map_mul f] {contextual := tt})
 
+lemma dvd_prod [comm_semiring α] {a : α} {s : multiset α} : a ∈ s → a ∣ s.prod :=
+quotient.induction_on s (λ l a h, by simpa using list.dvd_prod h) a
+
 lemma sum_hom [add_comm_monoid α] [add_comm_monoid β] (f : α → β) [is_add_monoid_hom f] (s : multiset α) :
   (s.map f).sum = f s.sum :=
 multiset.induction_on s (by simp [is_add_monoid_hom.map_zero f])

ring_theory/associated.lean

@@ -13,6 +13,8 @@ open lattice
 /-- is unit -/
 def is_unit [monoid α] (a : α) : Prop := ∃u:units α, a = u
 
+@[simp] lemma is_unit_unit [monoid α] (u : units α) : is_unit (u : α) := ⟨u, rfl⟩
+
 @[simp] theorem is_unit_zero_iff [semiring α] : is_unit (0 : α) ↔ (0:α) = 1 :=
 ⟨λ ⟨⟨_, a, (a0 : 0 * a = 1), _⟩, rfl⟩, by rwa zero_mul at a0,
  λ h, begin
@@ -70,6 +72,12 @@ theorem mul_dvd_of_is_unit_left [comm_semiring α] {x y z : α} (h : is_unit x)
 theorem mul_dvd_of_is_unit_right [comm_semiring α] {x y z : α} (h : is_unit y) : x * y ∣ z ↔ x ∣ z :=
 by rw [mul_comm, mul_dvd_of_is_unit_left h]
 
+@[simp] lemma unit_mul_dvd_iff [comm_semiring α] {a b : α} {u : units α} : (u : α) * a ∣ b ↔ a ∣ b :=
+mul_dvd_of_is_unit_left (is_unit_unit _)
+
+@[simp] lemma mul_unit_dvd_iff [comm_semiring α] {a b : α} {u : units α} : a * u ∣ b ↔ a ∣ b :=
+mul_dvd_of_is_unit_right (is_unit_unit _)
+
 theorem is_unit_of_dvd_unit {α} [comm_semiring α] {x y : α}
   (xy : x ∣ y) (hu : is_unit y) : is_unit x :=
 is_unit_iff_dvd_one.2 $ dvd_trans xy $ is_unit_iff_dvd_one.1 hu
@@ -97,7 +105,7 @@ lemma dvd_and_not_dvd_iff [integral_domain α] {x y : α} :
 def prime [comm_semiring α] (p : α) : Prop :=
 p ≠ 0 ∧ ¬ is_unit p ∧ (∀a b, p ∣ a * b → p ∣ a ∨ p ∣ b)
 
-lemma not_prime_zero [integral_domain α] : ¬ prime (0 : α)
+@[simp] lemma not_prime_zero [integral_domain α] : ¬ prime (0 : α)
 | ⟨h, _⟩ := h rfl
 
 @[simp] lemma not_prime_one [comm_semiring α] : ¬ prime (1 : α) :=
@@ -263,6 +271,78 @@ begin
   exact ⟨units.mk_of_mul_eq_one c d (this.symm), by rw [units.mk_of_mul_eq_one, units.val_coe]⟩
 end
 
+lemma exists_associated_mem_of_dvd_prod [integral_domain α] {p : α}
+  (hp : prime p) {s : multiset α} : (∀ r ∈ s, prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
+multiset.induction_on s (by simp [mt is_unit_iff_dvd_one.2 hp.2.1])
+  (λ a s ih hs hps, begin
+    rw [multiset.prod_cons] at hps,
+    cases hp.2.2 _ _ hps with h h,
+    { use [a, by simp],
+      cases h with u hu,
+      cases ((irreducible_of_prime (hs a (multiset.mem_cons.2
+        (or.inl rfl)))).2 p u hu).resolve_left hp.2.1 with v hv,
+      exact ⟨v, by simp [hu, hv]⟩ },
+    { rcases ih (λ r hr, hs _ (multiset.mem_cons.2 (or.inr hr))) h with ⟨q, hq₁, hq₂⟩,
+      exact ⟨q, multiset.mem_cons.2 (or.inr hq₁), hq₂⟩ }
+  end)
+
+lemma dvd_iff_dvd_of_rel_left [comm_semiring α] {a b c : α} (h : a ~ᵤ b) : a ∣ c ↔ b ∣ c :=
+let ⟨u, hu⟩ := h in hu ▸ mul_unit_dvd_iff.symm
+
+@[simp] lemma dvd_mul_unit_iff [comm_semiring α] {a b : α} {u : units α} : a ∣ b * u ↔ a ∣ b :=
+⟨λ ⟨d, hd⟩, ⟨d * (u⁻¹ : units α), by simp [(mul_assoc _ _ _).symm, hd.symm]⟩,
+  λ h, dvd.trans h (by simp)⟩
+
+lemma dvd_iff_dvd_of_rel_right [comm_semiring α] {a b c : α} (h : b ~ᵤ c) : a ∣ b ↔ a ∣ c :=
+let ⟨u, hu⟩ := h in hu ▸ dvd_mul_unit_iff.symm
+
+lemma eq_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a = 0 ↔ b = 0 :=
+⟨λ ha, let ⟨u, hu⟩ := h in by simp [hu.symm, ha],
+  λ hb, let ⟨u, hu⟩ := h.symm in by simp [hu.symm, hb]⟩
+
+lemma ne_zero_iff_of_associated [comm_semiring α] {a b : α} (h : a ~ᵤ b) : a ≠ 0 ↔ b ≠ 0 :=
+by haveI := classical.dec; exact not_iff_not.2 (eq_zero_iff_of_associated h)
+
+lemma prime_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) (hp : prime p) : prime q :=
+⟨(ne_zero_iff_of_associated h).1 hp.1,
+  let ⟨u, hu⟩ := h in
+    ⟨λ ⟨v, hv⟩, hp.2.1 ⟨v * u⁻¹, by simp [hv.symm, hu.symm]⟩,
+      hu ▸ by simp [mul_unit_dvd_iff]; exact hp.2.2⟩⟩
+
+lemma prime_iff_of_associated [comm_semiring α] {p q : α}
+  (h : p ~ᵤ q) : prime p ↔ prime q :=
+⟨prime_of_associated h, prime_of_associated h.symm⟩
+
+lemma is_unit_iff_of_associated [monoid α] {a b : α} (h :  a ~ᵤ b) : is_unit a ↔ is_unit b :=
+⟨let ⟨u, hu⟩ := h in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩,
+  let ⟨u, hu⟩ := h.symm in λ ⟨v, hv⟩, ⟨v * u, by simp [hv, hu.symm]⟩⟩
+
+lemma irreducible_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q)
+  (hp : irreducible p) : irreducible q :=
+⟨mt (is_unit_iff_of_associated h).2 hp.1,
+  let ⟨u, hu⟩ := h in λ a b hab,
+  have hpab : p = a * (b * (u⁻¹ : units α)),
+    from calc p = (p * u) * (u ⁻¹ : units α) : by simp
+      ... = _ : by rw hu; simp [hab, mul_assoc],
+  (hp.2 _ _ hpab).elim or.inl (λ ⟨v, hv⟩, or.inr ⟨v * u, by simp [hv.symm]⟩)⟩
+
+lemma irreducible_iff_of_associated [comm_semiring α] {p q : α} (h : p ~ᵤ q) :
+  irreducible p ↔ irreducible q :=
+⟨irreducible_of_associated h, irreducible_of_associated h.symm⟩
+
+lemma associated_mul_left_cancel [integral_domain α] {a b c d : α}
+(h : a * b ~ᵤ c * d) (h₁ : a ~ᵤ c) (ha : a ≠ 0) : b ~ᵤ d :=
+let ⟨u, hu⟩ := h in let ⟨v, hv⟩ := associated.symm h₁ in
+⟨u * (v : units α), (domain.mul_left_inj ha).1
+  begin
+    rw [← hv, mul_assoc c (v : α) d, mul_left_comm c, ← hu],
+    simp [hv.symm, mul_assoc, mul_comm, mul_left_comm]
+  end⟩
+
+lemma associated_mul_right_cancel [integral_domain α] {a b c d : α} :
+  a * b ~ᵤ c * d → b ~ᵤ d → b ≠ 0 → a ~ᵤ c :=
+by rw [mul_comm a, mul_comm c]; exact associated_mul_left_cancel
+
 def associates (α : Type*) [monoid α] : Type* :=
 quotient (associated.setoid α)
 

ring_theory/principal_ideal_domain.lean

@@ -218,6 +218,7 @@ This is not added as type class instance, since the `factors` might be computed
 E.g. factors could return normalized values.
 -/
 noncomputable def to_unique_factorization_domain : unique_factorization_domain α :=
+unique_factorization_domain.of_unique_irreducible_factorization
 { factors := factors,
   factors_prod := assume a ha, associated.symm (factors_spec a ha).2,
   irreducible_factors := assume a ha, (factors_spec a ha).1,

ring_theory/unique_factorization_domain.lean

@@ -14,16 +14,162 @@ local infix ` ~ᵤ ` : 50 := associated
 
 /-- Unique factorization domains.
 
-In a unique factorization domain each element (except zero) is uniquely represented as a multiset
-of irreducible factors. Uniqueness is only up to associated elements.
+In a unique factorization domain each element (except zero) is uniquely
+represented as a multiset of irreducible factors.
+Uniqueness is only up to associated elements.
+
+This is equivalent to defining a unique factorization domain as a domain in
+which each element (except zero) is represented as a multiset of prime factors.
+This definition is used.
+
+To define a UFD using the traditional definition in terms of multisets of irreducible
+factors, use the definition `of_unique_irreducible_factorization
+
 -/
 class unique_factorization_domain (α : Type*) [integral_domain α] :=
 (factors : α → multiset α)
 (factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
+(prime_factors : ∀{a : α}, a ≠ 0 → ∀x∈factors a, prime x)
+
+namespace unique_factorization_domain
+
+variables [integral_domain α] [unique_factorization_domain α]
+
+@[elab_as_eliminator] lemma induction_on_prime {P : α → Prop}
+  (a : α) (h₁ : P 0) (h₂ : ∀ x : α, is_unit x → P x)
+  (h₃ : ∀ a p : α, a ≠ 0 → prime p → P a → P (p * a)) : P a :=
+by haveI := classical.dec_eq α; exact
+if ha0 : a = 0 then ha0.symm ▸ h₁
+else @multiset.induction_on _
+  (λ s : multiset α, ∀ (a : α), a ≠ 0 → s.prod ~ᵤ a → (∀ p ∈ s, prime p) →  P a)
+    (factors a)
+  (λ _ _ h _, h₂ _ ((is_unit_iff_of_associated h.symm).2 is_unit_one))
+  (λ p s ih a ha0 ⟨u, hu⟩ hsp,
+    have ha : a = (p * u) * s.prod, by simp [hu.symm, mul_comm, mul_assoc],
+    have hs0 : s.prod ≠ 0, from λ _ : s.prod = 0, by simp * at *,
+    ha.symm ▸ h₃ _ _ hs0
+      (prime_of_associated ⟨u, rfl⟩ (hsp p (multiset.mem_cons_self _ _)))
+      (ih _ hs0 (by refl) (λ p hp, hsp p (multiset.mem_cons.2 (or.inr hp)))))
+  _
+  ha0
+  (factors_prod ha0)
+  (prime_factors ha0)
+
+lemma factors_irreducible {a : α} (ha : irreducible a) :
+  ∃ p, a ~ᵤ p ∧ factors a = p :: 0 :=
+by haveI := classical.dec_eq α; exact
+multiset.induction_on (factors a)
+  (λ h, (ha.1 (associated_one_iff_is_unit.1 h.symm)).elim)
+  (λ p s _ hp hs, let ⟨u, hu⟩ := hp in ⟨p,
+    have hs0 : s = 0, from classical.by_contradiction
+      (λ hs0, let ⟨q, hq⟩ := multiset.exists_mem_of_ne_zero hs0 in
+       (hs q (by simp [hq])).2.1 $
+        (ha.2 ((p * u) * (s.erase q).prod) _
+          (by rw [mul_right_comm _ _ q, mul_assoc, ← multiset.prod_cons,
+            multiset.cons_erase hq]; simp [hu.symm, mul_comm, mul_assoc])).resolve_left $
+              mt is_unit_of_mul_is_unit_left $ mt is_unit_of_mul_is_unit_left
+                (hs p (multiset.mem_cons_self _ _)).2.1),
+    ⟨associated.symm (by clear _let_match; simp * at *), hs0 ▸ rfl⟩⟩)
+  (factors_prod (nonzero_of_irreducible ha))
+  (prime_factors (nonzero_of_irreducible ha))
+
+lemma irreducible_iff_prime {p : α} : irreducible p ↔ prime p :=
+by letI := classical.dec_eq α; exact
+if hp0 : p = 0 then by simp [hp0]
+else
+  ⟨λ h, let ⟨q, hq⟩ := factors_irreducible h in
+      have prime q, from hq.2 ▸ prime_factors hp0 _ (by simp [hq.2]),
+      suffices prime (factors p).prod,
+        from prime_of_associated (factors_prod hp0) this,
+      hq.2.symm ▸ by simp [this],
+    irreducible_of_prime⟩
+
+lemma irreducible_factors :  ∀{a : α}, a ≠ 0 → ∀x∈factors a, irreducible x :=
+by simp only [irreducible_iff_prime]; exact @prime_factors _ _ _
+
+lemma unique : ∀{f g : multiset α},
+  (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod →
+  multiset.rel associated f g :=
+by haveI := classical.dec_eq α; exact
+λ f, multiset.induction_on f
+  (λ g _ hg h,
+    multiset.rel_zero_left.2 $
+      multiset.eq_zero_of_forall_not_mem (λ x hx,
+        have is_unit g.prod, by simpa [associated_one_iff_is_unit] using h.symm,
+        (hg x hx).1 (is_unit_iff_dvd_one.2 (dvd.trans (multiset.dvd_prod hx)
+          (is_unit_iff_dvd_one.1 this)))))
+  (λ p f ih g hf hg hfg,
+    let ⟨b, hbg, hb⟩ := exists_associated_mem_of_dvd_prod
+      (irreducible_iff_prime.1 (hf p (by simp)))
+      (λ q hq, irreducible_iff_prime.1 (hg _ hq)) $
+        (dvd_iff_dvd_of_rel_right hfg).1
+          (show p ∣ (p :: f).prod, by simp) in
+    begin
+      rw ← multiset.cons_erase hbg,
+      exact multiset.rel.cons hb (ih (λ q hq, hf _ (by simp [hq]))
+        (λ q (hq : q ∈ g.erase b), hg q (multiset.mem_of_mem_erase hq))
+        (associated_mul_left_cancel
+          (by rwa [← multiset.prod_cons, ← multiset.prod_cons, multiset.cons_erase hbg]) hb
+        (nonzero_of_irreducible (hf p (by simp)))))
+    end)
+
+end unique_factorization_domain
+
+structure unique_irreducible_factorization (α : Type*) [integral_domain α] :=
+(factors : α → multiset α)
+(factors_prod : ∀{a : α}, a ≠ 0 → (factors a).prod ~ᵤ a)
 (irreducible_factors : ∀{a : α}, a ≠ 0 →  ∀x∈factors a, irreducible x)
 (unique : ∀{f g : multiset α},
   (∀x∈f, irreducible x) → (∀x∈g, irreducible x) → f.prod ~ᵤ g.prod → multiset.rel associated f g)
 
+namespace unique_factorization_domain
+
+def of_unique_irreducible_factorization {α : Type*} [integral_domain α]
+  (o : unique_irreducible_factorization α) : unique_factorization_domain α :=
+by letI := classical.dec_eq α; exact
+{ prime_factors := λ a h p (hpa : p ∈ o.factors a),
+    have hpi : irreducible p, from o.irreducible_factors h _ hpa,
+    ⟨nonzero_of_irreducible hpi, hpi.1,
+      λ a b ⟨x, hx⟩,
+      if hab0 : a * b = 0
+      then (eq_zero_or_eq_zero_of_mul_eq_zero hab0).elim
+        (λ ha0, by simp [ha0])
+        (λ hb0, by simp [hb0])
+      else
+        have hx0 : x ≠ 0, from λ hx0, by simp * at *,
+        have ha0 : a ≠ 0, from ne_zero_of_mul_ne_zero_right hab0,
+        have hb0 : b ≠ 0, from ne_zero_of_mul_ne_zero_left hab0,
+        have multiset.rel associated  (p :: o.factors x) (o.factors a + o.factors b),
+          from o.unique
+            (λ i hi, (multiset.mem_cons.1 hi).elim
+              (λ hip, hip.symm ▸ hpi)
+              (o.irreducible_factors hx0 _))
+            (show ∀ x ∈ o.factors a + o.factors b, irreducible x,
+              from λ x hx, (multiset.mem_add.1 hx).elim
+                (o.irreducible_factors (ne_zero_of_mul_ne_zero_right hab0) _)
+                (o.irreducible_factors (ne_zero_of_mul_ne_zero_left hab0) _)) $
+              calc multiset.prod (p :: o.factors x)
+                  ~ᵤ a * b : by rw [hx, multiset.prod_cons];
+                    exact associated_mul_mul (by refl)
+                      (o.factors_prod hx0)
+              ... ~ᵤ (o.factors a).prod * (o.factors b).prod :
+                associated_mul_mul
+                  (o.factors_prod ha0).symm
+                  (o.factors_prod hb0).symm
+              ... = _ : by rw multiset.prod_add,
+        let ⟨q, hqf, hq⟩ := multiset.exists_mem_of_rel_of_mem this
+          (multiset.mem_cons_self p _) in
+        (multiset.mem_add.1 hqf).elim
+          (λ hqa, or.inl $ (dvd_iff_dvd_of_rel_left hq).2 $
+            (dvd_iff_dvd_of_rel_right (o.factors_prod ha0)).1
+              (multiset.dvd_prod hqa))
+          (λ hqb, or.inr $ (dvd_iff_dvd_of_rel_left hq).2 $
+            (dvd_iff_dvd_of_rel_right (o.factors_prod hb0)).1
+              (multiset.dvd_prod hqb))⟩,
+  ..o }
+
+end unique_factorization_domain
+
 namespace associates
 open unique_factorization_domain associated lattice
 variables [integral_domain α] [unique_factorization_domain α] [decidable_eq (associates α)]