# Documentation

Mathlib.RingTheory.DedekindDomain.PID

# Proving a Dedekind domain is a PID #

This file contains some results that we can use to show 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} [] {P : } (hP : ) [] [] {x : R} (x_mem : x P) (hxP2 : ¬x P ^ 2) (hxQ : ∀ (Q : ), Q P¬x Q) :

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} [] [] [Algebra R A] {S : } [] (I : ()ˣ) {v : A} (hv : v I⁻¹) (h : Submodule.comap () (I * Submodule.span R {v}) = ) :
theorem FractionalIdeal.isPrincipal.of_finite_maximals_of_inv {R : Type u_1} [] {A : Type u_2} [] [Algebra R A] {S : } [] (hS : ) (hf : Set.Finite {I | }) (I : ) (I' : ) (hinv : I * I' = 1) :

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} [] (hf : Set.Finite {I | }) {I : } (hI : IsUnit 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} [] [] [] (h : Set.Finite {I | }) :

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

theorem IsLocalization.OverPrime.mem_normalizedFactors_of_isPrime {R : Type u_1} [] [] [] (S : Type u_2) [] [] [Algebra R S] [] [] (p : ) (hp0 : p ) [] {Sₚ : Type u_3} [CommRing Sₚ] [Algebra S Sₚ] [] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsDomain Sₚ] [] [DecidableEq (Ideal Sₚ)] {P : Ideal Sₚ} (hP : ) (hP0 : 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} [] [] [] (S : Type u_2) [] [] [Algebra R S] [] [] (p : ) (hp0 : p ) [] {Sₚ : Type u_3} [CommRing Sₚ] [Algebra S Sₚ] [] [Algebra R Sₚ] [IsScalarTower R S 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.