English
Let 𝒜 be a graded algebra over a ring with a homogeneous element f, and let x be a point of the basic open in Proj corresponding to f. Then the base map of the morphism to Spec of the homogeneous localization A⁰_f is exactly the natural comorphism from the primes along the map mapId 𝒜 to the closed point coming from the corresponding prime. In other words, the underlying map on prime spectra is obtained by pulling back along the canonical ring map and evaluating at the closed prime corresponding to x.
Русский
Пусть 𝒜 — градуированная алгебра над кольцом и f — однородный элемент; пусть x — точка на открытом множействе Proj, соответствующая f. Тогда базовое отображение морфизма к Spec для локализации A⁰_f совпадает с естественным сопряжением нулевых идеалов: множество простых идеалов протягивается вдоль естественного отображения колец и достигается над соответствующим нулевым элементом, соответствующим x. Иными словами, отображение на спектре простых задаётся через сопоставление простых идеалов через соответствующее отображение колец.
LaTeX
$$$$(toSpec\;\mathcal{A}f).base\;x = \operatorname{PrimeSpectrum.comap}\bigl(\operatorname{mapId}_\mathcal{A}\bigl(\operatorname{Submonoid.powers\_le.mpr}\;x.2\bigr)\bigr)\bigl(\operatorname{closedPoint}(\operatorname{AtPrime} \mathcal{A} x.1.asHomogeneousIdeal.toIdeal)\bigr).$$$$
Lean4
theorem toSpec_base_apply_eq_comap {f} (x : Proj| pbo f) :
(toSpec 𝒜 f).base x =
PrimeSpectrum.comap (mapId 𝒜 (Submonoid.powers_le.mpr x.2))
(closedPoint (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)) :=
by
change
PrimeSpectrum.comap (awayToΓ 𝒜 f ≫ (Proj| pbo f).presheaf.Γgerm x).hom
(IsLocalRing.closedPoint ((Proj| pbo f).presheaf.stalk x)) =
_
rw [awayToΓ_ΓToStalk, CommRingCat.hom_comp, PrimeSpectrum.comap_comp]
exact
congr(PrimeSpectrum.comap _
$(@IsLocalRing.comap_closedPoint (HomogeneousLocalization.AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) _ _
((Proj| pbo f).presheaf.stalk x) _ _ _ (isLocalHom_of_isIso _)))
