Lean4
/-- The isomorphism of `R`-modules from the stalk of `M^~` at `x` to the localization of `M` at the
prime ideal corresponding to `x`.
-/
@[simps]
noncomputable def stalkIso (x : PrimeSpectrum.Top R) :
TopCat.Presheaf.stalk (tildeInModuleCat M) x ≅ ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)
where
hom := stalkToFiberLinearMap M x
inv := localizationToStalk M x
hom_inv_id :=
TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦
ModuleCat.hom_ext <|
LinearMap.ext fun s ↦
by
change
localizationToStalk M x (stalkToFiberLinearMap M x (M.tildeInModuleCat.germ U x hxU s)) =
M.tildeInModuleCat.germ U x hxU s
rw [stalkToFiberLinearMap_germ]
obtain ⟨V, hxV, iVU, f, g, (hg : V ≤ PrimeSpectrum.basicOpen _), hs⟩ := exists_const _ _ s x hxU
have := res_apply M U V iVU s ⟨x, hxV⟩
dsimp only [isLocallyFraction_pred, Opens.val_apply, LocalizedModule.mkLinearMap_apply,
Opens.apply_mk] at this
rw [← this, ← hs, const_apply, localizationToStalk_mk]
exact (tildeInModuleCat M).germ_ext V hxV (homOfLE hg) iVU <| hs ▸ rfl
inv_hom_id := by ext x;
exact
x.induction_on
(fun _ _ =>
by
simp only [hom_comp, LinearMap.coe_comp, Function.comp_apply, hom_id, LinearMap.id_coe, id_eq]
rw [localizationToStalk_mk, stalkToFiberLinearMap_germ]
simp)
