Criteria under which a Dedekind domain is a PID #
This file contains some results that we can use to test wether 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_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 = Ideal.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.
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 : FractionalIdeal S A)
(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
IsPrincipalIdealRing.of_finite_primes
{R : Type u_1}
[CommRing R]
[IsDedekindDomain R]
(h : {I : Ideal R | I.IsPrime}.Finite)
:
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]
[Module.Free 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]
[Module.Free 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]
:
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.