mathlib3 documentation

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 #

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] [is_dedekind_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_finite_maximals_of_inv {R : Type u_1} [comm_ring R] {A : Type u_2} [comm_ring A] [algebra R A] {S : submonoid R} [is_localization S A] (hS : S non_zero_divisors R) (hf : {I : ideal R | I.is_maximal}.finite) (I I' : fractional_ideal S 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

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

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

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

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ₚ.

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.