The fiber of a ring homomorphism at a prime ideal

Main results

• PrimeSpectrum.preimageOrderIsoTensorResidueField : We show that there is an OrderIso between fiber of a ring homomorphism algebraMap R S : R →+* S at a prime ideal p : PrimeSpectrum R and the prime spectrum of the tensor product of S and the residue field of p.

noncomputable def PrimeSpectrum.preimageOrderIsoTensorResidueField (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : ↑((algebraMap R S).specComap ⁻¹' {p}) ≃o PrimeSpectrum (TensorProduct R p.asIdeal.ResidueField S)

The OrderIso between fiber of a ring homomorphism algebraMap R S : R →+* S at a prime ideal p : PrimeSpectrum R and the prime spectrum of the tensor product of S and the residue field of p.

Equations

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