Fiber at prime ideal

Stream: Is there code for X?

[Wang Jingting]

Do we have something like the following lemma?

def PrimeSpectrum.preimageOrderIsoTensorResidueField (R S : Type*) [CommRing R]
    [CommRing S] [Algebra R S] (p : PrimeSpectrum R) :
    (algebraMap R S).specComap ⁻¹' {p} ≃o
      PrimeSpectrum (TensorProduct R p.asIdeal.ResidueField S) := sorry

I'm working on a proof_wanted on the upper bound on the Krull dimension of the polynomial ring, and this is the last sorry I'm stuck on.

Edit: This lemma corresponds to the mathematical fact that, if we have a ring homomorphism $f : A \rightarrow B$, let $f^* : Spec B \rightarrow Spec A$ be the corresponding map between the prime spectrums, then for a prime ideal $\mathfrak{p} \in Spec A$, we can identify $f^{*-1} \mathfrak{p}$ with $Spec (B \otimes_A \kappa ( \mathfrak{p}) )$.

[Andrew Yang]

We only have the global (scheme) version. But If you only need an order iso this shouldn't be hard.
The map on the inverse direction is just TensorProduct.inclusionRight.specComap, and to show this is bijective you show that $B_p$ surjects onto $B \otimes_A \kappa(p)$ and use the description of primes in localization.

[Wang Jingting]

Thanks! I'll look into this and try to add this version.