Complements on ideals of a Dedekind domain

This file collects general facts about ideals and height-one primes of a Dedekind domain, complementing Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean. In particular, it develops the predicate Ideal.IsPrimeTo I S, saying that I is nonzero and divisible by no prime in S, together with its induction principle Ideal.IsPrimeTo.induction_on and its transport Ideal.isPrimeTo_comap_iff along a ring isomorphism.

The predicate is closed under products (Ideal.isPrimeTo_mul_iff, its finite form Ideal.isPrimeTo_prod_iff) and powers (Ideal.isPrimeTo_pow_iff), and forbidding one more prime is Ideal.isPrimeTo_insert_iff. Complementing a set of primes turns it into a support condition: IsPrimeTo I Sᶜ says that every prime factor of I lies in S. The two extreme cases are Ideal.isPrimeTo_univ_iff (no prime factor at all, so I = ⊤) and Ideal.isPrimeTo_compl_singleton_iff (a single allowed prime, so I is a prime power), and Ideal.IsPrimeTo.exists_eq_pow_mul splits off one allowed prime at a time. The file also records the prime-power factorization Ideal.exists_eq_prod_pow of an arbitrary nonzero ideal. Together with the uniqueness statement Ideal.eq_and_eq_of_pow_mul_eq_pow_mul and the relative primality Ideal.IsPrimeTo.isRelPrime of ideals supported on complementary sets, these are what turn a finite set of primes into a finite Euler product in TauCeti/NumberTheory/ArithmeticDirichletSeries/EulerProduct/Basic.lean.

It also collects how an isomorphism e : R ≃+* R' moves ideals: Ideal.map e preserves divisibility (Ideal.map_dvd_map_iff_of_ringEquiv, Ideal.map_pow_dvd_map_iff_of_ringEquiv, stated over commutative semirings, since the proofs use only that Ideal.map e and Ideal.map e.symm are mutually inverse) and factorisation multiplicities (Ideal.count_factors_map_of_ringEquiv), and Mathlib's transport equivOfRingEquiv e of height one primes is Ideal.map e on underlying ideals (IsDedekindDomain.HeightOneSpectrum.asIdeal_equivOfRingEquiv). Those four are the ideal-level input to the adic-valuation transport in TauCeti/RingTheory/DedekindDomain/AdicValuation/Transport.lean; they are adapted from AINTLIB (Apache-2.0), commit 513e83879e2f, projects/HasseWeil/HasseWeil/WeilPairing/DivisorGalois.lean. The inverse transport (equivOfRingEquiv e).symm is Ideal.comap e on underlying ideals (IsDedekindDomain.HeightOneSpectrum.asIdeal_equivOfRingEquiv_symm).

Ideal.IsPrimeTo generalizes the IsGood predicate of TauCetiRoadmap/ArithmeticDirichletSeries/Suggested.lean, where it is stated for the bad primes of an ideal weight on a number field; the design of the predicate — nonzeroness included, so that ⊥ is prime to no set at all — is taken from there, while nothing in it is specific to a number field.

The file also identifies any height-one prime of a discrete valuation ring with its maximal ideal (IsDedekindDomain.HeightOneSpectrum.eq_maximalIdeal), which is what lets a condition stated at the height-one primes of such a ring be read as a condition on its valuation. It was split out of material adapted from Michael Stoll's elliptic-curves formalisation (EllipticCurves/Mathlib/AdicCompletionExtension.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll), where it is the step behind valuation_adicCompletion_algebraMap.

The theorem IsDedekindDomain.HeightOneSpectrum.exists_mem_notMem was split out of material adapted from Michael Stoll's elliptic-curves formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.lean at the roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll); following this repository's convention for adapted material, the upstream authorship is credited here rather than in the copyright header.

IsDedekindDomain.HeightOneSpectrum.comapOfNeBot and its projection are likewise adapted from that formalisation (github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/Basic.lean line 539, at the roadmap's pin 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e, Apache 2.0, by Michael Stoll). The construction is the source's; what changed is the hypothesis — the source and this version take the nonvanishing of the contraction as a hypothesis, where Mathlib's HeightOneSpectrum.comap instead derives it from surjectivity of the map.

Ideal.ne_bot_of_comap_ne_bot plays the role of the source's comap_ne_bot_of_comap_comap_ne_bot (EllipticCurves/Mathlib/Basic.lean line 270): it is what discharges that nonvanishing hypothesis when a prime is contracted through an intermediate ring. It is stated here in the general form — an arbitrary ideal and an injective ring homomorphism, with the map producing the ideal dropped, since it plays no role — and proved from Mathlib's Ideal.comap_bot_of_injective.

theorem Ideal.map_dvd_map_iff_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommSemiring R] [CommSemiring R'] (e : R ≃+* R') (I J : Ideal R) : map e I ∣ map e J ↔ I ∣ J

Divisibility of ideals is unchanged by pushing forward along a ring isomorphism: Ideal.map e and Ideal.map e.symm are mutually inverse homomorphisms of the semirings of ideals.

theorem Ideal.map_pow_dvd_map_iff_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommSemiring R] [CommSemiring R'] (e : R ≃+* R') (p I : Ideal R) (n : ℕ) : map e p ^ n ∣ map e I ↔ p ^ n ∣ I

The prime-power divisibility p ^ n ∣ I is unchanged by pushing forward along a ring isomorphism.

theorem Ideal.count_factors_map_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [IsDedekindDomain R] [CommRing R'] [IsDedekindDomain R'] (e : R ≃+* R') {p I : Ideal R} (hp : Prime p) (hI : I ≠ ⊥) : (Associates.mk (map e p)).count (Associates.mk (map e I)).factors = (Associates.mk p).count (Associates.mk I).factors

Multiplicities in the factorisation of an ideal are unchanged by pushing forward along a ring isomorphism: the number of times Ideal.map e p divides Ideal.map e I is the number of times p divides I.

theorem Ideal.multiplicity_eq_zero_of_isPrime_ne {B : Type u_1} [CommRing B] [IsDedekindDomain B] {P Q : Ideal B} (hP0 : P ≠ ⊥) [P.IsPrime] [Q.IsPrime] (hne : Q ≠ P) : multiplicity Q P = 0

Distinct nonzero primes have zero multiplicity in one another. In a Dedekind domain a nonzero prime is maximal, so Q ∣ P would force Q = P.

This is the coefficient-level form of "a prime power is supported at one prime": in a weighted sum over the primes above a fixed ideal, every term but the matching one vanishes.

theorem Ideal.ne_bot_of_comap_ne_bot {R : Type u_1} {S : Type u_2} {F : Type u_3} [Semiring R] [Semiring S] [FunLike F R S] [RingHomClass F R S] (f : F) (hf : Function.Injective ⇑f) {J : Ideal S} (h : comap f J ≠ ⊥) : J ≠ ⊥

If the contraction of J along an injective ring homomorphism is nonzero, so is J itself.

This is the eliminator that discharges the nonvanishing hypothesis of IsDedekindDomain.HeightOneSpectrum.comapOfNeBot when a prime is contracted through an intermediate ring: contract all the way down to a base where nonvanishing is already known, and read the intermediate step off from that. Only injectivity of the lower map is needed; the map producing J plays no role, so it does not appear.

def IsDedekindDomain.HeightOneSpectrum.comapOfNeBot {B : Type u_1} {C : Type u_2} [CommRing B] [CommRing C] (ψ : B →+* C) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) : HeightOneSpectrum B

The height-one prime of B obtained by contracting a height-one prime of C along a ring homomorphism ψ : B →+* C, given that the contraction is nonzero.

Mathlib's IsDedekindDomain.HeightOneSpectrum.comap is the same construction, but it asks for ψ to be surjective and derives the ne_bot field from that. comapOfNeBot generalises it: the surjective case is recovered by supplying (Ideal.eq_bot_of_comap_eq_bot' hf).mt w.ne_bot, and only the converse fails.

The generality is needed because the maps contracted along here are embeddings into completions — R → v.adicCompletionIntegers K — which are neither surjective, so Mathlib's comap does not apply, nor integral Algebra maps, so HeightOneSpectrum.under does not either. (ℤ → ℤ_p is flat, not integral.) The ne_bot hypothesis has to be supplied by hand.

Adapted from Michael Stoll's EllipticCurves (EllipticCurves/Mathlib/Basic.lean line 539, Apache 2.0, at the roadmap's pin 66889eada51a74c2f5dfb7fb5909b0b5a0a2d96e); the ne_bot-as-hypothesis formulation is the source's.

Equations

• IsDedekindDomain.HeightOneSpectrum.comapOfNeBot ψ w hne = { asIdeal := Ideal.comap ψ w.asIdeal, isPrime := ⋯, ne_bot := hne }

@[simp]

theorem IsDedekindDomain.HeightOneSpectrum.comapOfNeBot_asIdeal {B : Type u_1} {C : Type u_2} [CommRing B] [CommRing C] (ψ : B →+* C) (w : HeightOneSpectrum C) (hne : Ideal.comap ψ w.asIdeal ≠ ⊥) : (comapOfNeBot ψ w hne).asIdeal = Ideal.comap ψ w.asIdeal

The underlying ideal of comapOfNeBot is the contracted ideal.

theorem IsDedekindDomain.HeightOneSpectrum.asIdeal_equivOfRingEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] (e : R ≃+* R') (v : HeightOneSpectrum R) : ((equivOfRingEquiv e) v).asIdeal = Ideal.map e v.asIdeal

Mathlib's transport equivOfRingEquiv e of height one primes along a ring isomorphism e pushes the underlying ideal forward: (equivOfRingEquiv e v).asIdeal = Ideal.map e v.asIdeal.

theorem IsDedekindDomain.HeightOneSpectrum.asIdeal_equivOfRingEquiv_symm {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] (e : R ≃+* R') (w : HeightOneSpectrum R') : ((equivOfRingEquiv e).symm w).asIdeal = Ideal.comap e w.asIdeal

The inverse transport (equivOfRingEquiv e).symm pulls the underlying ideal back along e: ((equivOfRingEquiv e).symm w).asIdeal = Ideal.comap e w.asIdeal.

theorem IsDedekindDomain.HeightOneSpectrum.exists_mem_notMem {R : Type u_1} [CommRing R] [IsDedekindDomain R] {v w : HeightOneSpectrum R} (h : w ≠ v) : ∃ a ∈ v.asIdeal, a ∉ w.asIdeal

Distinct height one primes are incomparable: a height one prime is not contained in any other one, since both are maximal.

def Ideal.IsPrimeTo {R : Type u_1} [CommRing R] (I : Ideal R) (S : Set (IsDedekindDomain.HeightOneSpectrum R)) : Prop

An ideal of a Dedekind domain is prime to a set S of height-one primes when it is nonzero and no prime of S divides it. Nonzeroness is part of the definition, so ⊥ is prime to no set at all — not even to ∅.

Equations

• I.IsPrimeTo S = (I ≠ ⊥ ∧ ∀ 𝔭 ∈ S, ¬𝔭.asIdeal ∣ I)

theorem Ideal.isPrimeTo_iff {R : Type u_1} [CommRing R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} : I.IsPrimeTo S ↔ I ≠ ⊥ ∧ ∀ 𝔭 ∈ S, ¬𝔭.asIdeal ∣ I

theorem Ideal.IsPrimeTo.ne_bot {R : Type u_1} [CommRing R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} (h : I.IsPrimeTo S) : I ≠ ⊥

theorem Ideal.IsPrimeTo.not_dvd {R : Type u_1} [CommRing R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} (h : I.IsPrimeTo S) {𝔭 : IsDedekindDomain.HeightOneSpectrum R} (h𝔭 : 𝔭 ∈ S) : ¬𝔭.asIdeal ∣ I

@[simp]

theorem Ideal.not_isPrimeTo_bot {R : Type u_1} [CommRing R] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} : ¬⊥.IsPrimeTo S

The zero ideal is prime to no set of primes, not even to the empty set.

@[simp]

theorem Ideal.isPrimeTo_empty {R : Type u_1} [CommRing R] {I : Ideal R} : I.IsPrimeTo ∅ ↔ I ≠ ⊥

@[simp]

theorem Ideal.isPrimeTo_top {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} : ⊤.IsPrimeTo S

theorem Ideal.IsPrimeTo.mono {R : Type u_1} [CommRing R] {I : Ideal R} {S T : Set (IsDedekindDomain.HeightOneSpectrum R)} (hST : S ⊆ T) (h : I.IsPrimeTo T) : I.IsPrimeTo S

@[simp]

theorem Ideal.isPrimeTo_insert_iff {R : Type u_1} [CommRing R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {𝔭 : IsDedekindDomain.HeightOneSpectrum R} : I.IsPrimeTo (insert 𝔭 S) ↔ I.IsPrimeTo S ∧ ¬𝔭.asIdeal ∣ I

Enlarging the set of forbidden primes by one. An ideal is prime to insert 𝔭 S exactly when it is prime to S and not divisible by 𝔭.

@[simp]

theorem Ideal.isPrimeTo_mul_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} : (I * J).IsPrimeTo S ↔ I.IsPrimeTo S ∧ J.IsPrimeTo S

Being prime to S is multiplicative. A product of ideals is prime to S exactly when both factors are: neither factor may vanish, and a prime of S divides the product exactly when it divides one of the factors.

@[simp]

theorem Ideal.isPrimeTo_asIdeal_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {𝔭 : IsDedekindDomain.HeightOneSpectrum R} : 𝔭.asIdeal.IsPrimeTo S ↔ 𝔭 ∉ S

A height-one prime ideal is prime to S exactly when its spectrum point is not in S.

theorem Ideal.isPrimeTo_comap_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {A : Type u_2} [CommRing A] [IsDedekindDomain A] (e : R ≃+* A) {I : Ideal A} {T : Set (IsDedekindDomain.HeightOneSpectrum R)} : (comap e I).IsPrimeTo T ↔ I.IsPrimeTo (⇑(IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv e) '' T)

Being prime to a set of primes transports along a ring isomorphism. An ideal pulled back along e : R ≃+* A is prime to T exactly when the ideal itself is prime to the image of T under the induced bijection of height-one spectra.

theorem Ideal.IsPrimeTo.induction_on {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {motive : Ideal R → Prop} (h : I.IsPrimeTo S) (top : motive ⊤) (mul_prime : ∀ (𝔭 : IsDedekindDomain.HeightOneSpectrum R) (J : Ideal R), 𝔭 ∉ S → J.IsPrimeTo S → motive J → motive (𝔭.asIdeal * J)) : motive I

Induction on ideals prime to S. Such an ideal is a finite product of height-one primes outside S, so a property holding at ⊤ and stable under multiplication by a height-one prime outside S holds for all of them.

theorem Ideal.IsPrimeTo.pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} (h : I.IsPrimeTo S) (n : ℕ) : (I ^ n).IsPrimeTo S

Powers of an ideal prime to S are again prime to S.

@[simp]

theorem Ideal.isPrimeTo_pow_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {n : ℕ} (hn : n ≠ 0) : (I ^ n).IsPrimeTo S ↔ I.IsPrimeTo S

A nonzero power of an ideal is prime to S exactly when the ideal is.

@[simp]

theorem Ideal.isPrimeTo_prod_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {ι : Type u_2} {t : Finset ι} {I : ι → Ideal R} : (∏ i ∈ t, I i).IsPrimeTo S ↔ ∀ i ∈ t, (I i).IsPrimeTo S

Being prime to S passes to finite products. A finite product of ideals is prime to S exactly when every factor is; the empty product is ⊤, which is prime to everything.

@[simp]

theorem Ideal.isPrimeTo_univ_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} : I.IsPrimeTo Set.univ ↔ I = ⊤

An ideal divisible by no height-one prime at all is the unit ideal.

theorem Ideal.isPrimeTo_compl_singleton_iff {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {𝔭 : IsDedekindDomain.HeightOneSpectrum R} : I.IsPrimeTo {𝔭}ᶜ ↔ ∃ (n : ℕ), I = 𝔭.asIdeal ^ n

An ideal divisible by no height-one prime other than 𝔭 is a power of 𝔭.

theorem Ideal.IsPrimeTo.isRelPrime {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I J : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} (hI : I.IsPrimeTo S) (hJ : J.IsPrimeTo Sᶜ) : IsRelPrime I J

Ideals supported on complementary sets of primes are relatively prime.

theorem Ideal.exists_eq_prod_pow {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} (hI : I ≠ ⊥) : ∃ (S : Finset (IsDedekindDomain.HeightOneSpectrum R)) (e : IsDedekindDomain.HeightOneSpectrum R → ℕ), I = ∏ 𝔭 ∈ S, 𝔭.asIdeal ^ e 𝔭

Every nonzero ideal is a finite product of prime powers. This produces the prime-power factorizations consumed by multiplicativity statements such as TauCeti.IdealArithmeticFunction.IsMultiplicative.map_prod_pow.

theorem Ideal.IsPrimeTo.exists_eq_pow_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] {I : Ideal R} {S : Set (IsDedekindDomain.HeightOneSpectrum R)} {𝔭 : IsDedekindDomain.HeightOneSpectrum R} (h : I.IsPrimeTo (insert 𝔭 S)ᶜ) : ∃ (n : ℕ) (J : Ideal R), J.IsPrimeTo Sᶜ ∧ I = 𝔭.asIdeal ^ n * J

Splitting off one allowed prime. An ideal all of whose prime factors lie in insert 𝔭 S is a power of 𝔭 times an ideal all of whose prime factors lie in S.

theorem Ideal.eq_and_eq_of_pow_mul_eq_pow_mul {R : Type u_1} [CommRing R] [IsDedekindDomain R] {p : Ideal R} (hp : p ≠ ⊥) {m n : ℕ} {I J : Ideal R} (hI : ¬p ∣ I) (hJ : ¬p ∣ J) (h : p ^ m * I = p ^ n * J) : m = n ∧ I = J

Uniqueness of the splitting. The exponent and the prime-to-p cofactor of a nonzero ideal are determined by it. Only nonzeroness of p is used, not primality.

theorem IsDedekindDomain.HeightOneSpectrum.eq_maximalIdeal {A : Type u_1} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A] (P : HeightOneSpectrum A) : P = IsDiscreteValuationRing.maximalIdeal A

The maximal ideal is the only height-one prime of a discrete valuation ring.

Mathlib has IsDiscreteValuationRing.maximalIdeal as a HeightOneSpectrum and IsLocalRing.eq_maximalIdeal for ideals, but not that the two agree at the level of HeightOneSpectrum. That identification is what lets a statement about the height-one primes of a discrete valuation ring be read as a statement about its valuation.