ufd.lean

import ring_theory.dedekind_domain.ideal
import algebra.big_operators.finsupp

section associated

lemma associated_prod {γ : Type*} [comm_monoid γ]
  {s t : multiset γ}
  (h : multiset.rel associated s t) :
  associated s.prod t.prod :=
begin
  induction s using multiset.induction_on with x s ih t generalizing t,
  { rw multiset.rel_zero_left.mp h },
  { obtain ⟨y, u, h1, h2, rfl⟩ := multiset.rel_cons_left.mp h,
    rw [multiset.prod_cons, multiset.prod_cons],
    exact associated.mul_mul h1 (ih h2) }
end

end associated

namespace unique_factorization_monoid

variables {β : Type*} [comm_ring β] [is_domain β] [unique_factorization_monoid β]
--variables {β : Type*} [cancel_comm_monoid_with_zero β] [unique_factorization_monoid β]

open multiset

lemma exists_associated_pow_of_mul_eq_pow (p : ℕ) (a b c : β) (cp : is_coprime a b) (h : a*b = c^p) (hb : b ≠ 0) :
  ∃ d : β, associated a (d ^ p) :=
begin
  classical,
  obtain rfl|ha := eq_or_ne a 0,
  { use 0, rw [zero_pow _],
    rw [pos_iff_ne_zero], rintro rfl,
    rw [pow_zero, zero_mul] at h, exact zero_ne_one h },
  let fa := factors a,
  let fb := factors b,
  let fc := factors c,
  suffices : ∃ f : multiset (associates β), fa.map associates.mk = p • f,
  { obtain ⟨f, hf⟩ := this,
    obtain ⟨t, ht⟩ := map_surjective_of_surjective associates.mk_surjective f,
    refine ⟨t.prod, (factors_prod ha).symm.trans _⟩,
    rw [←prod_nsmul],
    apply associated_prod,
    rw [associates.rel_associated_iff_map_eq_map, multiset.map_nsmul, hf, ht] },
  refine exists_smul_of_dvd_count _ (λ x hx, _),
  obtain ⟨x, hx', rfl⟩ := mem_map.mp hx,
  rw count_map,
  simp_rw associates.mk_eq_mk_iff_associated,
  convert dvd_mul_right p (fc.countp (associated x)),
  rw [←countp_nsmul, ←countp_eq_card_filter],
  calc fa.countp (associated x)
      = fa.countp (associated x) + fb.countp (associated x) : _
  ... = (fa + fb).countp (associated x) : (countp_add _ fa fb).symm
  ... = (factors (a * b)).countp (associated x) : (rel.countp_eq _ _ (factors_mul ha hb)).symm
  ... = (factors (c ^ p)).countp (associated x) : by rw h
  ... = (p • fc).countp (associated x) : rel.countp_eq _ _ (factors_pow p),
  rw [eq_comm, add_right_eq_self, countp_eq_zero],
  exact λ d hdb hxd, (prime_of_factor _ hdb).not_unit
    (cp.is_unit_of_dvd' (hxd.symm.dvd.trans $ dvd_of_mem_factors hx') (dvd_of_mem_factors hdb)),
end


end unique_factorization_monoid

section is_dedekind_domain

variables {α : Type*} [comm_ring α] [is_domain α] [is_dedekind_domain α]

lemma ideal.is_unit_iff' (I : ideal α) : is_unit I ↔ I = ⊤ :=
by rw [is_unit_iff_dvd_one, ideal.dvd_iff_le, ideal.one_eq_top, top_le_iff]

example (p : nat) (a b c : ideal α) (cp : is_coprime a b) (h : a*b = c^p) :
  ∃ d : ideal α, a = d ^ p :=
begin
  obtain rfl|hb := eq_or_ne b 0,
  { rw [is_coprime_zero_right, ideal.is_unit_iff'] at cp,
    exact ⟨⊤, by rw [cp, ideal.top_pow]⟩ },
--  have := unique_factorization_monoid.exists_associated_pow_of_mul_eq_pow p a b c cp,
  sorry,
end

end is_dedekind_domain