mathlib documentation

ring_theory.dedekind_domain.ideal

Dedekind domains and ideals #

In this file, we show a ring is a Dedekind domain iff all fractional ideals are invertible. Then we prove some results on the unique factorization monoid structure of the ideals.

Main definitions #

is_dedekind_domain_inv alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.
is_dedekind_domain_inv_iff shows that this does note depend on the choice of field of fractions.
is_dedekind_domain.height_one_spectrum defines the type of nonzero prime ideals of R.

Main results: #

Implementation notes #

The definitions that involve a field of fractions choose a canonical field of fractions, but are independent of that choice. The ..._iff lemmas express this independence.

Often, definitions assume that Dedekind domains are not fields. We found it more practical to add a (h : ¬ is_field A) assumption whenever this is explicitly needed.

References #

Tags #

dedekind domain, dedekind ring

@[protected, instance]

noncomputable def fractional_ideal.has_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] :

has_inv (fractional_ideal R₁⁰ K)

Equations

fractional_ideal.has_inv K = {inv := λ (I : fractional_ideal R₁⁰ K), 1 / I}

theorem fractional_ideal.inv_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I : fractional_ideal R₁⁰ K} :

I⁻¹ = 1 / I

theorem fractional_ideal.inv_zero' (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] :

theorem fractional_ideal.inv_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :

J⁻¹ = ⟨↑1 / ↑J, _⟩

theorem fractional_ideal.coe_inv_of_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :

↑J⁻¹ = is_localization.coe_submodule K ⊤ / ↑J

theorem fractional_ideal.mem_inv_iff {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I : fractional_ideal R₁⁰ K} (hI : I ≠ 0) {x : K} :

x ∈ I⁻¹ ↔ ∀ (y : K), y ∈ I → x * y ∈ 1

theorem fractional_ideal.inv_anti_mono {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I J : fractional_ideal R₁⁰ K} (hI : I ≠ 0) (hJ : J ≠ 0) (hIJ : I ≤ J) :

J⁻¹ ≤ I⁻¹

theorem fractional_ideal.le_self_mul_inv {K : Type u_3} [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I : fractional_ideal R₁⁰ K} (hI : I ≤ 1) :

I ≤ I * I⁻¹

theorem fractional_ideal.coe_ideal_le_self_mul_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (I : ideal R₁) :

↑I ≤ (↑I) * (↑I)⁻¹

theorem fractional_ideal.right_inverse_eq (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (I J : fractional_ideal R₁⁰ K) (h : I * J = 1) :

I⁻¹ is the inverse of I if I has an inverse.

theorem fractional_ideal.mul_inv_cancel_iff (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I : fractional_ideal R₁⁰ K} :

I * I⁻¹ = 1 ↔ ∃ (J : fractional_ideal R₁⁰ K), I * J = 1

theorem fractional_ideal.mul_inv_cancel_iff_is_unit (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {I : fractional_ideal R₁⁰ K} :

I * I⁻¹ = 1 ↔ is_unit I

@[simp]

theorem fractional_ideal.map_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] {K' : Type u_5} [field K'] [algebra R₁ K'] [is_fraction_ring R₁ K'] (I : fractional_ideal R₁⁰ K) (h : K ≃ₐ[R₁] K') :

fractional_ideal.map ↑h I⁻¹ = (fractional_ideal.map ↑h I)⁻¹

@[simp]

theorem fractional_ideal.span_singleton_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (x : K) :

(fractional_ideal.span_singleton R₁⁰ x)⁻¹ = fractional_ideal.span_singleton R₁⁰ x⁻¹

theorem fractional_ideal.mul_generator_self_inv (K : Type u_3) [field K] {R₁ : Type u_1} [comm_ring R₁] [algebra R₁ K] [is_localization R₁⁰ K] (I : fractional_ideal R₁⁰ K) [↑I.is_principal] (h : I ≠ 0) :

I * fractional_ideal.span_singleton R₁⁰ (submodule.is_principal.generator ↑I)⁻¹ = 1

theorem fractional_ideal.invertible_of_principal (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (I : fractional_ideal R₁⁰ K) [↑I.is_principal] (h : I ≠ 0) :

I * I⁻¹ = 1

theorem fractional_ideal.invertible_iff_generator_nonzero (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (I : fractional_ideal R₁⁰ K) [↑I.is_principal] :

I * I⁻¹ = 1 ↔ submodule.is_principal.generator ↑I ≠ 0

theorem fractional_ideal.is_principal_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] (I : fractional_ideal R₁⁰ K) [↑I.is_principal] (h : I ≠ 0) :

I⁻¹.val.is_principal

@[simp]

theorem fractional_ideal.one_inv (K : Type u_3) [field K] {R₁ : Type u_4} [comm_ring R₁] [is_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K] :

def is_dedekind_domain_inv (A : Type u_2) [comm_ring A] [is_domain A] :

Prop

A Dedekind domain is an integral domain such that every fractional ideal has an inverse.

This is equivalent to is_dedekind_domain. In particular we provide a fractional_ideal.comm_group_with_zero instance, assuming is_dedekind_domain A, which implies is_dedekind_domain_inv. For integral ideals, is_dedekind_domain(_inv) implies only ideal.cancel_comm_monoid_with_zero.

Equations

is_dedekind_domain_inv A = ∀ (I : fractional_ideal A⁰ (fraction_ring A)), I ≠ ⊥ → I * I⁻¹ = 1

theorem is_dedekind_domain_inv_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] :

is_dedekind_domain_inv A ↔ ∀ (I : fractional_ideal A⁰ K), I ≠ ⊥ → I * I⁻¹ = 1

theorem fractional_ideal.adjoin_integral_eq_one_of_is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] (x : K) (hx : is_integral A x) (hI : is_unit (fractional_ideal.adjoin_integral A⁰ x hx)) :

fractional_ideal.adjoin_integral A⁰ x hx = 1

theorem is_dedekind_domain_inv.mul_inv_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] (h : is_dedekind_domain_inv A) {I : fractional_ideal A⁰ K} (hI : I ≠ 0) :

I * I⁻¹ = 1

theorem is_dedekind_domain_inv.inv_mul_eq_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] (h : is_dedekind_domain_inv A) {I : fractional_ideal A⁰ K} (hI : I ≠ 0) :

I⁻¹ * I = 1

@[protected]

theorem is_dedekind_domain_inv.is_unit {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] (h : is_dedekind_domain_inv A) {I : fractional_ideal A⁰ K} (hI : I ≠ 0) :

theorem is_dedekind_domain_inv.is_noetherian_ring {A : Type u_2} [comm_ring A] [is_domain A] (h : is_dedekind_domain_inv A) :

is_noetherian_ring A

theorem is_dedekind_domain_inv.integrally_closed {A : Type u_2} [comm_ring A] [is_domain A] (h : is_dedekind_domain_inv A) :

is_integrally_closed A

theorem is_dedekind_domain_inv.dimension_le_one {A : Type u_2} [comm_ring A] [is_domain A] (h : is_dedekind_domain_inv A) :

ring.dimension_le_one A

theorem is_dedekind_domain_inv.is_dedekind_domain {A : Type u_2} [comm_ring A] [is_domain A] (h : is_dedekind_domain_inv A) :

is_dedekind_domain A

Showing one side of the equivalence between the definitions is_dedekind_domain_inv and is_dedekind_domain of Dedekind domains.

theorem exists_multiset_prod_cons_le_and_prod_not_le {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] (hNF : ¬is_field A) {I M : ideal A} (hI0 : I ≠ ⊥) (hIM : I ≤ M) [hM : M.is_maximal] :

∃ (Z : multiset (prime_spectrum A)), (M ::ₘ multiset.map prime_spectrum.as_ideal Z).prod ≤ I ∧ ¬(multiset.map prime_spectrum.as_ideal Z).prod ≤ I

Specialization of exists_prime_spectrum_prod_le_and_ne_bot_of_domain to Dedekind domains: Let I : ideal A be a nonzero ideal, where A is a Dedekind domain that is not a field. Then exists_prime_spectrum_prod_le_and_ne_bot_of_domain states we can find a product of prime ideals that is contained within I. This lemma extends that result by making the product minimal: let M be a maximal ideal that contains I, then the product including M is contained within I and the product excluding M is not contained within I.

theorem fractional_ideal.exists_not_mem_one_of_ne_bot {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] (hNF : ¬is_field A) {I : ideal A} (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :

∃ (x : K), x ∈ (↑I)⁻¹ ∧ x ∉ 1

theorem fractional_ideal.one_mem_inv_coe_ideal {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] {I : ideal A} (hI : I ≠ ⊥) :

1 ∈ (↑I)⁻¹

theorem fractional_ideal.mul_inv_cancel_of_le_one {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [h : is_dedekind_domain A] {I : ideal A} (hI0 : I ≠ ⊥) (hI : ((↑I) * (↑I)⁻¹)⁻¹ ≤ 1) :

(↑I) * (↑I)⁻¹ = 1

theorem fractional_ideal.coe_ideal_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [h : is_dedekind_domain A] (I : ideal A) (hI0 : I ≠ ⊥) :

(↑I) * (↑I)⁻¹ = 1

Nonzero integral ideals in a Dedekind domain are invertible.

We will use this to show that nonzero fractional ideals are invertible, and finally conclude that fractional ideals in a Dedekind domain form a group with zero.

@[protected]

theorem fractional_ideal.mul_inv_cancel {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] {I : fractional_ideal A⁰ K} (hne : I ≠ 0) :

I * I⁻¹ = 1

Nonzero fractional ideals in a Dedekind domain are units.

This is also available as _root_.mul_inv_cancel, using the comm_group_with_zero instance defined below.

theorem fractional_ideal.mul_right_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] {J : fractional_ideal A⁰ K} (hJ : J ≠ 0) {I I' : fractional_ideal A⁰ K} :

I * J ≤ I' * J ↔ I ≤ I'

theorem fractional_ideal.mul_left_le_iff {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] {J : fractional_ideal A⁰ K} (hJ : J ≠ 0) {I I' : fractional_ideal A⁰ K} :

J * I ≤ J * I' ↔ I ≤ I'

theorem fractional_ideal.mul_right_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] {I : fractional_ideal A⁰ K} (hI : I ≠ 0) :

strict_mono (λ (_x : fractional_ideal A⁰ K), _x * I)

theorem fractional_ideal.mul_left_strict_mono {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] {I : fractional_ideal A⁰ K} (hI : I ≠ 0) :

strict_mono (has_mul.mul I)

@[protected]

theorem fractional_ideal.div_eq_mul_inv {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [algebra A K] [is_fraction_ring A K] [is_dedekind_domain A] (I J : fractional_ideal A⁰ K) :

I / J = I * J⁻¹

This is also available as _root_.div_eq_mul_inv, using the comm_group_with_zero instance defined below.

theorem is_dedekind_domain_iff_is_dedekind_domain_inv {A : Type u_2} [comm_ring A] [is_domain A] :

is_dedekind_domain A ↔ is_dedekind_domain_inv A

is_dedekind_domain and is_dedekind_domain_inv are equivalent ways to express that an integral domain is a Dedekind domain.

@[protected, instance]

noncomputable def fractional_ideal.comm_group_with_zero {A : Type u_2} (K : Type u_3) [comm_ring A] [field K] [is_domain A] [is_dedekind_domain A] [algebra A K] [is_fraction_ring A K] :

comm_group_with_zero (fractional_ideal A⁰ K)

Equations

fractional_ideal.comm_group_with_zero K = {mul := comm_semiring.mul fractional_ideal.comm_semiring, mul_assoc := _, one := comm_semiring.one fractional_ideal.comm_semiring, one_mul := _, mul_one := _, npow := comm_semiring.npow fractional_ideal.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := comm_semiring.zero fractional_ideal.comm_semiring, zero_mul := _, mul_zero := _, inv := λ (I : fractional_ideal A⁰ K), I⁻¹, div := has_div.div fractional_ideal.fractional_ideal_has_div, div_eq_mul_inv := _, zpow := group_with_zero.zpow._default comm_semiring.mul _ comm_semiring.one _ _ comm_semiring.npow _ _ (λ (I : fractional_ideal A⁰ K), I⁻¹), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}

@[protected, instance]

noncomputable def ideal.cancel_comm_monoid_with_zero {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] :

cancel_comm_monoid_with_zero (ideal A)

Equations

ideal.cancel_comm_monoid_with_zero = function.injective.cancel_comm_monoid_with_zero ⇑(fractional_ideal.coe_ideal_hom A⁰ (fraction_ring A)) ideal.cancel_comm_monoid_with_zero._proof_2 ideal.cancel_comm_monoid_with_zero._proof_3 ideal.cancel_comm_monoid_with_zero._proof_4 ideal.cancel_comm_monoid_with_zero._proof_5 ideal.cancel_comm_monoid_with_zero._proof_6

theorem ideal.dvd_iff_le {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {I J : ideal A} :

I ∣ J ↔ J ≤ I

For ideals in a Dedekind domain, to divide is to contain.

theorem ideal.dvd_not_unit_iff_lt {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {I J : ideal A} :

dvd_not_unit I J ↔ J < I

@[protected, instance]

def ideal.wf_dvd_monoid {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] :

wf_dvd_monoid (ideal A)

@[protected, instance]

def ideal.unique_factorization_monoid {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] :

unique_factorization_monoid (ideal A)

@[protected, instance]

noncomputable def ideal.normalization_monoid {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] :

normalization_monoid (ideal A)

Equations

ideal.normalization_monoid = normalization_monoid_of_unique_units

@[simp]

theorem ideal.dvd_span_singleton {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {I : ideal A} {x : A} :

I ∣ ideal.span {x} ↔ x ∈ I

theorem ideal.is_prime_of_prime {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {P : ideal A} (h : prime P) :

theorem ideal.prime_of_is_prime {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {P : ideal A} (hP : P ≠ ⊥) (h : P.is_prime) :

theorem ideal.prime_iff_is_prime {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] {P : ideal A} (hP : P ≠ ⊥) :

prime P ↔ P.is_prime

In a Dedekind domain, the (nonzero) prime elements of the monoid with zero ideal A are exactly the prime ideals.

theorem ideal.strict_anti_pow {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] (I : ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) :

strict_anti (pow I)

theorem ideal.pow_lt_self {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] (I : ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (e : ℕ) (he : 2 ≤ e) :

I ^ e < I

theorem ideal.exists_mem_pow_not_mem_pow_succ {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] (I : ideal A) (hI0 : I ≠ ⊥) (hI1 : I ≠ ⊤) (e : ℕ) :

∃ (x : A) (H : x ∈ I ^ e), x ∉ I ^ (e + 1)

theorem associates.le_singleton_iff {A : Type u_2} [comm_ring A] [is_domain A] [is_dedekind_domain A] (x : A) (n : ℕ) (I : ideal A) :

associates.mk I ^ n ≤ associates.mk (ideal.span {x}) ↔ x ∈ I ^ n

theorem ideal.exist_integer_multiples_not_mem {A : Type u_2} {K : Type u_3} [comm_ring A] [field K] [is_domain A] [is_dedekind_domain A] [algebra A K] [is_fraction_ring A K] {J : ideal A} (hJ : J ≠ ⊤) {ι : Type u_1} (s : finset ι) (f : ι → K) {j : ι} (hjs : j ∈ s) (hjf : f j ≠ 0) :

∃ (a : K), (∀ (i : ι), i ∈ s → is_localization.is_integer A (a * f i)) ∧ ∃ (i : ι) (H : i ∈ s), a * f i ∉ ↑J

Strengthening of is_localization.exist_integer_multiples: Let J ≠ ⊤ be an ideal in a Dedekind domain A, and f ≠ 0 a finite collection of elements of K = Frac(A), then we can multiply the elements of f by some a : K to find a collection of elements of A that is not completely contained in J.

theorem prod_normalized_factors_eq_self {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I : ideal T} (hI : I ≠ ⊥) :

(unique_factorization_monoid.normalized_factors I).prod = I

theorem normalized_factors_prod {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {α : multiset (ideal T)} (h : ∀ (p : ideal T), p ∈ α → prime p) :

unique_factorization_monoid.normalized_factors α.prod = α

theorem count_le_of_ideal_ge {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I J : ideal T} (h : I ≤ J) (hI : I ≠ ⊥) (K : ideal T) :

multiset.count K (unique_factorization_monoid.normalized_factors J) ≤ multiset.count K (unique_factorization_monoid.normalized_factors I)

theorem sup_eq_prod_inf_factors {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I J : ideal T} (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :

I ⊔ J = (unique_factorization_monoid.normalized_factors I ∩ unique_factorization_monoid.normalized_factors J).prod

theorem irreducible_pow_sup {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I J : ideal T} (hI : I ≠ ⊥) (hJ : irreducible J) (n : ℕ) :

J ^ n ⊔ I = J ^ min (multiset.count J (unique_factorization_monoid.normalized_factors I)) n

theorem irreducible_pow_sup_of_le {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I J : ideal T} (hJ : irreducible J) (n : ℕ) (hn : ↑n ≤ multiplicity J I) :

J ^ n ⊔ I = J ^ n

theorem irreducible_pow_sup_of_ge {T : Type u_4} [comm_ring T] [is_domain T] [is_dedekind_domain T] {I J : ideal T} (hI : I ≠ ⊥) (hJ : irreducible J) (n : ℕ) (hn : multiplicity J I ≤ ↑n) :

J ^ n ⊔ I = J ^ (multiplicity J I).get _

Height one spectrum of a Dedekind domain #

If R is a Dedekind domain of Krull dimension 1, the maximal ideals of R are exactly its nonzero prime ideals. We define height_one_spectrum and provide lemmas to recover the facts that prime ideals of height one are prime and irreducible.

theorem is_dedekind_domain.height_one_spectrum.ext {R : Type u_1} {_inst_1 : comm_ring R} {_inst_5 : is_domain R} {_inst_6 : is_dedekind_domain R} (x y : is_dedekind_domain.height_one_spectrum R) (h : x.as_ideal = y.as_ideal) :

x = y

@[nolint, ext]

structure is_dedekind_domain.height_one_spectrum (R : Type u_1) [comm_ring R] [is_domain R] [is_dedekind_domain R] :

Type u_1

as_ideal : ideal R
is_prime : self.as_ideal.is_prime
ne_bot : self.as_ideal ≠ ⊥

The height one prime spectrum of a Dedekind domain R is the type of nonzero prime ideals of R. Note that this equals the maximal spectrum if R has Krull dimension 1.

theorem is_dedekind_domain.height_one_spectrum.ext_iff {R : Type u_1} {_inst_1 : comm_ring R} {_inst_5 : is_domain R} {_inst_6 : is_dedekind_domain R} (x y : is_dedekind_domain.height_one_spectrum R) :

x = y ↔ x.as_ideal = y.as_ideal

theorem is_dedekind_domain.height_one_spectrum.prime {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

prime v.as_ideal

theorem is_dedekind_domain.height_one_spectrum.irreducible {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

irreducible v.as_ideal

theorem is_dedekind_domain.height_one_spectrum.associates_irreducible {R : Type u_1} [comm_ring R] [is_domain R] [is_dedekind_domain R] (v : is_dedekind_domain.height_one_spectrum R) :

irreducible (associates.mk v.as_ideal)