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