From 633c2a63af8d8668b5b269d622d902bc2ef98f0f Mon Sep 17 00:00:00 2001
From: Aaron Anderson <awainverse@gmail.com>
Date: Sat, 14 Nov 2020 19:46:53 +0000
Subject: [PATCH] feat(ring_theory/gauss_lemma): two primitive polynomials
 divide iff they do in a fraction field (#5003)

Shows `polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map`, that two primitive polynomials divide iff they do over a fraction field.
Shows `polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast`, the version for integers and rationals.
---
 src/ring_theory/polynomial/gauss_lemma.lean | 42 ++++++++++++++++++++-
 1 file changed, 41 insertions(+), 1 deletion(-)

diff --git a/src/ring_theory/polynomial/gauss_lemma.lean b/src/ring_theory/polynomial/gauss_lemma.lean
index b50bea89d76ac..5f86e08be7b52 100644
--- a/src/ring_theory/polynomial/gauss_lemma.lean
+++ b/src/ring_theory/polynomial/gauss_lemma.lean
@@ -14,8 +14,12 @@ Gauss's Lemma is one of a few results pertaining to irreducibility of primitive
 ## Main Results
  - `polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map`:
   A primitive polynomial is irreducible iff it is irreducible in a fraction field.
- - `is_primitive.int.irreducible_iff_irreducible_map_cast`:
+ - `polynomial.is_primitive.int.irreducible_iff_irreducible_map_cast`:
   A primitive polynomial over `ℤ` is irreducible iff it is irreducible over `ℚ`.
+ - `polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map`:
+  Two primitive polynomials divide each other iff they do in a fraction field.
+ - `polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast`:
+  Two primitive polynomials over `ℤ` divide each other if they do in `ℚ`.
 
 -/
 
@@ -125,6 +129,37 @@ begin
   { left,
     apply is_unit_or_eq_zero_of_is_unit_integer_normalization_prim_part f h0.1 h },
 end
+
+lemma is_primitive.dvd_of_fraction_map_dvd_fraction_map {p q : polynomial R}
+  (hp : p.is_primitive) (hq : q.is_primitive) (h_dvd : p.map f.to_map ∣ q.map f.to_map) :
+  (p ∣ q) :=
+begin
+  rcases h_dvd with ⟨r, hr⟩,
+  obtain ⟨⟨s, s0⟩, hs⟩ := @integer_normalization_map_to_map _ _ _ _ _ f r,
+  rw [algebra.smul_def, ← C_eq_algebra_map, subtype.coe_mk] at hs,
+  have h : p ∣ q * C s,
+  { use (f.integer_normalization r),
+    apply map_injective _ f.injective,
+    rw [map_mul, map_mul, hs, hr, mul_assoc, mul_comm r],
+    simp },
+  rw [← hp.dvd_prim_part_iff_dvd, prim_part_mul, hq.prim_part_eq, dvd_iff_dvd_of_rel_right] at h,
+  { exact h },
+  { symmetry,
+    rcases is_unit_prim_part_C s with ⟨u, hu⟩,
+    use u,
+    simp [hu], },
+  iterate 2 { apply mul_ne_zero hq.ne_zero,
+    rw [ne.def, C_eq_zero],
+    contrapose! s0,
+    simp [s0, mem_non_zero_divisors_iff_ne_zero] }
+end
+
+lemma is_primitive.dvd_iff_fraction_map_dvd_fraction_map {p q : polynomial R}
+  (hp : p.is_primitive) (hq : q.is_primitive) :
+  (p ∣ q) ↔ (p.map f.to_map ∣ q.map f.to_map) :=
+⟨λ ⟨a,b⟩, ⟨a.map f.to_map, b.symm ▸ (map_mul f.to_map)⟩,
+  λ h, hp.dvd_of_fraction_map_dvd_fraction_map f hq h⟩
+
 end fraction_map
 
 /-- Gauss's Lemma for `ℤ` states that a primitive integer polynomial is irreducible iff it is
@@ -134,5 +169,10 @@ theorem is_primitive.int.irreducible_iff_irreducible_map_cast
   irreducible p ↔ irreducible (p.map (int.cast_ring_hom ℚ)) :=
 hp.irreducible_iff_irreducible_map_fraction_map fraction_map.int.fraction_map
 
+lemma is_primitive.int.dvd_iff_map_cast_dvd_map_cast (p q : polynomial ℤ)
+  (hp : p.is_primitive) (hq : q.is_primitive) :
+  (p ∣ q) ↔ (p.map (int.cast_ring_hom ℚ) ∣ q.map (int.cast_ring_hom ℚ)) :=
+hp.dvd_iff_fraction_map_dvd_fraction_map fraction_map.int.fraction_map hq
+
 end gcd_monoid
 end polynomial