refactor(algebra/gcd_monoid): don't require normalization (#9443)

This will allow us to set up a gcd_monoid instance for all euclidean_domains and generalize the results in ring_theory/euclidean_domain.lean to PIDs.

docs/overview.yaml

@@ -84,7 +84,7 @@ General algebra:
     separable polynomial: 'polynomial.separable'
     $K[X]$ is Euclidean: 'polynomial.euclidean_domain'
     Hilbert basis theorem: 'polynomial.is_noetherian_ring'
-    $A[X]$ has gcd and lcm if $A$ does: 'polynomial.gcd_monoid'
+    $A[X]$ has gcd and lcm if $A$ does: 'polynomial.normalized_gcd_monoid'
     $A[X]$ is a UFD when $A$ is a UFD: 'polynomial.unique_factorization_monoid'
     irreducible polynomial: 'irreducible'
     Eisenstein's criterion: 'polynomial.irreducible_of_eisenstein_criterion'

src/algebra/associated.lean

@@ -255,6 +255,25 @@ theorem associated_one_of_associated_mul_one [comm_monoid α] {a b : α} :
   a * b ~ᵤ 1 → a ~ᵤ 1
 | ⟨u, h⟩ := associated_one_of_mul_eq_one (b * u) $ by simpa [mul_assoc] using h
 
+lemma associated_mul_unit_left {β : Type*} [monoid β] (a u : β) (hu : is_unit u) :
+  associated (a * u) a :=
+let ⟨u', hu⟩ := hu in ⟨u'⁻¹, hu ▸ units.mul_inv_cancel_right _ _⟩
+
+lemma associated_unit_mul_left {β : Type*} [comm_monoid β] (a u : β) (hu : is_unit u) :
+  associated (u * a) a :=
+begin
+  rw mul_comm,
+  exact associated_mul_unit_left _ _ hu
+end
+
+lemma associated_mul_unit_right {β : Type*} [monoid β] (a u : β) (hu : is_unit u) :
+  associated a (a * u) :=
+(associated_mul_unit_left a u hu).symm
+
+lemma associated_unit_mul_right {β : Type*} [comm_monoid β] (a u : β) (hu : is_unit u) :
+  associated a (u * a) :=
+(associated_unit_mul_left a u hu).symm
+
 lemma associated.mul_mul [comm_monoid α] {a₁ a₂ b₁ b₂ : α} :
   a₁ ~ᵤ b₁ → a₂ ~ᵤ b₂ → (a₁ * a₂) ~ᵤ (b₁ * b₂)
 | ⟨c₁, h₁⟩ ⟨c₂, h₂⟩ := ⟨c₁ * c₂, by simp [h₁.symm, h₂.symm, mul_assoc, mul_comm, mul_left_comm]⟩
@@ -381,10 +400,12 @@ by rw [mul_comm a, mul_comm c]; exact associated.of_mul_left
 section unique_units
 variables [monoid α] [unique (units α)]
 
+lemma units_eq_one (u : units α) : u = 1 := subsingleton.elim u 1
+
 theorem associated_iff_eq {x y : α} : x ~ᵤ y ↔ x = y :=
 begin
   split,
-  { rintro ⟨c, rfl⟩, simp [subsingleton.elim c 1] },
+  { rintro ⟨c, rfl⟩, rw [units_eq_one c, units.coe_one, mul_one] },
   { rintro rfl, refl },
 end
 

src/algebra/gcd_monoid/finset.lean

@@ -31,7 +31,7 @@ variables {α β γ : Type*}
 namespace finset
 open multiset
 
-variables [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α]
+variables [comm_cancel_monoid_with_zero α] [nontrivial α] [normalized_gcd_monoid α]
 
 /-! ### lcm -/
 section lcm
@@ -201,7 +201,7 @@ end finset
 namespace finset
 section integral_domain
 
-variables [nontrivial β] [integral_domain α] [gcd_monoid α]
+variables [nontrivial β] [integral_domain α] [normalized_gcd_monoid α]
 
 lemma gcd_eq_of_dvd_sub {s : finset β} {f g : β → α} {a : α}
   (h : ∀ x : β, x ∈ s → a ∣ f x - g x) :

src/algebra/gcd_monoid/multiset.lean

@@ -24,7 +24,7 @@ multiset, gcd
 -/
 
 namespace multiset
-variables {α : Type*} [comm_cancel_monoid_with_zero α] [nontrivial α] [gcd_monoid α]
+variables {α : Type*} [comm_cancel_monoid_with_zero α] [nontrivial α] [normalized_gcd_monoid α]
 
 /-! ### lcm -/
 section lcm

src/field_theory/minpoly.lean

@@ -351,7 +351,7 @@ section gcd_domain
 /-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
 over the fraction field. -/
 lemma gcd_domain_eq_field_fractions {A R : Type*} (K : Type*) [integral_domain A]
-  [gcd_monoid A] [field K] [integral_domain R] [algebra A K] [is_fraction_ring A K]
+  [normalized_gcd_monoid A] [field K] [integral_domain R] [algebra A K] [is_fraction_ring A K]
   [algebra K R] [algebra A R] [is_scalar_tower A K R] {x : R} (hx : is_integral A x) :
   minpoly K x = (minpoly A x).map (algebra_map A K) :=
 begin
@@ -367,7 +367,7 @@ end
 /-- For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral
 element as root. -/
 lemma gcd_domain_dvd {A R : Type*} (K : Type*)
-  [integral_domain A] [gcd_monoid A] [field K] [integral_domain R] [algebra A K]
+  [integral_domain A] [normalized_gcd_monoid A] [field K] [integral_domain R] [algebra A K]
   [is_fraction_ring A K] [algebra K R] [algebra A R] [is_scalar_tower A K R]
   {x : R} (hx : is_integral A x)
   {P : polynomial A} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :

src/ring_theory/int/basic.lean

@@ -92,10 +92,14 @@ instance : gcd_monoid ℕ :=
   gcd_dvd_left := nat.gcd_dvd_left ,
   gcd_dvd_right := nat.gcd_dvd_right,
   dvd_gcd := λ a b c, nat.dvd_gcd,
-  normalize_gcd := λ a b, normalize_eq _,
-  gcd_mul_lcm := λ a b, by rw [normalize_eq _, nat.gcd_mul_lcm],
+  gcd_mul_lcm := λ a b, by rw [nat.gcd_mul_lcm],
   lcm_zero_left := nat.lcm_zero_left,
-  lcm_zero_right := nat.lcm_zero_right,
+  lcm_zero_right := nat.lcm_zero_right }
+
+instance : normalized_gcd_monoid ℕ :=
+{ normalize_gcd := λ a b, normalize_eq _,
+  normalize_lcm := λ a b, normalize_eq _,
+  .. (infer_instance : gcd_monoid ℕ),
   .. (infer_instance : normalization_monoid ℕ) }
 
 lemma gcd_eq_nat_gcd (m n : ℕ) : gcd m n = nat.gcd m n := rfl
@@ -145,11 +149,17 @@ instance : gcd_monoid ℤ :=
   gcd_dvd_left   := assume a b, int.gcd_dvd_left _ _,
   gcd_dvd_right  := assume a b, int.gcd_dvd_right _ _,
   dvd_gcd        := assume a b c, dvd_gcd,
-  normalize_gcd  := assume a b, normalize_coe_nat _,
-  gcd_mul_lcm    := by intros; rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize],
+  gcd_mul_lcm    := λ a b, by {
+    rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize],
+    exact normalize_associated (a * b) },
   lcm_zero_left  := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_left _,
-  lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _,
-  .. int.normalization_monoid }
+  lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _}
+
+instance : normalized_gcd_monoid ℤ :=
+{ normalize_gcd  := λ a b, normalize_coe_nat _,
+  normalize_lcm  := λ a b, normalize_coe_nat _,
+  .. int.normalization_monoid,
+  .. (infer_instance : gcd_monoid ℤ) }
 
 lemma coe_gcd (i j : ℤ) : ↑(int.gcd i j) = gcd_monoid.gcd i j := rfl
 lemma coe_lcm (i j : ℤ) : ↑(int.lcm i j) = gcd_monoid.lcm i j := rfl
@@ -194,7 +204,7 @@ by rw [←gcd_eq_one_iff_coprime, nat.coprime_iff_gcd_eq_one, gcd_eq_nat_abs]
 lemma sq_of_gcd_eq_one {a b c : ℤ} (h : int.gcd a b = 1) (heq : a * b = c ^ 2) :
   ∃ (a0 : ℤ), a = a0 ^ 2 ∨ a = - (a0 ^ 2) :=
 begin
-  have h' : gcd_monoid.gcd a b = 1, { rw [← coe_gcd, h], dec_trivial },
+  have h' : is_unit (gcd_monoid.gcd a b), { rw [← coe_gcd, h, int.coe_nat_one], exact is_unit_one },
   obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq,
   use d,
   rw ← hu,

src/ring_theory/polynomial/basic.lean

@@ -974,7 +974,7 @@ variables {D : Type u} [integral_domain D] [unique_factorization_monoid D]
 instance unique_factorization_monoid : unique_factorization_monoid (polynomial D) :=
 begin
   haveI := arbitrary (normalization_monoid D),
-  haveI := to_gcd_monoid D,
+  haveI := to_normalized_gcd_monoid D,
   exact ufm_of_gcd_of_wf_dvd_monoid
 end
 

src/ring_theory/polynomial/content.lean

@@ -22,7 +22,7 @@ Let `p : polynomial R`.
 ## Main Results
  - `polynomial.content_mul`:
   If `p q : polynomial R`, then `(p * q).content = p.content * q.content`.
- - `polynomial.gcd_monoid`:
+ - `polynomial.normalized_gcd_monoid`:
   The polynomial ring of a GCD domain is itself a GCD domain.
 
 -/
@@ -61,8 +61,8 @@ end primitive
 
 variables {R : Type*} [integral_domain R]
 
-section gcd_monoid
-variable [gcd_monoid R]
+section normalized_gcd_monoid
+variable [normalized_gcd_monoid R]
 
 /-- `p.content` is the `gcd` of the coefficients of `p`. -/
 def content (p : polynomial R) : R := (p.support).gcd p.coeff
@@ -432,8 +432,8 @@ begin
 end
 
 @[priority 100]
-instance gcd_monoid : gcd_monoid (polynomial R) :=
-gcd_monoid_of_exists_lcm $ λ p q, begin
+instance normalized_gcd_monoid : normalized_gcd_monoid (polynomial R) :=
+normalized_gcd_monoid_of_exists_lcm $ λ p q, begin
   rcases exists_primitive_lcm_of_is_primitive p.is_primitive_prim_part q.is_primitive_prim_part
     with ⟨r, rprim, hr⟩,
   refine ⟨C (lcm p.content q.content) * r, λ s, _⟩,
@@ -449,5 +449,5 @@ gcd_monoid_of_exists_lcm $ λ p q, begin
   tauto,
 end
 
-end gcd_monoid
+end normalized_gcd_monoid
 end polynomial

src/ring_theory/polynomial/gauss_lemma.lean

@@ -28,8 +28,8 @@ open_locale non_zero_divisors
 variables {R : Type*} [integral_domain R]
 
 namespace polynomial
-section gcd_monoid
-variable [gcd_monoid R]
+section normalized_gcd_monoid
+variable [normalized_gcd_monoid R]
 
 section
 variables {S : Type*} [integral_domain S] {φ : R →+* S} (hinj : function.injective φ)
@@ -180,5 +180,5 @@ lemma is_primitive.int.dvd_iff_map_cast_dvd_map_cast (p q : polynomial ℤ)
   (p ∣ q) ↔ (p.map (int.cast_ring_hom ℚ) ∣ q.map (int.cast_ring_hom ℚ)) :=
 hp.dvd_iff_fraction_map_dvd_fraction_map ℚ hq
 
-end gcd_monoid
+end normalized_gcd_monoid
 end polynomial