English
If a commutative domain R is a unique factorization domain and there exists an irreducible element p such that any two irreducibles are associated, then R is a principal ideal ring (every ideal is generated by a single element).
Русский
Если кольцо R коммутативно, является областью уникального факторизации и существует ирредуцируемый элемент p, при котором любые ирредуцируемые элементы являются ассоциированы между собой, то R — кольцо с порождающими идеалами одним элементом (первый признак пид).
LaTeX
$$$\mathrm{IsPrincipalIdealRing}(R)$$$
Lean4
theorem aux_pid_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) :
IsPrincipalIdealRing R := by
classical
constructor
intro I
by_cases I0 : I = ⊥
· rw [I0]
use 0
simp only [Set.singleton_zero, Submodule.span_zero]
obtain ⟨x, hxI, hx0⟩ : ∃ x ∈ I, x ≠ (0 : R) := I.ne_bot_iff.mp I0
obtain ⟨p, _, H⟩ := HasUnitMulPowIrreducibleFactorization.of_ufd_of_unique_irreducible h₁ h₂
have ex : ∃ n : ℕ, p ^ n ∈ I := by
obtain ⟨n, u, rfl⟩ := H hx0
refine ⟨n, ?_⟩
simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hxI
constructor
use p ^ Nat.find ex
change I = Ideal.span _
apply le_antisymm
· intro r hr
by_cases hr0 : r = 0
· simp only [hr0, Submodule.zero_mem]
obtain ⟨n, u, rfl⟩ := H hr0
simp only [mem_span_singleton, Units.isUnit, IsUnit.dvd_mul_right]
apply pow_dvd_pow
apply Nat.find_min'
simpa only [Units.mul_inv_cancel_right] using I.mul_mem_right (↑u⁻¹) hr
· rw [span_singleton_le_iff_mem]
exact Nat.find_spec ex
