Primes in an extension of localization at prime

Let R ⊆ S be an extension of Dedekind domains and p be a prime ideal of R. Let Rₚ be the localization of R at the complement of p and Sₚ the localization of S at the (image) of the complement of p.

In this file, we study the relation between the (nonzero) prime ideals of Sₚ and the prime ideals of S above p. In particular, we prove that (under suitable conditions) they are in bijection.

Main definitions and results

• IsLocalization.AtPrime.mem_primesOver_of_isPrime: The nonzero prime ideals of Sₚ are primes over the maximal ideal of Rₚ.

• IsDedekindDomain.primesOverEquivPrimesOver: the order-preserving bijection between the primes over p in S and the primes over the maximal ideal of Rₚ in Sₚ.

theorem IsLocalization.AtPrime.mem_primesOver_of_isPrime (Rₚ : Type u_3) [CommRing Rₚ] [IsLocalRing Rₚ] (Sₚ : Type u_4) [CommRing Sₚ] [Algebra Rₚ Sₚ] {Q : Ideal Sₚ} [Q.IsMaximal] [Algebra.IsIntegral Rₚ Sₚ] : Q ∈ (IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ

The nonzero prime ideals of Sₚ are prime ideals over the maximal ideal of Rₚ. See Localization.AtPrime.primesOverEquivPrimesOver for the bijection between the prime ideals of Sₚ over the maximal ideal of Rₚ and the primes ideals of S above p.

theorem IsLocalization.AtPrime.liesOver_comap_of_liesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] {T : Type u_5} [CommRing T] [Algebra R T] [Algebra Rₚ T] [Algebra S T] [IsScalarTower R S T] [IsScalarTower R Rₚ T] (Q : Ideal T) [Q.LiesOver (IsLocalRing.maximalIdeal Rₚ)] : (Ideal.comap (algebraMap S T) Q).LiesOver p

theorem IsLocalization.AtPrime.liesOver_map_of_liesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type u_4) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra Rₚ Sₚ] (P : Ideal S) [hPp : P.LiesOver p] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [P.IsPrime] : (Ideal.map (algebraMap S Sₚ) P).LiesOver (IsLocalRing.maximalIdeal Rₚ)

noncomputable def IsDedekindDomain.primesOverEquivPrimesOver {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type u_4) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra Rₚ Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hp : p ≠ ⊥) : ↑(p.primesOver S) ≃o ↑((IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ)

For R ⊆ S an extension of Dedekind domains and p a prime ideal of R, the bijection between the primes of S over p and the primes over the maximal ideal of Rₚ in Sₚ where Rₚ and Sₚ are resp. the localizations of R and S at the complement of p.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem IsDedekindDomain.primesOverEquivPrimesOver_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type u_4) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra Rₚ Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hp : p ≠ ⊥) (P : ↑(p.primesOver S)) : ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp) P) = Ideal.map (algebraMap S Sₚ) ↑P

@[simp]

theorem IsDedekindDomain.primesOverEquivPrimesOver_symm_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_3) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsLocalRing Rₚ] (Sₚ : Type u_4) [CommRing Sₚ] [Algebra S Sₚ] [IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] [Algebra Rₚ Sₚ] [Algebra R Sₚ] [IsScalarTower R S Sₚ] [IsScalarTower R Rₚ Sₚ] [IsDedekindDomain S] [NoZeroSMulDivisors R S] (hp : p ≠ ⊥) (Q : ↑((IsLocalRing.maximalIdeal Rₚ).primesOver Sₚ)) : ↑((primesOverEquivPrimesOver p Rₚ Sₚ hp).symm Q) = Ideal.comap (algebraMap S Sₚ) ↑Q