English
There is a canonical isomorphism between the projective spectrum restricted to a basic open D(f) and the affine scheme Spec of A⁰_f.
Русский
Существует канонический изоморфизм между ограниченным проективным спектром на D(f) и аффинным спектром Spec(A⁰_f).
LaTeX
$$$$(\mathrm{Proj}\;|\;pbo\;f) \cong \mathrm{Spec}(A⁰_f)$$$$
Lean4
/-- If `f ∈ A` is a homogeneous element of positive degree, then the projective spectrum restricted to
`D(f)` as a locally ringed space is isomorphic to `Spec A⁰_f`.
-/
def projIsoSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (Proj| pbo f) ≅ (Spec (A⁰_ f)) :=
@asIso _ _ _ _ (f := toSpec 𝒜 f) (isIso_toSpec 𝒜 f f_deg hm)