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 and that the residual degree and ramification index are preserved by this bijection.
Main definitions and results #
IsLocalization.AtPrime.mem_primesOver_of_isPrime: The nonzero prime ideals ofSₚare primes over the maximal ideal ofRₚ.IsLocalization.AtPrime.equivQuotientMapOfIsMaximal:S ⧸ P ≃+* Sₚ ⧸ P·SₚwherePis a maximal ideal ofSabovep.IsDedekindDomain.primesOverEquivPrimesOver: the bijection between the primes overpinSand the primes over the maximal ideal ofRₚinSₚ.IsDedekindDomain.primesOverEquivPrimesOver_inertiagDeg_eq: the bijectionprimesOverEquivPrimesOverpreserves the inertia degree.IsDedekindDomain.primesOverEquivPrimesOver_ramificationIdx_eq: the bijectionprimesOverEquivPrimesOverpreserves the ramification index.
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.
The isomorphism S ⧸ P ≃+* Sₚ ⧸ P·Sₚ, where Sₚ is the localization of S at the (image) of
the complement of p and P is a maximal ideal of S above p.
Note that this isomorphism makes the obvious diagram involving R ⧸ p ≃+* Rₚ ⧸ maximalIdeal Rₚ
commute, see IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply.
Equations
Instances For
The following diagram where the vertical maps are the algebra maps and the horizontal maps are
Localization.AtPrime.equivQuotMaximalIdeal.symm and
Localization.AtPrime.equivQuotientMapOfIsMaximal.symm commutes:
Rₚ ⧸ 𝓂 ──▶ R ⧸ p
│ │
Sₚ ⧸ 𝒫 ──▶ S ⧸ P
Here, 𝓂 denotes the maximal ideal of Rₚ and 𝒫 the image of P in Sₚ.
Note that result is stated in that direction since this is the formulation needed for the proof
of Localization.AtPrime.inertiaDeg_map_eq_inertiaDeg.
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.