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] [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) :

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.

source

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] [algebra R A] {S : submonoid R} [is_localization S A] (I : (fractional_ideal S A)ˣ) {v : A} (hv : v ∈ ↑I⁻¹) (h : submodule.comap (algebra.linear_map R A) (↑I * submodule.span R {v}) = ⊤) :

↑I.is_principal

source

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) :

↑I.is_principal

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

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

source

theorem ideal.is_principal.of_finite_maximals_of_is_unit {R : Type u_1} [comm_ring R] (hf : {I : ideal R | I.is_maximal}.finite) {I : ideal R} (hI : is_unit ↑I) :

submodule.is_principal I

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

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

source

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

is_principal_ideal_ring R

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

source

theorem is_localization.over_prime.mem_normalized_factors_of_is_prime {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (S : Type u_2) [comm_ring S] [is_domain S] [algebra R S] [module.free R S] [module.finite R S] (p : ideal R) (hp0 : p ≠ ⊥) [p.is_prime] {Sₚ : Type u_3} [comm_ring Sₚ] [algebra S Sₚ] [is_localization (algebra.algebra_map_submonoid S p.prime_compl) Sₚ] [algebra R Sₚ] [is_scalar_tower R S Sₚ] [is_domain Sₚ] [is_dedekind_domain Sₚ] [decidable_eq (ideal Sₚ)] {P : ideal Sₚ} (hP : P.is_prime) (hP0 : P ≠ ⊥) :

P ∈ unique_factorization_monoid.normalized_factors (ideal.map (algebra_map 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ₚ.

source

theorem is_dedekind_domain.is_principal_ideal_ring_localization_over_prime {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (S : Type u_2) [comm_ring S] [is_domain S] [algebra R S] [module.free R S] [module.finite R S] (p : ideal R) (hp0 : p ≠ ⊥) [p.is_prime] {Sₚ : Type u_3} [comm_ring Sₚ] [algebra S Sₚ] [is_localization (algebra.algebra_map_submonoid S p.prime_compl) Sₚ] [algebra R Sₚ] [is_scalar_tower R S Sₚ] [is_domain Sₚ] [is_dedekind_domain Sₚ] :

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