A saturated submonoid (with zero) of a unique factorization monoid is itself a unique factorization monoid.

saturated_submonoid_UFM.lean

import ring_theory.unique_factorization_domain

variables {α : Type*} [cancel_comm_monoid_with_zero α] (s : submonoid α) [hmem : fact ((0 : α) ∈ s)]

abbreviation semi_saturated := ∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → a * b ∈ s → b ∈ s
abbreviation saturated := ∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → b ∣ a → b ∈ s
-- a ≠ 0 → a * b ∈ s → b ∈ s

instance [hs : fact (saturated s)] : fact (semi_saturated s) :=
let hs := hs.out in ⟨λ a b ha hn hab, begin
  by_cases a * b = 0,
  { rw [(no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero h).resolve_left hn, ← h], exact hab },
  { exact hs hab h (dvd_mul_left b a) },
end ⟩

include hmem

namespace submonoid

instance cancel_comm_monoid_with_zero : cancel_comm_monoid_with_zero s :=
{ zero := ⟨0, hmem.out⟩,
  zero_mul := λ _, by { ext, apply zero_mul },
  mul_zero := λ _, by { ext, apply mul_zero },
  mul_left_cancel_of_ne_zero := λ a b c ha he, by { ext,
    exact cancel_monoid_with_zero.mul_left_cancel_of_ne_zero
      (λ h, ha $ by { ext, exact h }) (subtype.ext_iff.1 he) },
  mul_right_cancel_of_ne_zero := λ a b c ha he, by { ext,
    exact cancel_monoid_with_zero.mul_right_cancel_of_ne_zero
      (λ h, ha $ by { ext, exact h }) (subtype.ext_iff.1 he) },
.. submonoid.to_comm_monoid s }

omit hmem

variables {s} [hs : fact (semi_saturated s)] {a b : s}

lemma _root_.irreducible.ne_zero' {a : s} (hi : irreducible a) : a.1 ≠ 0 :=
λ h, by { haveI : fact ((0 : α) ∈ s) := ⟨h ▸ a.2⟩, exact hi.ne_zero (subtype.ext h) }

include hs

lemma is_unit_iff : is_unit a ↔ is_unit a.1 :=
⟨ by { repeat { rw is_unit_iff_exists_inv }, exact λ ⟨b,h⟩, ⟨b, subtype.ext_iff.1 h⟩ },
  λ hu, by { cases subsingleton_or_nontrivial α; resetI,
    { refine ⟨⟨a,a,_,_⟩,rfl⟩; apply subsingleton.elim },
    { have := hu.ne_zero, replace hs := hs.out,
      rw is_unit_iff_exists_inv at hu ⊢, obtain ⟨b,h⟩ := hu,
      exact ⟨⟨b, hs a.2 this $ by { rw h, exact s.one_mem }⟩, subtype.ext h ⟩ } } ⟩

lemma dvd_iff : a ∣ b ↔ a.1 ∣ b.1 :=
⟨ λ ⟨c,h⟩, ⟨c.1, subtype.ext_iff.1 h⟩,
  λ ⟨c,he⟩, begin
    by_cases a.1 = 0, { use a, ext, convert he, simpa [h] }, replace hs := hs.out,
    exact ⟨⟨c, hs a.2 h $ by { convert b.2, rw he }⟩, subtype.ext he⟩,
  end ⟩

include hmem
lemma prime_of_coe_prime (hp : prime a.1) : prime a :=
⟨ λ h, hp.1 (subtype.ext_iff.1 h), λ h, hp.2.1 $ is_unit_iff.1 h,
  λ b c h, by { rw [dvd_iff, dvd_iff], exact hp.2.2 b.1 c.1 (dvd_iff.1 h) } ⟩
omit hmem

omit hs
variable [hs' : fact (saturated s)]
include hs'

lemma mem_of_is_unit {a : α} (hu : is_unit a) : a ∈ s :=
begin
  cases subsingleton_or_nontrivial α; resetI,
  { convert s.one_mem },
  { have hs := hs'.out, exact hs s.one_mem one_ne_zero (is_unit_iff_dvd_one.1 hu) },
end

lemma irreducible_iff : irreducible a ↔ irreducible a.1 :=
⟨ λ hi, ⟨ λ hu, hi.not_unit $ is_unit_iff.2 hu, 
    λ b c h, begin
      have hs := hs'.out,
      have he : a = ⟨b, hs a.2 hi.ne_zero' $ by { rw h, apply dvd_mul_right }⟩ * 
        ⟨c, hs a.2 hi.ne_zero' $ by { rw h, apply dvd_mul_left }⟩
        := subtype.ext h,
      have := hi.is_unit_or_is_unit he, repeat {rw is_unit_iff at this}, exact this,
  end ⟩,
  λ hi, ⟨ λ hu, hi.not_unit $ is_unit_iff.1 hu,
    λ b c h, by { repeat {rw is_unit_iff},
    exact hi.is_unit_or_is_unit (subtype.ext_iff.1 h) } ⟩ ⟩

include hmem
lemma ufm (hα : unique_factorization_monoid α) : unique_factorization_monoid s :=
begin
  rw unique_factorization_monoid.iff_exists_prime_factors at hα ⊢,
  intros a ha, have hs := hs'.out, have ha' : a.1 ≠ 0 := λ h, ha (subtype.ext h),
  obtain ⟨w,h,u,hw⟩ := hα a ha',
  have : ∀ b ∈ w, b ∈ s,
  { intros b hb, refine hs a.2 ha' ((multiset.dvd_prod hb).trans _),
    convert dvd_mul_right _ _, exact hw.symm },
  use w.attach.map (λ b, ⟨b, this b b.2⟩), split,
  { rintro ⟨b,hb⟩ hm, rw multiset.mem_map at hm,
    obtain ⟨⟨c,hc⟩,_,he⟩ := hm, rw ← he,
    exact prime_of_coe_prime (h c hc) },
  have : is_unit (⟨u, mem_of_is_unit u.is_unit⟩ : s) := is_unit_iff.2 u.is_unit,
  use this.unit, ext, change _ * ↑u = _, convert ← hw,
  convert ← multiset.prod_hom _ s.subtype, rw multiset.map_map,
  convert w.attach_map_val using 1,
end

lemma prime_iff [h : unique_factorization_monoid α] : prime a ↔ prime a.1 :=
by { rw [←h.irreducible_iff_prime, ←(ufm h).irreducible_iff_prime], exacts [irreducible_iff, hs'] }

end submonoid