Commit 2024-06-11 06:47 5618bfde

feat(AlgebraicGeometry/ProjectiveSpectrum/Scheme): morphism of locally ringed space $\mathrm{Proj}|_{D(f)} -> \mathrm{Spec} A^0_f$ (#13689) We construct a morphism of locally ringed spaces α : Proj| (pbo f) ⟶ Spec.T A⁰_f as the following: by the Gamma-Spec adjunction, it is sufficient to construct a ring map A⁰_f → Γ(Proj, pbo f) from the ring of homogeneous localization of A away from f to the local sections of structure sheaf of projective spectrum on the basic open set around f. The map A⁰_f → Γ(Proj, pbo f) is constructed in awayToΓ and is defined by sending s ∈ A⁰_f to the section x ↦ s on pbo f.