feat(ring_theory/polynomial): mv_polynomial over UFD is UFD (#12866)

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

docs/overview.yaml

@@ -85,7 +85,7 @@ General algebra:
     $K[X]$ is Euclidean: 'polynomial.euclidean_domain'
     Hilbert basis theorem: 'polynomial.is_noetherian_ring'
     $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'
+    $A[{X_i}]$ is a UFD when $A$ is a UFD: 'mv_polynomial.unique_factorization_monoid'
     irreducible polynomial: 'irreducible'
     Eisenstein's criterion: 'polynomial.irreducible_of_eisenstein_criterion'
     polynomial in several indeterminates: 'mv_polynomial'

docs/undergrad.yaml

@@ -144,7 +144,7 @@ Ring Theory:
     unique factorisation domain (UFD): 'unique_factorization_monoid'
     greatest common divisor: 'gcd_monoid.gcd'
     least common multiple: 'gcd_monoid.lcm'
-    $A[X]$ is a UFD when $A$ is a UFD: 'polynomial.unique_factorization_monoid'
+    $A[{X_i}]$ is a UFD when $A$ is a UFD: 'mv_polynomial.unique_factorization_monoid'
     principal ideal domain: 'submodule.is_principal'
     Euclidean rings: 'euclidean_domain'
     Euclid's' algorithm: 'nat.xgcd'

src/algebra/associated.lean

@@ -63,6 +63,21 @@ end prime
 @[simp] lemma not_prime_one : ¬ prime (1 : α) :=
 λ h, h.not_unit is_unit_one
 
+section map
+variables [comm_monoid_with_zero β] {F : Type*} {G : Type*}
+  [monoid_with_zero_hom_class F α β] [mul_hom_class G β α] (f : F) (g : G) {p : α}
+
+lemma comap_prime (hinv : ∀ a, g (f a : β) = a) (hp : prime (f p)) : prime p :=
+⟨ λ h, hp.1 $ by simp [h],  λ h, hp.2.1 $ h.map f,  λ a b h, by
+  { refine (hp.2.2 (f a) (f b) $ by { convert map_dvd f h, simp }).imp _ _;
+    { intro h, convert ← map_dvd g h; apply hinv } } ⟩
+
+lemma mul_equiv.prime_iff (e : α ≃* β) : prime p ↔ prime (e p) :=
+⟨ λ h, comap_prime e.symm e (λ a, by simp) $ (e.symm_apply_apply p).substr h,
+  comap_prime e e.symm (λ a, by simp) ⟩
+
+end map
+
 end prime
 
 lemma prime.left_dvd_or_dvd_right_of_dvd_mul [cancel_comm_monoid_with_zero α] {p : α}

src/algebra/divisibility.lean

@@ -75,13 +75,14 @@ theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
 
 section map_dvd
 
-variables {M N : Type*}
+variables {M N : Type*} [monoid M] [monoid N]
 
-lemma mul_hom.map_dvd [monoid M] [monoid N] (f : mul_hom M N) {a b} : a ∣ b → f a ∣ f b
-| ⟨c, h⟩ := ⟨f c, h.symm ▸ f.map_mul a c⟩
+lemma map_dvd {F : Type*} [mul_hom_class F M N] (f : F) {a b} : a ∣ b → f a ∣ f b
+| ⟨c, h⟩ := ⟨f c, h.symm ▸ map_mul f a c⟩
 
-lemma monoid_hom.map_dvd [monoid M] [monoid N] (f : M →* N) {a b} : a ∣ b → f a ∣ f b :=
-f.to_mul_hom.map_dvd
+lemma mul_hom.map_dvd (f : mul_hom M N) {a b} : a ∣ b → f a ∣ f b := map_dvd f
+
+lemma monoid_hom.map_dvd (f : M →* N) {a b} : a ∣ b → f a ∣ f b := map_dvd f
 
 end map_dvd
 

src/algebra/ring/basic.lean

@@ -602,8 +602,7 @@ variables [semiring α] {a : α}
 
 @[simp] theorem two_dvd_bit0 : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
 
-lemma ring_hom.map_dvd [semiring β] (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
-f.to_monoid_hom.map_dvd
+lemma ring_hom.map_dvd [semiring β] (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b := map_dvd f
 
 end semiring
 

src/data/mv_polynomial/rename.lean

@@ -105,6 +105,24 @@ begin
   exact finsupp.map_domain_injective (finsupp.map_domain_injective hf)
 end
 
+section
+variables {f : σ → τ} (hf : function.injective f)
+open_locale classical
+
+/-- Given a function between sets of variables `f : σ → τ` that is injective with proof `hf`,
+  `kill_compl hf` is the `alg_hom` from `R[τ]` to `R[σ]` that is left inverse to
+  `rename f : R[σ] → R[τ]` and sends the variables in the complement of the range of `f` to `0`. -/
+def kill_compl : mv_polynomial τ R →ₐ[R] mv_polynomial σ R :=
+aeval (λ i, if h : i ∈ set.range f then X $ (equiv.of_injective f hf).symm ⟨i,h⟩ else 0)
+
+lemma kill_compl_comp_rename : (kill_compl hf).comp (rename f) = alg_hom.id R _ := alg_hom_ext $
+λ i, by { dsimp, rw [rename, kill_compl, aeval_X, aeval_X, dif_pos, equiv.of_injective_symm_apply] }
+
+@[simp] lemma kill_compl_rename_app (p : mv_polynomial σ R) : kill_compl hf (rename f p) = p :=
+alg_hom.congr_fun (kill_compl_comp_rename hf) p
+
+end
+
 section
 variables (R)
 
@@ -178,6 +196,21 @@ begin
     { simp only [rename_rename, rename_X, subtype.coe_mk, alg_hom.map_mul], refl, }, },
 end
 
+/-- `exists_finset_rename` for two polyonomials at once: for any two polynomials `p₁`, `p₂` in a
+  polynomial semiring `R[σ]` of possibly infinitely many variables, `exists_finset_rename₂` yields
+  a finite subset `s` of `σ` such that both `p₁` and `p₂` are contained in the polynomial semiring
+  `R[s]` of finitely many variables. -/
+lemma exists_finset_rename₂ (p₁ p₂ : mv_polynomial σ R) :
+  ∃ (s : finset σ) (q₁ q₂ : mv_polynomial s R), p₁ = rename coe q₁ ∧ p₂ = rename coe q₂ :=
+begin
+  obtain ⟨s₁,q₁,rfl⟩ := exists_finset_rename p₁,
+  obtain ⟨s₂,q₂,rfl⟩ := exists_finset_rename p₂,
+  classical, use s₁ ∪ s₂,
+  use rename (set.inclusion $ s₁.subset_union_left s₂) q₁,
+  use rename (set.inclusion $ s₁.subset_union_right s₂) q₂,
+  split; simpa,
+end
+
 /-- Every polynomial is a polynomial in finitely many variables. -/
 theorem exists_fin_rename (p : mv_polynomial σ R) :
   ∃ (n : ℕ) (f : fin n → σ) (hf : injective f) (q : mv_polynomial (fin n) R), p = rename f q :=

src/ring_theory/polynomial/basic.lean

@@ -20,8 +20,9 @@ import ring_theory.unique_factorization_domain
   Hilbert basis theorem, that if a ring is noetherian then so is its polynomial ring.
 * `polynomial.wf_dvd_monoid`:
   If an integral domain is a `wf_dvd_monoid`, then so is its polynomial ring.
-* `polynomial.unique_factorization_monoid`:
-  If an integral domain is a `unique_factorization_monoid`, then so is its polynomial ring.
+* `polynomial.unique_factorization_monoid`, `mv_polynomial.unique_factorization_monoid`:
+  If an integral domain is a `unique_factorization_monoid`, then so is its polynomial ring (of any
+  number of variables).
 -/
 
 noncomputable theory
@@ -651,7 +652,64 @@ is_noetherian_submodule_left.1 (is_noetherian_of_fg_of_noetherian _
 
 end ideal
 
+section prime
+variables (σ) {r : R}
+
+namespace polynomial
+lemma prime_C_iff : prime (C r) ↔ prime r :=
+⟨ comap_prime C (eval_ring_hom (0 : R)) (λ r, eval_C),
+  λ hr, by { have := hr.1,
+    rw ← ideal.span_singleton_prime at hr ⊢,
+    { convert ideal.is_prime_map_C_of_is_prime hr using 1,
+      rw [ideal.map_span, set.image_singleton] },
+    exacts [λ h, this (C_eq_zero.1 h), this] } ⟩
+end polynomial
+
+namespace mv_polynomial
+
+private lemma prime_C_iff_of_fintype [fintype σ] : prime (C r : mv_polynomial σ R) ↔ prime r :=
+begin
+  rw (rename_equiv R (fintype.equiv_fin σ)).to_mul_equiv.prime_iff,
+  convert_to prime (C r) ↔ _, { congr, apply rename_C },
+  { symmetry, induction fintype.card σ with d hd,
+    { exact (is_empty_alg_equiv R (fin 0)).to_mul_equiv.symm.prime_iff },
+    { rw [hd, ← polynomial.prime_C_iff],
+      convert (fin_succ_equiv R d).to_mul_equiv.symm.prime_iff,
+      rw ← fin_succ_equiv_comp_C_eq_C, refl } },
+end
+
+lemma prime_C_iff : prime (C r : mv_polynomial σ R) ↔ prime r :=
+⟨ comap_prime C constant_coeff constant_coeff_C,
+  λ hr, ⟨ λ h, hr.1 $ by { rw [← C_inj, h], simp },
+    λ h, hr.2.1 $ by { rw ← constant_coeff_C r, exact h.map _ },
+    λ a b hd, begin
+      obtain ⟨s,a',b',rfl,rfl⟩ := exists_finset_rename₂ a b,
+      rw ← algebra_map_eq at hd, have : algebra_map R _ r ∣ a' * b',
+      { convert (kill_compl subtype.coe_injective).to_ring_hom.map_dvd hd, simpa, simp },
+      rw ← rename_C (coe : s → σ), let f := (rename (coe : s → σ)).to_ring_hom,
+      exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp f.map_dvd f.map_dvd,
+    end ⟩ ⟩
+
+variable {σ}
+lemma prime_rename_iff (s : set σ) {p : mv_polynomial s R} :
+  prime (rename (coe : s → σ) p) ↔ prime p :=
+begin
+  classical, symmetry, let eqv := (sum_alg_equiv R _ _).symm.trans
+    (rename_equiv R $ (equiv.sum_comm ↥sᶜ s).trans $ equiv.set.sum_compl s),
+  rw [← prime_C_iff ↥sᶜ, eqv.to_mul_equiv.prime_iff], convert iff.rfl,
+  suffices : (rename coe).to_ring_hom = eqv.to_alg_hom.to_ring_hom.comp C,
+  { apply ring_hom.congr_fun this },
+  { apply ring_hom_ext,
+    { intro, dsimp [eqv], erw [iter_to_sum_C_C, rename_C, rename_C] },
+    { intro, dsimp [eqv], erw [iter_to_sum_C_X, rename_X, rename_X], refl } },
+end
+
+end mv_polynomial
+
+end prime
+
 namespace polynomial
+
 @[priority 100]
 instance {R : Type*} [comm_ring R] [is_domain R] [wf_dvd_monoid R] :
   wf_dvd_monoid R[X] :=
@@ -1062,10 +1120,11 @@ def quotient_equiv_quotient_mv_polynomial (I : ideal R) :
 
 end mv_polynomial
 
-namespace polynomial
+section unique_factorization_domain
+variables {D : Type u} [comm_ring D] [is_domain D] [unique_factorization_monoid D] (σ)
 open unique_factorization_monoid
 
-variables {D : Type u} [comm_ring D] [is_domain D] [unique_factorization_monoid D]
+namespace polynomial
 
 @[priority 100]
 instance unique_factorization_monoid : unique_factorization_monoid (polynomial D) :=
@@ -1076,3 +1135,32 @@ begin
 end
 
 end polynomial
+
+namespace mv_polynomial
+
+private lemma unique_factorization_monoid_of_fintype [fintype σ] :
+  unique_factorization_monoid (mv_polynomial σ D) :=
+(rename_equiv D (fintype.equiv_fin σ)).to_mul_equiv.symm.unique_factorization_monoid $
+begin
+  induction fintype.card σ with d hd,
+  { apply (is_empty_alg_equiv D (fin 0)).to_mul_equiv.symm.unique_factorization_monoid,
+    apply_instance },
+  { apply (fin_succ_equiv D d).to_mul_equiv.symm.unique_factorization_monoid,
+    exactI polynomial.unique_factorization_monoid },
+end
+
+@[priority 100]
+instance : unique_factorization_monoid (mv_polynomial σ D) :=
+begin
+  rw iff_exists_prime_factors,
+  intros a ha, obtain ⟨s,a',rfl⟩ := exists_finset_rename a,
+  obtain ⟨w,h,u,hw⟩ := iff_exists_prime_factors.1
+    (unique_factorization_monoid_of_fintype s) a' (λ h, ha $ by simp [h]),
+  exact ⟨ w.map (rename coe),
+    λ b hb, let ⟨b',hb',he⟩ := multiset.mem_map.1 hb in he ▸ (prime_rename_iff ↑s).2 (h b' hb'),
+    units.map (@rename s σ D _ coe).to_ring_hom.to_monoid_hom u,
+    by erw [multiset.prod_hom, ← map_mul, hw] ⟩,
+end
+
+end mv_polynomial
+end unique_factorization_domain

src/ring_theory/unique_factorization_domain.lean

@@ -314,6 +314,26 @@ theorem unique_factorization_monoid.iff_exists_prime_factors [cancel_comm_monoid
 ⟨λ h, @unique_factorization_monoid.exists_prime_factors _ _ h,
   unique_factorization_monoid.of_exists_prime_factors⟩
 
+section
+variables {β : Type*} [cancel_comm_monoid_with_zero α] [cancel_comm_monoid_with_zero β]
+
+lemma mul_equiv.unique_factorization_monoid (e : α ≃* β)
+  (hα : unique_factorization_monoid α) : unique_factorization_monoid β :=
+begin
+  rw unique_factorization_monoid.iff_exists_prime_factors at hα ⊢, intros a ha,
+  obtain ⟨w,hp,u,h⟩ := hα (e.symm a) (λ h, ha $ by { convert ← map_zero e, simp [← h] }),
+  exact ⟨ w.map e,
+    λ b hb, let ⟨c,hc,he⟩ := multiset.mem_map.1 hb in he ▸ e.prime_iff.1 (hp c hc),
+    units.map e.to_monoid_hom u,
+    by { erw [multiset.prod_hom, ← e.map_mul, h], simp } ⟩,
+end
+
+lemma mul_equiv.unique_factorization_monoid_iff (e : α ≃* β) :
+  unique_factorization_monoid α ↔ unique_factorization_monoid β :=
+⟨ e.unique_factorization_monoid, e.symm.unique_factorization_monoid ⟩
+
+end
+
 theorem irreducible_iff_prime_of_exists_unique_irreducible_factors [cancel_comm_monoid_with_zero α]
   (eif : ∀ (a : α), a ≠ 0 → ∃ f : multiset α, (∀b ∈ f, irreducible b) ∧ f.prod ~ᵤ a)
   (uif : ∀ (f g : multiset α),