English
The localization to stalk along a prime is the germ of the structure sheaf at the corresponding basic open.
Русский
Локализация в stalk вдоль простого идеала равняется гемеру структуры оболочки над соответствующим базовым открытием.
LaTeX
$$$ localizationToStalk\\ R x (IsLocalization.mk' (Localization.AtPrime x.asIdeal) f s) = (structureSheaf R).presheaf.germ (PrimeSpectrum.basicOpen (s : R)) x s.2 (const R f s (PrimeSpectrum.basicOpen s) fun _ => id)$$$
Lean4
/-- For an algebra `f : R →+* S`, this is the ring homomorphism `S →+* (f∗ 𝒪ₛ)ₚ` for a `p : Spec R`.
This is shown to be the localization at `p` in `isLocalizedModule_toPushforwardStalkAlgHom`.
-/
def toPushforwardStalk : S ⟶ (Spec.topMap f _* (structureSheaf S).1).stalk p :=
StructureSheaf.toOpen S ⊤ ≫ @TopCat.Presheaf.germ _ _ _ _ (Spec.topMap f _* (structureSheaf S).1) ⊤ p trivial
