English
The isomorphism specced by specStalkEquiv fits into the global equivalence of stalks and localizations, verifying the compatibility of several functorial identifications.
Русский
Изоморфизм, задаваемый specStalkEquiv, встроен в общую эквиваленцию stalks и локализаций, обеспечивая совместимость нескольких обращенияфункторов.
LaTeX
$$$$\text{compatibility of stalks under specStalkEquiv and localization}$$$$
Lean4
theorem toStalk_specStalkEquiv (f) (x : pbo f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) :
StructureSheaf.toStalk (A⁰_ f) ((toSpec 𝒜 f).base x) ≫ (specStalkEquiv 𝒜 f x f_deg hm).hom =
CommRingCat.ofHom (mapId _ <| Submonoid.powers_le.mpr x.2) :=
letI : Algebra (Away 𝒜 f) (AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal) :=
(mapId 𝒜 (Submonoid.powers_le.mpr x.2)).toAlgebra
letI := isLocalization_atPrime 𝒜 f x f_deg hm
CommRingCat.hom_ext
(IsLocalization.algEquiv (R := A⁰_ f) (M := ((toSpec 𝒜 f).base x).asIdeal.primeCompl) (S :=
(«Spec».structureSheaf (A⁰_ f)).presheaf.stalk ((toSpec 𝒜 f).base x)) (Q :=
AtPrime 𝒜 x.1.asHomogeneousIdeal.toIdeal)).toAlgHom.comp_algebraMap
