Dedekind domains and ideals #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_invalternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.is_dedekind_domain_inv_iffshows that this does note depend on the choice of field of fractions.is_dedekind_domain.height_one_spectrumdefines the type of nonzero prime ideals ofR.
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 #
- D. Marcus, Number Fields
- J.W.S. Cassels, A. Frölich, Algebraic Number Theory
- J. Neukirch, Algebraic Number Theory
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 (non_zero_divisors R₁) K)
Equations
- fractional_ideal.has_inv K = {inv := λ (I : fractional_ideal (non_zero_divisors 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 (non_zero_divisors 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 (non_zero_divisors R₁) K}
(h : J ≠ 0) :
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 (non_zero_divisors R₁) K}
(h : J ≠ 0) :
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 (non_zero_divisors R₁) K}
(hI : I ≠ 0)
{x : K} :
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 (non_zero_divisors R₁) K}
(hI : I ≠ 0)
(hJ : J ≠ 0)
(hIJ : I ≤ J) :
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 (non_zero_divisors R₁) K}
(hI : I ≤ 1) :
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 (non_zero_divisors 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 (non_zero_divisors R₁) K} :
I * I⁻¹ = 1 ↔ ∃ (J : fractional_ideal (non_zero_divisors 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 (non_zero_divisors R₁) K} :
@[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 (non_zero_divisors 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) :
@[simp]
theorem
fractional_ideal.span_singleton_div_span_singleton
(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 y : K) :
theorem
fractional_ideal.span_singleton_div_self
(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}
(hx : x ≠ 0) :
theorem
fractional_ideal.coe_ideal_span_singleton_div_self
(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 : R₁}
(hx : x ≠ 0) :
↑(ideal.span {x}) / ↑(ideal.span {x}) = 1
theorem
fractional_ideal.span_singleton_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]
{x : K}
(hx : x ≠ 0) :
theorem
fractional_ideal.coe_ideal_span_singleton_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]
{x : R₁}
(hx : x ≠ 0) :
↑(ideal.span {x}) * (↑(ideal.span {x}))⁻¹ = 1
theorem
fractional_ideal.span_singleton_inv_mul
(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}
(hx : x ≠ 0) :
theorem
fractional_ideal.coe_ideal_span_singleton_inv_mul
(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 : R₁}
(hx : x ≠ 0) :
(↑(ideal.span {x}))⁻¹ * ↑(ideal.span {x}) = 1
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 (non_zero_divisors R₁) K]
(I : fractional_ideal (non_zero_divisors R₁) K)
[↑I.is_principal]
(h : I ≠ 0) :
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 (non_zero_divisors R₁) K)
[↑I.is_principal]
(h : I ≠ 0) :
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 (non_zero_divisors R₁) K)
[↑I.is_principal] :
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 (non_zero_divisors R₁) K)
[↑I.is_principal]
(h : I ≠ 0) :
@[protected, instance]
noncomputable
def
fractional_ideal.inv_one_class
(K : Type u_3)
[field K]
{R₁ : Type u_4}
[comm_ring R₁]
[is_domain R₁]
[algebra R₁ K]
[is_fraction_ring R₁ K] :
Equations
- fractional_ideal.inv_one_class K = {one := 1, inv := has_inv.inv (fractional_ideal.has_inv K), inv_one := _}
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 (non_zero_divisors 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 (non_zero_divisors 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 (non_zero_divisors A) x hx)) :
fractional_ideal.adjoin_integral (non_zero_divisors 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 (non_zero_divisors A) K}
(hI : I ≠ 0) :
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 (non_zero_divisors A) K}
(hI : I ≠ 0) :
@[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 (non_zero_divisors A) K}
(hI : I ≠ 0) :
is_unit I
theorem
is_dedekind_domain_inv.is_noetherian_ring
{A : Type u_2}
[comm_ring A]
[is_domain A]
(h : is_dedekind_domain_inv A) :
theorem
is_dedekind_domain_inv.integrally_closed
{A : Type u_2}
[comm_ring A]
[is_domain A]
(h : is_dedekind_domain_inv 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) :
theorem
is_dedekind_domain_inv.is_dedekind_domain
{A : Type u_2}
[comm_ring A]
[is_domain A]
(h : is_dedekind_domain_inv 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.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 ≠ ⊥) :
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 (non_zero_divisors A) K}
(hne : I ≠ 0) :
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 (non_zero_divisors A) K}
(hJ : J ≠ 0)
{I I' : fractional_ideal (non_zero_divisors A) K} :
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 (non_zero_divisors A) K}
(hJ : J ≠ 0)
{I I' : fractional_ideal (non_zero_divisors A) K} :
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 (non_zero_divisors A) K}
(hI : I ≠ 0) :
strict_mono (λ (_x : fractional_ideal (non_zero_divisors 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 (non_zero_divisors A) K}
(hI : I ≠ 0) :
@[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 (non_zero_divisors A) K) :
This is also available as _root_.div_eq_mul_inv, using the
comm_group_with_zero instance defined below.
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.semifield
{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] :
Equations
- fractional_ideal.semifield K = {add := comm_semiring.add fractional_ideal.comm_semiring, add_assoc := _, zero := comm_semiring.zero fractional_ideal.comm_semiring, zero_add := _, add_zero := _, nsmul := comm_semiring.nsmul fractional_ideal.comm_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := comm_semiring.mul fractional_ideal.comm_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := comm_semiring.one fractional_ideal.comm_semiring, one_mul := _, mul_one := _, nat_cast := comm_semiring.nat_cast fractional_ideal.comm_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := comm_semiring.npow fractional_ideal.comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, inv := λ (I : fractional_ideal (non_zero_divisors A) K), I⁻¹, div := has_div.div fractional_ideal.has_div, div_eq_mul_inv := _, zpow := division_semiring.zpow._default comm_semiring.mul _ comm_semiring.one _ _ comm_semiring.npow _ _ (λ (I : fractional_ideal (non_zero_divisors A) K), I⁻¹), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, inv_zero := _, mul_inv_cancel := _}
@[protected, instance]
def
fractional_ideal.cancel_comm_monoid_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] :
Fractional ideals have cancellative multiplication in a Dedekind domain.
Although this instance is a direct consequence of the instance
fractional_ideal.comm_group_with_zero, we define this instance to provide
a computable alternative.
Equations
- fractional_ideal.cancel_comm_monoid_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 := _, mul_left_cancel_of_ne_zero := _}
@[protected, instance]
def
ideal.cancel_comm_monoid_with_zero
{A : Type u_2}
[comm_ring A]
[is_domain A]
[is_dedekind_domain A] :
Equations
- ideal.cancel_comm_monoid_with_zero = {mul := idem_comm_semiring.mul ideal.idem_comm_semiring, mul_assoc := _, one := idem_comm_semiring.one ideal.idem_comm_semiring, one_mul := _, mul_one := _, npow := idem_comm_semiring.npow ideal.idem_comm_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _, zero := idem_comm_semiring.zero ideal.idem_comm_semiring, zero_mul := _, mul_zero := _, mul_left_cancel_of_ne_zero := _}
@[protected, instance]
theorem
ideal.dvd_iff_le
{A : Type u_2}
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I J : ideal A} :
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] :
@[protected, instance]
@[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) :
P.is_prime
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 ≠ ⊤) :
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) :
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.
GCD and LCM of ideals in a Dedekind domain #
We show that the gcd of two ideals in a Dedekind domain is just their supremum,
and the lcm is their infimum, and use this to instantiate normalized_gcd_monoid (ideal A).
@[protected, instance]
Ideals in a Dedekind domain have gcd and lcm operators that (trivially) are compatible with the normalization operator.
Equations
- ideal.normalized_gcd_monoid = {to_normalization_monoid := {norm_unit := normalization_monoid.norm_unit ideal.normalization_monoid, norm_unit_zero := _, norm_unit_mul := _, norm_unit_coe_units := _}, to_gcd_monoid := {gcd := has_sup.sup (semilattice_sup.to_has_sup (ideal A)), lcm := has_inf.inf submodule.has_inf, gcd_dvd_left := _, gcd_dvd_right := _, dvd_gcd := _, gcd_mul_lcm := _, lcm_zero_left := _, lcm_zero_right := _}, normalize_gcd := _, normalize_lcm := _}
@[simp]
theorem
ideal.gcd_eq_sup
{A : Type u_2}
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
(I J : ideal A) :
gcd_monoid.gcd I J = I ⊔ J
@[simp]
theorem
ideal.lcm_eq_inf
{A : Type u_2}
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
(I J : ideal A) :
gcd_monoid.lcm I J = I ⊓ 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 ≠ ⊥) :
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) :
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 ≠ ⊥) :
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 ^ linear_order.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) :
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) :
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
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.
Instances for is_dedekind_domain.height_one_spectrum
- is_dedekind_domain.height_one_spectrum.has_sizeof_inst
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) :
@[protected, instance]
def
is_dedekind_domain.height_one_spectrum.is_maximal
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(v : is_dedekind_domain.height_one_spectrum R) :
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) :
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) :
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) :
def
is_dedekind_domain.height_one_spectrum.equiv_maximal_spectrum
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(hR : ¬is_field R) :
An equivalence between the height one and maximal spectra for rings of Krull dimension 1.
Equations
- is_dedekind_domain.height_one_spectrum.equiv_maximal_spectrum hR = {to_fun := λ (v : is_dedekind_domain.height_one_spectrum R), {as_ideal := v.as_ideal, is_maximal := _}, inv_fun := λ (v : maximal_spectrum R), {as_ideal := v.as_ideal, is_prime := _, ne_bot := _}, left_inv := _, right_inv := _}
theorem
is_dedekind_domain.height_one_spectrum.infi_localization_eq_bot
(R : Type u_1)
(K : Type u_3)
[comm_ring R]
[field K]
[is_domain R]
[is_dedekind_domain R]
[algebra R K]
[hK : is_fraction_ring R K] :
A Dedekind domain is equal to the intersection of its localizations at all its height one non-zero prime ideals viewed as subalgebras of its field of fractions.
def
ideal_factors_fun_of_quot_hom
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
{f : R ⧸ I →+* A ⧸ J}
(hf : function.surjective ⇑f) :
The map from ideals of R dividing I to the ideals of A dividing J induced by
a homomorphism f : R/I →+* A/J
Equations
- ideal_factors_fun_of_quot_hom hf = {to_fun := λ (X : ↥{p : ideal R | p ∣ I}), ⟨ideal.comap (ideal.quotient.mk J) (ideal.map f (ideal.map (ideal.quotient.mk I) ↑X)), _⟩, monotone' := _}
@[simp]
theorem
ideal_factors_fun_of_quot_hom_coe_coe
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
{f : R ⧸ I →+* A ⧸ J}
(hf : function.surjective ⇑f)
(X : ↥{p : ideal R | p ∣ I}) :
↑(⇑(ideal_factors_fun_of_quot_hom hf) X) = ideal.comap (ideal.quotient.mk J) (ideal.map f (ideal.map (ideal.quotient.mk I) ↑X))
@[simp]
theorem
ideal_factors_fun_of_quot_hom_id
{A : Type u_2}
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{J : ideal A} :
theorem
ideal_factors_fun_of_quot_hom_comp
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
{B : Type u_4}
[comm_ring B]
[is_domain B]
[is_dedekind_domain B]
{L : ideal B}
{f : R ⧸ I →+* A ⧸ J}
{g : A ⧸ J →+* B ⧸ L}
(hf : function.surjective ⇑f)
(hg : function.surjective ⇑g) :
def
ideal_factors_equiv_of_quot_equiv
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J) :
The bijection between ideals of R dividing I and the ideals of A dividing J induced by
an isomorphism f : R/I ≅ A/J.
Equations
@[simp]
theorem
ideal_factors_equiv_of_quot_equiv_symm_apply_coe_carrier
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
(a : ↥{p : ideal A | p ∣ J}) :
↑(⇑(rel_iso.symm (ideal_factors_equiv_of_quot_equiv f)) a).carrier = ⇑(ideal.quotient.mk I) ⁻¹' ↑(ideal.map ↑(f.symm) (ideal.map (ideal.quotient.mk J) ↑a))
@[simp]
theorem
ideal_factors_equiv_of_quot_equiv_apply_coe_carrier
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
(a : ↥{p : ideal R | p ∣ I}) :
↑(⇑(ideal_factors_equiv_of_quot_equiv f) a).carrier = ⇑(ideal.quotient.mk J) ⁻¹' ↑(ideal.map ↑f (ideal.map (ideal.quotient.mk I) ↑a))
theorem
ideal_factors_equiv_of_quot_equiv_symm
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J) :
theorem
ideal_factors_equiv_of_quot_equiv_mem_normalized_factors_of_mem_normalized_factors
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
[decidable_eq (ideal R)]
[decidable_eq (ideal A)]
(hJ : J ≠ ⊥)
{L : ideal R}
(hL : L ∈ unique_factorization_monoid.normalized_factors I) :
@[simp]
theorem
normalized_factors_equiv_of_quot_equiv_apply
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
[decidable_eq (ideal R)]
[decidable_eq (ideal A)]
(hI : I ≠ ⊥)
(hJ : J ≠ ⊥)
(j : ↥{L : ideal R | L ∈ unique_factorization_monoid.normalized_factors I}) :
⇑(normalized_factors_equiv_of_quot_equiv f hI hJ) j = ⟨↑(⇑(ideal_factors_equiv_of_quot_equiv f) ⟨↑j, _⟩), _⟩
def
normalized_factors_equiv_of_quot_equiv
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
[decidable_eq (ideal R)]
[decidable_eq (ideal A)]
(hI : I ≠ ⊥)
(hJ : J ≠ ⊥) :
↥{L : ideal R | L ∈ unique_factorization_monoid.normalized_factors I} ≃ ↥{M : ideal A | M ∈ unique_factorization_monoid.normalized_factors J}
The bijection between the sets of normalized factors of I and J induced by a ring
isomorphism f : R/I ≅ A/J.
Equations
- normalized_factors_equiv_of_quot_equiv f hI hJ = {to_fun := λ (j : ↥{L : ideal R | L ∈ unique_factorization_monoid.normalized_factors I}), ⟨↑(⇑(ideal_factors_equiv_of_quot_equiv f) ⟨↑j, _⟩), _⟩, inv_fun := λ (j : ↥{M : ideal A | M ∈ unique_factorization_monoid.normalized_factors J}), ⟨↑(⇑((ideal_factors_equiv_of_quot_equiv f).symm) ⟨↑j, _⟩), _⟩, left_inv := _, right_inv := _}
@[simp]
theorem
normalized_factors_equiv_of_quot_equiv_symm
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
[decidable_eq (ideal R)]
[decidable_eq (ideal A)]
(hI : I ≠ ⊥)
(hJ : J ≠ ⊥) :
(normalized_factors_equiv_of_quot_equiv f hI hJ).symm = normalized_factors_equiv_of_quot_equiv f.symm hJ hI
theorem
normalized_factors_equiv_of_quot_equiv_multiplicity_eq_multiplicity
{R : Type u_1}
{A : Type u_2}
[comm_ring R]
[comm_ring A]
[is_domain A]
[is_dedekind_domain A]
{I : ideal R}
{J : ideal A}
[is_domain R]
[is_dedekind_domain R]
(f : R ⧸ I ≃+* A ⧸ J)
[decidable_eq (ideal R)]
[decidable_eq (ideal A)]
[decidable_rel has_dvd.dvd]
[decidable_rel has_dvd.dvd]
(hI : I ≠ ⊥)
(hJ : J ≠ ⊥)
(L : ideal R)
(hL : L ∈ unique_factorization_monoid.normalized_factors I) :
multiplicity ↑(⇑(normalized_factors_equiv_of_quot_equiv f hI hJ) ⟨L, hL⟩) J = multiplicity L I
The map normalized_factors_equiv_of_quot_equiv preserves multiplicities.
theorem
is_dedekind_domain.inf_prime_pow_eq_prod
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{ι : Type u_2}
(s : finset ι)
(f : ι → ideal R)
(e : ι → ℕ)
(prime : ∀ (i : ι), i ∈ s → _root_.prime (f i))
(coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → f i ≠ f j) :
The intersection of distinct prime powers in a Dedekind domain is the product of these prime powers.
noncomputable
def
is_dedekind_domain.quotient_equiv_pi_of_prod_eq
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{ι : Type u_2}
[fintype ι]
(I : ideal R)
(P : ι → ideal R)
(e : ι → ℕ)
(prime : ∀ (i : ι), _root_.prime (P i))
(coprime : ∀ (i j : ι), i ≠ j → P i ≠ P j)
(prod_eq : finset.univ.prod (λ (i : ι), P i ^ e i) = I) :
Chinese remainder theorem for a Dedekind domain: if the ideal I factors as
∏ i, P i ^ e i, then R ⧸ I factors as Π i, R ⧸ (P i ^ e i).
Equations
- is_dedekind_domain.quotient_equiv_pi_of_prod_eq I P e prime coprime prod_eq = (ideal.quot_equiv_of_eq _).trans (ideal.quotient_inf_ring_equiv_pi_quotient (λ (i : ι), P i ^ e i) _)
noncomputable
def
is_dedekind_domain.quotient_equiv_pi_factors
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{I : ideal R}
(hI : I ≠ ⊥) :
R ⧸ I ≃+* Π (P : ↥((unique_factorization_monoid.factors I).to_finset)), R ⧸ ↑P ^ multiset.count ↑P (unique_factorization_monoid.factors I)
Chinese remainder theorem for a Dedekind domain: R ⧸ I factors as Π i, R ⧸ (P i ^ e i),
where P i ranges over the prime factors of I and e i over the multiplicities.
Equations
- is_dedekind_domain.quotient_equiv_pi_factors hI = is_dedekind_domain.quotient_equiv_pi_of_prod_eq I (λ (P : ↥((unique_factorization_monoid.factors I).to_finset)), ↑P) (λ (P : ↥((unique_factorization_monoid.factors I).to_finset)), multiset.count ↑P (unique_factorization_monoid.factors I)) is_dedekind_domain.quotient_equiv_pi_factors._proof_1 is_dedekind_domain.quotient_equiv_pi_factors._proof_2 _
@[simp]
theorem
is_dedekind_domain.quotient_equiv_pi_factors_mk
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{I : ideal R}
(hI : I ≠ ⊥)
(x : R) :
⇑(is_dedekind_domain.quotient_equiv_pi_factors hI) (⇑(ideal.quotient.mk I) x) = λ (P : ↥((unique_factorization_monoid.factors I).to_finset)), ⇑(ideal.quotient.mk (↑P ^ multiset.count ↑P (unique_factorization_monoid.factors I))) x
noncomputable
def
ideal.quotient_mul_equiv_quotient_prod
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(I J : ideal R)
(coprime : I ⊔ J = ⊤) :
Chinese remainder theorem, specialized to two ideals.
Equations
- I.quotient_mul_equiv_quotient_prod J coprime = (ideal.quot_equiv_of_eq _).trans (I.quotient_inf_equiv_quotient_prod J coprime)
noncomputable
def
is_dedekind_domain.quotient_equiv_pi_of_finset_prod_eq
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{ι : Type u_2}
{s : finset ι}
(I : ideal R)
(P : ι → ideal R)
(e : ι → ℕ)
(prime : ∀ (i : ι), i ∈ s → _root_.prime (P i))
(coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j)
(prod_eq : s.prod (λ (i : ι), P i ^ e i) = I) :
Chinese remainder theorem for a Dedekind domain: if the ideal I factors as
∏ i in s, P i ^ e i, then R ⧸ I factors as Π (i : s), R ⧸ (P i ^ e i).
This is a version of is_dedekind_domain.quotient_equiv_pi_of_prod_eq where we restrict
the product to a finite subset s of a potentially infinite indexing type ι.
Equations
- is_dedekind_domain.quotient_equiv_pi_of_finset_prod_eq I P e prime coprime prod_eq = is_dedekind_domain.quotient_equiv_pi_of_prod_eq I (λ (i : ↥s), P ↑i) (λ (i : ↥s), e ↑i) _ _ _
theorem
is_dedekind_domain.exists_representative_mod_finset
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{ι : Type u_2}
{s : finset ι}
(P : ι → ideal R)
(e : ι → ℕ)
(prime : ∀ (i : ι), i ∈ s → _root_.prime (P i))
(coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j)
(x : Π (i : ↥s), R ⧸ P ↑i ^ e ↑i) :
Corollary of the Chinese remainder theorem: given elements x i : R / P i ^ e i,
we can choose a representative y : R such that y ≡ x i (mod P i ^ e i).
theorem
is_dedekind_domain.exists_forall_sub_mem_ideal
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
{ι : Type u_2}
{s : finset ι}
(P : ι → ideal R)
(e : ι → ℕ)
(prime : ∀ (i : ι), i ∈ s → _root_.prime (P i))
(coprime : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → P i ≠ P j)
(x : ↥s → R) :
Corollary of the Chinese remainder theorem: given elements x i : R,
we can choose a representative y : R such that y - x i ∈ P i ^ e i.
theorem
span_singleton_dvd_span_singleton_iff_dvd
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
{a b : R} :
ideal.span {a} ∣ ideal.span {b} ↔ a ∣ b
theorem
singleton_span_mem_normalized_factors_of_mem_normalized_factors
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[normalization_monoid R]
[decidable_eq R]
[decidable_eq (ideal R)]
{a b : R}
(ha : a ∈ unique_factorization_monoid.normalized_factors b) :
theorem
multiplicity_eq_multiplicity_span
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_rel has_dvd.dvd]
[decidable_rel has_dvd.dvd]
{a b : R} :
multiplicity (ideal.span {a}) (ideal.span {b}) = multiplicity a b
@[simp]
theorem
normalized_factors_equiv_span_normalized_factors_symm_apply
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_eq R]
[decidable_eq (ideal R)]
[normalization_monoid R]
{r : R}
(hr : r ≠ 0)
(b : ↥{I : ideal R | I ∈ unique_factorization_monoid.normalized_factors (ideal.span {r})}) :
noncomputable
def
normalized_factors_equiv_span_normalized_factors
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_eq R]
[decidable_eq (ideal R)]
[normalization_monoid R]
{r : R}
(hr : r ≠ 0) :
↥{d : R | d ∈ unique_factorization_monoid.normalized_factors r} ≃ ↥{I : ideal R | I ∈ unique_factorization_monoid.normalized_factors (ideal.span {r})}
The bijection between the (normalized) prime factors of r and the (normalized) prime factors
of span {r}
Equations
- normalized_factors_equiv_span_normalized_factors hr = equiv.of_bijective (λ (d : ↥{d : R | d ∈ unique_factorization_monoid.normalized_factors r}), ⟨ideal.span {↑d}, _⟩) _
@[simp]
theorem
normalized_factors_equiv_span_normalized_factors_apply_coe_carrier
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_eq R]
[decidable_eq (ideal R)]
[normalization_monoid R]
{r : R}
(hr : r ≠ 0)
(d : ↥{d : R | d ∈ unique_factorization_monoid.normalized_factors r}) :
theorem
multiplicity_normalized_factors_equiv_span_normalized_factors_eq_multiplicity
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_eq R]
[decidable_eq (ideal R)]
[normalization_monoid R]
[decidable_rel has_dvd.dvd]
[decidable_rel has_dvd.dvd]
{r d : R}
(hr : r ≠ 0)
(hd : d ∈ unique_factorization_monoid.normalized_factors r) :
multiplicity d r = multiplicity ↑(⇑(normalized_factors_equiv_span_normalized_factors hr) ⟨d, hd⟩) (ideal.span {r})
The bijection normalized_factors_equiv_span_normalized_factors between the set of prime
factors of r and the set of prime factors of the ideal ⟨r⟩ preserves multiplicities.
theorem
multiplicity_normalized_factors_equiv_span_normalized_factors_symm_eq_multiplicity
{R : Type u_1}
[comm_ring R]
[is_domain R]
[is_principal_ideal_ring R]
[decidable_eq R]
[decidable_eq (ideal R)]
[normalization_monoid R]
[decidable_rel has_dvd.dvd]
[decidable_rel has_dvd.dvd]
{r : R}
(hr : r ≠ 0)
(I : ↥{I : ideal R | I ∈ unique_factorization_monoid.normalized_factors (ideal.span {r})}) :
multiplicity ↑(⇑((normalized_factors_equiv_span_normalized_factors hr).symm) I) r = multiplicity ↑I (ideal.span {r})
The bijection normalized_factors_equiv_span_normalized_factors.symm between the set of prime
factors of the ideal ⟨r⟩ and the set of prime factors of r preserves multiplicities.