# mathlib3documentation

ring_theory.dedekind_domain.pid

# Proving a Dedekind domain is a PID #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Main results #

• ideal.is_principal.of_finite_maximals_of_is_unit: an invertible ideal in a commutative ring with finitely many maximal ideals, is a principal ideal.
• is_principal_ideal_ring.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} [comm_ring R] {P : ideal R} (hP : P.is_prime) [is_domain R] {x : R} (x_mem : x P) (hxP2 : x P ^ 2) (hxQ : (Q : ideal R), Q.is_prime 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 fractional_ideal.is_principal_of_unit_of_comap_mul_span_singleton_eq_top {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {S : submonoid R} [ A] (I : A)ˣ) {v : A} (hv : v I⁻¹) (h : (I * {v}) = ) :
theorem fractional_ideal.is_principal.of_finite_maximals_of_inv {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [ A] {S : submonoid R} [ A] (hS : S ) (hf : {I : | I.is_maximal}.finite) (I I' : A) (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.is_principal.of_finite_maximals_of_is_unit {R : Type u_1} [comm_ring R] (hf : {I : | I.is_maximal}.finite) {I : ideal R} (hI : is_unit I) :

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

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

theorem is_principal_ideal_ring.of_finite_primes {R : Type u_1} [comm_ring R] [is_domain R] (h : {I : | I.is_prime}.finite) :

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

theorem is_localization.over_prime.mem_normalized_factors_of_is_prime {R : Type u_1} [comm_ring R] [is_domain R] (S : Type u_2) [comm_ring S] [is_domain S] [ S] [ S] [ S] (p : ideal R) (hp0 : p ) [p.is_prime] {Sₚ : Type u_3} [comm_ring Sₚ] [ Sₚ] [ Sₚ] [ Sₚ] [is_domain Sₚ] [decidable_eq (ideal Sₚ)] {P : ideal Sₚ} (hP : P.is_prime) (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 is_dedekind_domain.is_principal_ideal_ring_localization_over_prime {R : Type u_1} [comm_ring R] [is_domain R] (S : Type u_2) [comm_ring S] [is_domain S] [ S] [ S] [ S] (p : ideal R) (hp0 : p ) [p.is_prime] {Sₚ : Type u_3} [comm_ring Sₚ] [ Sₚ] [ Sₚ] [ Sₚ] [is_domain 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.