Lean4
/-- The ring isomorphism between the stalk of the structure sheaf of `R` at a point `p`
corresponding to a prime ideal in `R` and the localization of `R` at `p`. -/
@[simps]
def stalkIso (x : PrimeSpectrum.Top R) :
(structureSheaf R).presheaf.stalk x ≅ CommRingCat.of (Localization.AtPrime x.asIdeal)
where
hom := stalkToFiberRingHom R x
inv := localizationToStalk R x
hom_inv_id := by
apply stalk_hom_ext
intro U hxU
ext s
dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply, CommRingCat.hom_id, RingHom.coe_id, id_eq]
rw [stalkToFiberRingHom_germ]
obtain ⟨V, hxV, iVU, f, g, (hg : V ≤ PrimeSpectrum.basicOpen _), hs⟩ := exists_const _ _ s x hxU
have := res_apply R U V iVU s ⟨x, hxV⟩
dsimp only [isLocallyFraction_pred, Opens.apply_mk] at this
rw [← this, ← hs, const_apply, localizationToStalk_mk']
refine (structureSheaf R).presheaf.germ_ext V hxV (homOfLE hg) iVU ?_
rw [← hs, res_const']
inv_hom_id :=
CommRingCat.hom_ext <|
IsLocalization.ringHom_ext x.asIdeal.primeCompl <| by
ext f
rw [CommRingCat.hom_comp, CommRingCat.hom_id, RingHom.comp_apply, RingHom.comp_apply, localizationToStalk_of,
stalkToFiberRingHom_toStalk, RingHom.comp_apply, RingHom.id_apply]
