Criteria under which a Dedekind domain is a PID

This file contains some results that we can use to test whether all ideals in a Dedekind domain are principal.

Main results

• Ideal.IsPrincipal.of_finite_maximals_of_isUnit: an invertible ideal in a commutative ring with finitely many maximal ideals, is a principal ideal.
• IsPrincipalIdealRing.of_finite_primes: if a Dedekind domain has finitely many prime ideals, it is a principal ideal domain.

theorem Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne {R : Type u_1} [CommRing R] {P : Ideal R} (hP : P.IsPrime) [IsDedekindDomain R] {x : R} (x_mem : x ∈ P) (hxP2 : x ∉ P ^ 2) (hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q) : P = span {x}

Let P be a prime ideal, x ∈ P \ P² and x ∉ Q for all prime ideals Q ≠ P. Then P is generated by x.

@[deprecated Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne (since := "2025-05-23")]

theorem Ideal.eq_span_singleton_of_mem_of_not_mem_sq_of_not_mem_prime_ne {R : Type u_1} [CommRing R] {P : Ideal R} (hP : P.IsPrime) [IsDedekindDomain R] {x : R} (x_mem : x ∈ P) (hxP2 : x ∉ P ^ 2) (hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q) : P = span {x}

Alias of Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne.

---

Let P be a prime ideal, x ∈ P \ P² and x ∉ Q for all prime ideals Q ≠ P. Then P is generated by x.

theorem FractionalIdeal.isPrincipal_of_unit_of_comap_mul_span_singleton_eq_top {R : Type u_2} {A : Type u_3} [CommRing R] [CommRing A] [Algebra R A] {S : Submonoid R} [IsLocalization S A] (I : (FractionalIdeal S A)ˣ) {v : A} (hv : v ∈ ↑I⁻¹) (h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤) : (↑↑I).IsPrincipal

theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv {R : Type u_1} [CommRing R] {A : Type u_2} [CommRing A] [Algebra R A] {S : Submonoid R} [IsLocalization S A] (hS : S ≤ nonZeroDivisors R) (hf : {I : Ideal R | I.IsMaximal}.Finite) (I I' : FractionalIdeal S A) (hinv : I * I' = 1) : (↑I).IsPrincipal

An invertible fractional ideal of a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857

theorem Ideal.IsPrincipal.of_finite_maximals_of_isUnit {R : Type u_1} [CommRing R] (hf : {I : Ideal R | I.IsMaximal}.Finite) {I : Ideal R} (hI : IsUnit ↑I) : Submodule.IsPrincipal I

An invertible ideal in a commutative ring with finitely many maximal ideals is principal.

https://math.stackexchange.com/a/95857

theorem IsPrincipalIdealRing.of_finite_primes {R : Type u_1} [CommRing R] [IsDedekindDomain R] (h : {I : Ideal R | I.IsPrime}.Finite) : IsPrincipalIdealRing R

A Dedekind domain is a PID if its set of primes is finite.

theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] (p : Ideal R) (hp0 : p ≠ ⊥) [p.IsPrime] {Sₚ : Type u_3} [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsDedekindDomain Sₚ] [IsDomain S] {P : Ideal Sₚ} (hP : P.IsPrime) (hP0 : P ≠ ⊥) : P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R Sₚ) p)

If p is a prime in the Dedekind domain R, S an extension of R and Sₚ the localization of S at p, then all primes in Sₚ are factors of the image of p in Sₚ.

theorem IsDedekindDomain.isPrincipalIdealRing_localization_over_prime {R : Type u_1} [CommRing R] [IsDedekindDomain R] (S : Type u_2) [CommRing S] [Algebra R S] [NoZeroSMulDivisors R S] [Module.Finite R S] (p : Ideal R) (hp0 : p ≠ ⊥) [p.IsPrime] {Sₚ : Type u_3} [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsDedekindDomain Sₚ] [IsDomain S] : IsPrincipalIdealRing Sₚ

Let p be a prime in the Dedekind domain R and S be an integral extension of R, then the localization Sₚ of S at p is a PID.