A polynomial ring of arbitrary number of variables over a UFD is itself a UFD.

mv_polynomial_UFD.lean

import ring_theory.unique_factorization_domain
import ring_theory.polynomial.basic
/- based on mathlib at commit 45061f3692 -/

lemma mul_equiv.is_unit_iff {R S : Type*} [monoid R] [monoid S]
  (e : R ≃* S) (r : R) : is_unit r ↔ is_unit (e r) :=
⟨is_unit.map e, λ h, by { convert h.map e.symm, simp }⟩

lemma mul_equiv.prime {R S : Type*} [comm_monoid_with_zero R] [comm_monoid_with_zero S]
  (e : R ≃* S) {r : R} (hr : prime r) : prime (e r) :=
⟨ λ h, hr.1 $ by { convert map_zero e.symm, simp [← h] },
  λ h, hr.2.1 $ by { convert h.map e.symm, simp },
  λ a b h, begin
    have : r ∣ e.symm a * e.symm b,
    { convert e.symm.to_monoid_hom.map_dvd h; simp },
    refine (hr.2.2 _ _ this).imp _ _;
    { intro h, convert e.to_monoid_hom.map_dvd h, simp },
  end⟩

/- lemmas above due to Kevin Buzzard -/

open unique_factorization_monoid
lemma mul_equiv.unique_factorization_monoid {R S : Type*}
  [cancel_comm_monoid_with_zero R] [cancel_comm_monoid_with_zero S] (e : R ≃* S)
  (hR : unique_factorization_monoid R) : unique_factorization_monoid S :=
begin
  rw iff_exists_prime_factors at hR ⊢, intros a ha,
  obtain ⟨w,hp,u,h⟩ := hR (e.symm a) (λ h, ha (by { convert ← map_zero e, simp [← h] })),
  use w.map e, split,
  { intros b hb, rw multiset.mem_map at hb,
    obtain ⟨c,hc,he⟩ := hb, rw ← he, exact e.prime (hp c hc) },
  { use units.map e.to_monoid_hom u, erw [multiset.prod_hom, ← e.map_mul, h], simp },
end

namespace mv_polynomial
variables (R : Type*) {σ : Type*}
noncomputable theory

section
variables [comm_semiring R] (s : set σ)
open_locale classical

def kill_compl : mv_polynomial σ R →ₐ[R] mv_polynomial s R :=
aeval (λ i, if h : i ∈ s then X ⟨i,h⟩ else 0)

lemma kill_compl_comp_rename : (kill_compl R s).comp (rename coe) = alg_hom.id R _ :=
alg_hom_ext (λ ⟨i,h⟩, by { dsimp, rw [rename, kill_compl, aeval_X, aeval_X], apply dif_pos h })

variables {R s}
@[simp] lemma kill_compl_rename_app (a : mv_polynomial s R) : kill_compl R s (rename coe a) = a :=
alg_hom.congr_fun (kill_compl_comp_rename R s) a

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

end

variables {R} [comm_ring R] {r : R} (hr : prime r)
include hr

lemma _root_.polynomial.prime_C : prime (polynomial.C r) :=
begin
  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 (polynomial.C_eq_zero.1 h), this],
end

variable (σ)
private lemma prime_C_of_fintype [fintype σ] : prime (C r : mv_polynomial σ R) :=
begin
  have : prime (C r : mv_polynomial (fin (fintype.card σ)) R),
  { induction fintype.card σ with d hd,
    { exact (is_empty_alg_equiv R (fin 0)).to_mul_equiv.symm.prime hr },
    { convert (fin_succ_equiv R d).to_mul_equiv.symm.prime (polynomial.prime_C hd),
      rw ← fin_succ_equiv_comp_C_eq_C, refl } },
  convert (rename_equiv R (fintype.equiv_fin σ)).to_mul_equiv.symm.prime this,
  exact (rename_C _ r).symm,
end

lemma prime_C : prime (C r : mv_polynomial σ R) :=
⟨ λ h, hr.1 (by { rw ← C_inj, rw h, simp }),
  λ h, hr.2.1 (by { rw ← constant_coeff_C r, exact is_unit.map _ h }),
  λ 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 R ↑s).to_ring_hom.map_dvd hd, simpa, simp },
    rw ← rename_C (coe : s → σ), let f := (rename (coe : s → σ)).to_ring_hom,
    exact ((prime_C_of_fintype s hr).2.2 a' b' this).imp f.map_dvd f.map_dvd,
  end ⟩

omit hr
variable {σ}
lemma prime_rename (s : set σ) {p : mv_polynomial s R}
  (hp : prime p) : prime (rename (coe : s → σ) p) :=
begin
  classical, let eqv := ((sum_alg_equiv R _ _).symm.trans $
    rename_equiv R $ (equiv.sum_comm ↥sᶜ s).trans $ equiv.set.sum_compl s),
  convert eqv.to_mul_equiv.prime (prime_C _ hp),
  suffices : (rename coe).to_ring_hom = eqv.to_alg_hom.to_ring_hom.comp C,
  /- could extract a lemma: `comp` `iter_to_sum` `C` = `rename inl` -/
  { 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

variables (R σ) [is_domain R] [unique_factorization_monoid R] 

private lemma unique_factorization_monoid_of_fintype [fintype σ] :
  unique_factorization_monoid (mv_polynomial σ R) :=
(rename_equiv R (fintype.equiv_fin σ)).to_mul_equiv.symm.unique_factorization_monoid $
begin
  induction fintype.card σ with d hd,
  { apply (is_empty_alg_equiv R (fin 0)).to_mul_equiv.symm.unique_factorization_monoid,
    apply_instance },
  { apply (fin_succ_equiv R d).to_mul_equiv.symm.unique_factorization_monoid,
    exactI polynomial.unique_factorization_monoid },
end
/- by Kevin Buzzard-/

instance : unique_factorization_monoid (mv_polynomial σ R) :=
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 R s) a' (λ h, ha (by simp [h])),
  { use w.map (rename coe), split,
    { intros b hb, rw multiset.mem_map at hb, obtain ⟨b',hb',rfl⟩ := hb,
      exact prime_rename ↑s (h b' hb') },
    { use units.map (@rename s σ R _ coe).to_ring_hom.to_monoid_hom u,
      erw [multiset.prod_hom, ← map_mul, hw] } },
end

end mv_polynomial