English
There is a canonical ring hom from the stalk of the pushforward of the structure sheaf to the stalk at p, obtained by germ maps along the basic open.
Русский
Каноническое кольцевое отображение из локализации pushforward структуры оболочки к локализации в точке p, образованное геммером над базовым открытием.
LaTeX
$$$ toPushforwardStalk \\ f\\ p = StructureSheaf.toOpen S \\top ∘ Presheaf.germ (Spec.topMap f _* (structureSheaf S).1) \\top p \\ (trivial)$$$
Lean4
@[simp]
theorem localizationToStalk_mk' (x : PrimeSpectrum.Top R) (f : R) (s : x.asIdeal.primeCompl) :
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) :=
(IsLocalization.lift_mk'_spec (S := Localization.AtPrime x.asIdeal) _ _ _ _).2 <| by
rw [← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2, ← germ_toOpen R (PrimeSpectrum.basicOpen s) x s.2, ←
RingHom.map_mul, toOpen_eq_const, toOpen_eq_const, const_mul_cancel']
