Invertible ideals in commutative semi-local rings are principal.

principal_invertible.lean

import ring_theory.dedekind_domain.ideal
/- https://math.stackexchange.com/a/95857/12932 -/

open_locale non_zero_divisors big_operators

namespace submodule 
variables {R M N P : Type*}
variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid N] [add_comm_monoid P]
variables [module R M] [module R N] [module R P]

theorem map₂_span_singleton_eq_map (f : M →ₗ[R] N →ₗ[R] P) (m : M) :
  map₂ f (span R {m}) = map (f m) :=
begin
  funext, rw map₂_eq_span_image2, apply le_antisymm,
  { rw [span_le, set.image2_subset_iff],
    intros x hx y hy,
    obtain ⟨a, rfl⟩ := mem_span_singleton.1 hx,
    rw [f.map_smul],
    exact smul_mem _ a (mem_map_of_mem hy) },
  { rintro _ ⟨n, hn, rfl⟩,
    exact subset_span ⟨m, n, mem_span_singleton_self m, hn, rfl⟩ },
end

end submodule

variables {R : Type*} [comm_ring R]

theorem is_principal_ideal_ring.of_finite_maximals
  (hf : {I : ideal R | I.is_maximal}.finite)
  {I : ideal R} (hI : is_unit (I : fractional_ideal R⁰ (fraction_ring R))) :
  I.is_principal :=
begin
  let s := hf.to_finset,
  let f : ideal R → submodule R _ := is_localization.coe_submodule (fraction_ring R),
  haveI := classical.dec_eq (ideal R),
  have coprime : ∀ (M ∈ s) (M' ∈ s.erase M), M ⊔ M' = ⊤,
  { simp_rw [finset.mem_erase, hf.mem_to_finset],
    rintro M hM M' ⟨hne, hM'⟩, by_contra,
    exact hne (hM'.eq_of_le hM.ne_top $ le_sup_right.trans_eq (hM.eq_of_le h le_sup_left).symm) },
  have nle : ∀ M ∈ s, ¬ (⨅ (M' ∈ s.erase M), M') ≤ M := λ M hM, left_lt_sup.1
    ((hf.mem_to_finset.1 hM).ne_top.lt_top.trans_eq (ideal.sup_infi_eq_top $ coprime M hM).symm),
  have hsm : strict_mono f := is_localization.coe_submodule_strict_mono le_rfl,
  have hinj : function.injective f := is_localization.coe_submodule_injective _ le_rfl,
  let I' : submodule R (fraction_ring R) := ↑hI.unit⁻¹,
  have hinv := hI.mul_coe_inv,
  rw [subtype.ext_iff, fractional_ideal.coe_mul] at hinv,
  have : ∀ (M : ideal R) (hM : M ∈ s), ∃ (a ∈ I) (b ∈ I'), a • b ∉ f M,
  { simp_rw algebra.smul_def,
    intros M hM, by_contra' h,
    rw [hf.mem_to_finset] at hM,
    obtain ⟨x, hx, hxM⟩ := set_like.exists_of_lt ((hsm hM.ne_top.lt_top).trans_eq hinv.symm),
    refine hxM (submodule.map₂_le.2 _ hx),
    rintro _ ⟨y, hy, rfl⟩, apply h y hy },
  choose! a ha b hb hm using this,
  choose! u hu hum using λ M hM, set_like.not_le_iff_exists.1 (nle M hM),
  let v := ∑ M in s, u M • b M,
  have hv : v ∈ I' := submodule.sum_mem _ (λ M hM, submodule.smul_mem _ _ $ hb M hM),
  let J := submodule.comap (algebra.linear_map R $ fraction_ring R) (f I * submodule.span R {v}),
  have hJ : f J = f I * submodule.span R {v},
  { apply le_antisymm, { exact submodule.map_comap_le _ _ },
    intros x hx,
    obtain ⟨y, hy, rfl⟩ := (submodule.mul_le_mul_right _).trans_eq hinv hx,
    { exact submodule.mem_map_of_mem hx },
    exact (submodule.span_singleton_le_iff_mem _ _).2 hv },
  by_cases J = ⊤,
  { have : (1 : fraction_ring R) ∈ f I * submodule.span R {v},
    { rw [← hJ, h], exact ⟨1, trivial, (algebra_map R _).map_one⟩ },
    rw [mul_comm] at this,
    let L := (linear_map.mul R $ fraction_ring R),
    have hle := (congr_fun (submodule.map₂_span_singleton_eq_map L v) $ f I).le,
    obtain ⟨_, ⟨w, hw, rfl⟩, hvw⟩ := hle this,
    refine ⟨⟨w, hinj _⟩⟩,
    rw fractional_ideal.coe_one at hinv, change f I * I' = 1 at hinv,
    suffices : I' * f (ideal.span {w}) = 1,
    { refine trans _ (one_mul _), erw [← hinv, mul_assoc, this, mul_one] },
    apply le_antisymm,
    { rw [← hinv, mul_comm],
      apply submodule.mul_le_mul_left,
      apply hsm.monotone (I.span_singleton_le_iff_mem.2 hw) },
    { rw [submodule.one_le, ← hvw],
      exact submodule.mul_mem_mul hv ⟨w, ideal.mem_span_singleton_self w, rfl⟩ } },
  obtain ⟨M, hM, hJM⟩ := ideal.exists_le_maximal _ h,
  replace hM := hf.mem_to_finset.2 hM,
  have hmem := hJ.ge.trans (hsm.monotone hJM) (submodule.mul_mem_mul
    (submodule.mem_map_of_mem $ ha M hM) $ submodule.mem_span_singleton_self _),
  have : ∀ (a ∈ I) (b ∈ I'), ∃ c, algebra_map R _ c = a • b,
  { intros a ha b hb, have hi := hinv.le,
    obtain ⟨c, -, hc⟩ := hi (submodule.mul_mem_mul (submodule.mem_map_of_mem ha) hb),
    exact ⟨c, hc.trans (algebra.smul_def _ _).symm⟩ },
  simp_rw [finset.mul_sum, algebra.linear_map_apply,
    ← algebra.smul_def, smul_smul, mul_comm (a _), ← smul_smul] at hmem,
  rw [← s.add_sum_erase _ hM, submodule.add_mem_iff_left] at hmem,
  { refine (hm M hM _).elim,
    obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M hM),
    rw ← hc at hmem ⊢,
    rw [algebra.smul_def, ← map_mul] at hmem,
    obtain ⟨d, hdM, he⟩ := hmem,
    rw is_localization.injective _ le_rfl he at hdM,
    exact submodule.mem_map_of_mem
      (((hf.mem_to_finset.1 hM).is_prime.mem_or_mem hdM).resolve_left $ hum M hM) },
  { refine submodule.sum_mem _ (λ M' hM', _),
    rw finset.mem_erase at hM',
    obtain ⟨c, hc⟩ := this _ (ha M hM) _ (hb M' hM'.2),
    rw [← hc, algebra.smul_def, ← map_mul],
    apply submodule.mem_map_of_mem, apply ideal.mul_mem_right,
    specialize hu M' hM'.2,
    simp_rw ideal.mem_infi at hu,
    exact hu M (finset.mem_erase_of_ne_of_mem hM'.1.symm hM) },
end

/-- A Dedekind domain is a PID if its set of primes is finite. -/
theorem is_principal_ideal_ring.of_finite_primes [is_domain R] [is_dedekind_domain R]
  (h : {I : ideal R | I.is_prime}.finite) :
  is_principal_ideal_ring R :=
⟨λ I, begin
  obtain rfl | hI := eq_or_ne I ⊥,
  { exact bot_is_principal },
  apply is_principal_ideal_ring.of_finite_maximals,
  { apply h.subset, exact @ideal.is_maximal.is_prime _ _ },
  { exact is_unit_of_mul_eq_one _ _ (fractional_ideal.coe_ideal_mul_inv I hI) },
end⟩