Commit 2025-11-12 12:36 08d91a20

feat(RingTheory/Localization/AtPrime): bijection between prime ideals (#29322) Let R ⊆ S be an extension of rings and p be a prime ideal of R. Denote by Rₚ the localization of R at the complement of p and by Sₚ the localization of S at the (image) of the complement of p. In this PR, we study the extension Rₚ ⊆ Sₚ and 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. In a following PR #27706, we prove that the residual degree and ramification index are preserved by this bijection. Note. The new file RingTheory.Localization.AtPrime.Extension is imported in RingTheory.Trace.Quotient because one function from the latter was moved to the former, but the plan is eventually to move the isomorphisms proved in RingTheory.Trace.Quotient to RingTheory.Localization.AtPrime.Basic and RingTheory.Localization.AtPrime.Extension where they belong. This will be done in #27706.