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 #
IsDedekindDomainInv
alternatively defines a Dedekind domain as an integral domain where every nonzero fractional ideal is invertible.isDedekindDomainInv_iff
shows that this does note depend on the choice of field of fractions.IsDedekindDomain.HeightOneSpectrum
defines 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 : ¬ IsField 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
Equations
- FractionalIdeal.instInvNonZeroDivisors K = { inv := fun (I : FractionalIdeal (nonZeroDivisors R₁) K) => 1 / I }
I⁻¹
is the inverse of I
if I
has an inverse.
Equations
- FractionalIdeal.instInvOneClassNonZeroDivisors = InvOneClass.mk ⋯
A Dedekind domain is an integral domain such that every fractional ideal has an inverse.
This is equivalent to IsDedekindDomain
.
In particular we provide a fractional_ideal.comm_group_with_zero
instance,
assuming IsDedekindDomain A
, which implies IsDedekindDomainInv
. For integral ideals,
IsDedekindDomain
(_inv
) implies only Ideal.cancelCommMonoidWithZero
.
Equations
- IsDedekindDomainInv A = ∀ (I : FractionalIdeal (nonZeroDivisors A) (FractionRing A)), I ≠ ⊥ → I * I⁻¹ = 1
Instances For
Showing one side of the equivalence between the definitions
IsDedekindDomainInv
and IsDedekindDomain
of Dedekind domains.
Specialization of exists_primeSpectrum_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_primeSpectrum_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
.
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.
Nonzero fractional ideals in a Dedekind domain are units.
This is also available as _root_.mul_inv_cancel
, using the
Semifield
instance defined below.
This is also available as _root_.div_eq_mul_inv
, using the
Semifield
instance defined below.
IsDedekindDomain
and IsDedekindDomainInv
are equivalent ways
to express that an integral domain is a Dedekind domain.
Equations
- FractionalIdeal.semifield K = Semifield.mk ⋯ zpowRec ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯
Fractional ideals have cancellative multiplication in a Dedekind domain.
Although this instance is a direct consequence of the instance
FractionalIdeal.semifield
, we define this instance to provide
a computable alternative.
Equations
- FractionalIdeal.cancelCommMonoidWithZero K = CancelCommMonoidWithZero.mk
Equations
- Ideal.cancelCommMonoidWithZero = CancelCommMonoidWithZero.mk
For ideals in a Dedekind domain, to divide is to contain.
Equations
- Ideal.normalizationMonoid = normalizationMonoidOfUniqueUnits
Strengthening of IsLocalization.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 NormalizedGCDMonoid (Ideal A)
.
Ideals in a Dedekind domain have gcd and lcm operators that (trivially) are compatible with the normalization operator.
Equations
- Ideal.instNormalizedGCDMonoid = NormalizedGCDMonoid.mk ⋯ ⋯
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 HeightOneSpectrum
and provide lemmas to recover the facts that prime ideals of height
one are prime and irreducible.
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.
- asIdeal : Ideal R
- isPrime : self.asIdeal.IsPrime
Instances For
An equivalence between the height one and maximal spectra for rings of Krull dimension 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
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
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
The bijection between the sets of normalized factors of I and J induced by a ring
isomorphism f : R/I ≅ A/J
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map normalizedFactorsEquivOfQuotEquiv
preserves multiplicities.
The number of times an ideal I
occurs as normalized factor of another ideal J
is stable
when regarding at these ideals as associated elements of the monoid of ideals.
The intersection of distinct prime powers in a Dedekind domain is the product of these prime powers.
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
- IsDedekindDomain.quotientEquivPiOfProdEq I P e prime coprime prod_eq = (Ideal.quotEquivOfEq ⋯).trans (Ideal.quotientInfRingEquivPiQuotient (fun (i : ι) => P i ^ e i) ⋯)
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
Chinese remainder theorem for a Dedekind domain: if the ideal I
factors as
∏ i ∈ s, P i ^ e i
, then R ⧸ I
factors as Π (i : s), R ⧸ (P i ^ e i)
.
This is a version of IsDedekindDomain.quotientEquivPiOfProdEq
where we restrict
the product to a finite subset s
of a potentially infinite indexing type ι
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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)
.
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
.
The bijection between the (normalized) prime factors of r
and the (normalized) prime factors
of span {r}
Equations
- normalizedFactorsEquivSpanNormalizedFactors hr = Equiv.ofBijective (fun (d : ↑{d : R | d ∈ UniqueFactorizationMonoid.normalizedFactors r}) => ⟨Ideal.span {↑d}, ⋯⟩) ⋯
Instances For
The bijection normalizedFactorsEquivSpanNormalizedFactors
between the set of prime
factors of r
and the set of prime factors of the ideal ⟨r⟩
preserves multiplicities. See
count_normalizedFactorsSpan_eq_count
for the version stated in terms of multisets count
.
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.
The bijection between the set of prime factors of the ideal ⟨r⟩
and the set of prime factors
of r
preserves count
of the corresponding multisets. See
multiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_multiplicity
for the version
stated in terms of multiplicity.
The finite set of all prime factors of the pushforward of p
.
Equations
- primesOverFinset p B = (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap A B) p)).toFinset