English
A unique factorization domain with at least one irreducible element and in which all irreducibles are associated is a discrete valuation ring.
Русский
Уникальный факторизационный домен, имеющий хотя бы один ирредуцируемый элемент и такой, что все ирредуцируемые элементы ассоциированы, является дискретным оценочным кольцом.
LaTeX
$$$\mathrm{IsDiscreteValuationRing}(R)$$$
Lean4
/-- A unique factorization domain with at least one irreducible element
in which all irreducible elements are associated
is a discrete valuation ring.
-/
theorem of_ufd_of_unique_irreducible {R : Type u} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R]
(h₁ : ∃ p : R, Irreducible p) (h₂ : ∀ ⦃p q : R⦄, Irreducible p → Irreducible q → Associated p q) :
IsDiscreteValuationRing R := by
rw [iff_pid_with_one_nonzero_prime]
haveI PID : IsPrincipalIdealRing R := aux_pid_of_ufd_of_unique_irreducible R h₁ h₂
obtain ⟨p, hp⟩ := h₁
refine ⟨PID, ⟨Ideal.span { p }, ⟨?_, ?_⟩, ?_⟩⟩
· rw [Submodule.ne_bot_iff]
exact ⟨p, Ideal.mem_span_singleton.mpr (dvd_refl p), hp.ne_zero⟩
· rwa [Ideal.span_singleton_prime hp.ne_zero, ← UniqueFactorizationMonoid.irreducible_iff_prime]
· intro I
rw [← Submodule.IsPrincipal.span_singleton_generator I]
rintro ⟨I0, hI⟩
apply span_singleton_eq_span_singleton.mpr
apply h₂ _ hp
rw [Ne, Submodule.span_singleton_eq_bot] at I0
rwa [UniqueFactorizationMonoid.irreducible_iff_prime, ← Ideal.span_singleton_prime I0]
