theorem PrimeSpectrum.preimage_eq_range_tensor_residueField (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (p : PrimeSpectrum R) : (algebraMap R S).specComap ⁻¹' {p} = Set.range (algebraMap S (TensorProduct R S p.asIdeal.ResidueField)).specComap