English
There is a natural isomorphism between the stalk of the structure sheaf at x and the corresponding homogeneous localization at x, with explicit identifications on stalks and localizations.
Русский
Существует естественное изоморождение между стоком структуры пучка в точке x и соответствующей однородной локализацией в x, с явными идентификациями на стоках и локализациях.
LaTeX
$$$(\mathrm{stalk\,Iso}'_{\mathcal{A}})(x): (\mathcal{P}\!\mathrm{r}({\mathcal{A}}).\mathrm{presheaf}.\mathrm{stalk} x \cong \mathrm{AtPrime}_{\mathcal{A}} x$$$
Lean4
/-- Given any point `x` and `f` in the homogeneous localization at `x`, there is an element in the
stalk at `x` obtained by `sectionInBasicOpen`. This is the inverse of `stalkToFiberRingHom`.
-/
def homogeneousLocalizationToStalk (x : ProjectiveSpectrum.top 𝒜) (y : at x) :
(Proj.structureSheaf 𝒜).presheaf.stalk x :=
Quotient.liftOn' y
(fun f => (Proj.structureSheaf 𝒜).presheaf.germ _ x (mem_basicOpen_den _ x f) (sectionInBasicOpen _ x f))
fun f g (e : f.embedding = g.embedding) ↦
by
simp only [HomogeneousLocalization.NumDenSameDeg.embedding, Localization.mk_eq_mk', IsLocalization.mk'_eq_iff_eq,
IsLocalization.eq_iff_exists x.asHomogeneousIdeal.toIdeal.primeCompl] at e
obtain ⟨⟨c, hc⟩, hc'⟩ := e
apply
(Proj.structureSheaf 𝒜).presheaf.germ_ext
(ProjectiveSpectrum.basicOpen 𝒜 f.den.1 ⊓ ProjectiveSpectrum.basicOpen 𝒜 g.den.1 ⊓
ProjectiveSpectrum.basicOpen 𝒜 c)
⟨⟨mem_basicOpen_den _ x f, mem_basicOpen_den _ x g⟩, hc⟩ (homOfLE inf_le_left ≫ homOfLE inf_le_left)
(homOfLE inf_le_left ≫ homOfLE inf_le_right)
apply Subtype.ext
ext ⟨t, ⟨htf, htg⟩, ht'⟩
rw [Proj.res_apply, Proj.res_apply]
simp only [sectionInBasicOpen, HomogeneousLocalization.val_mk, Localization.mk_eq_mk', IsLocalization.mk'_eq_iff_eq]
apply
(IsLocalization.map_units (M := t.asHomogeneousIdeal.toIdeal.primeCompl)
(Localization t.asHomogeneousIdeal.toIdeal.primeCompl) ⟨c, ht'⟩).mul_left_cancel
rw [← map_mul, ← map_mul, hc']
