Proj as a Scheme¶
Scheme¶
Scheme is a locally ringed space $X$ that is locally affine, i.e. for any $x\in X$, there is an open neighourhood $x\in U$, such that $X|_U \cong \mathrm{Spec} R$ for some commutative ring $R$
structure Scheme extends to_LocallyRingedSpace : LocallyRingedSpace :=
(local_affine : ∀ x : to_LocallyRingedSpace,
∃ (U : open_nhds x) (R : CommRing), nonempty
(to_LocallyRingedSpace.restrict U.open_embedding ≅
Spec.to_LocallyRingedSpace.obj (op R)))
Locally ringed space¶
A locally ringed space is a sheafed space $X$ such that for any $x\in X$, the stalk at $x$ is a local ring.
structure LocallyRingedSpace extends SheafedSpace CommRing :=
(local_ring : ∀ x, local_ring (presheaf.stalk x))
Sheafed space¶
A sheafed space is a presheafed space whose structure presheaf is a sheaf.
structure SheafedSpace extends PresheafedSpace C :=
(is_sheaf : presheaf.is_sheaf)
Presheafed space¶
A presheafed space is a topological space $X$ with a structure presheaf on it.
structure PresheafedSpace :=
(carrier : Top)
(presheaf : carrier.presheaf C)
Given a $\mathbb N$-graded ring, we need a
a topology
a sheaf
a proof that stalks are local ring
an affine cover
Topology¶
Given an $\mathbb N$-graded ring $A$, define its projective spectrum as $$ \left\{I : \text{homogeneous prime ideal of } A\left| \bigoplus_{1\le i}A_i\not\subseteq I\right.\right\} $$
Then given any set $S\subseteq A$, the zero locus of $s$, $Z(s)$ is defined as $$ \left\{x : \mathrm{Proj}| s\subseteq x\right\} $$
Then
- $Z(\emptyset)=\mathrm{Proj}$ and $Z(A)=\emptyset$
- $Z(s)\cup Z(s') = Z(s\cap s')$
- $\bigcap_{i} Z(s_i)= Z\left(\bigcup_{i}s_i\right)$
Hence, by taking all the zero loci to be closed sets, we get a topology on $\mathrm{Proj}$. This is the Zariski topology.
For any $a\in A$, define basic open set $D(a)$ as the complement of $Z(\{a\})$. All the basic open sets form a basis for the Zariski topology.
To prove this, we need to show that for any open set $O=Z(s)$ and $p\in O$, there is some basic open set $p\in D(a)\subseteq O$. Since $p\not\in Z(s)$, $s\not\subseteq p$, so some $a$ is in $s$ but not in $p$. Then $p\in D(a)$. $D(a)\subseteq O$ if and only if $Z(s)\subseteq Z({a})$
Structure sheaf¶
Homogeneous localization¶
For a prime ideal $\mathfrak p$, the homogeneous localization of $A_{(\mathfrak p)}$ is the subring $$ \left\{\frac a b\in A_{(\mathfrak p)}\left|\text{$a, b\in A_n$ for some $n\in\mathbb N$}\right.\right\}. $$ We denote the homogeneously localized ring as $A^0_{(\mathfrak p)}$ Homogeneously localized rings are local.
Implementation 1¶
def homogeneous_localization : subring (localization.at_prime 𝔭) :=
{ carrier := {x | ∃ (n : ι) (a b : 𝒜 n) (b_not_mem : b.1 ∉ 𝔭),
x = localization.mk a.1 ⟨b.1, b_not_mem⟩},
mul_mem' := _,
one_mem' := _,
add_mem' := _,
zero_mem' := _,
neg_mem' := _ }
Implementation 2¶
Using quotient
structure num_denom_same_deg :=
(deg : ι)
(num denom : 𝒜 deg)
(denom_not_mem : (denom : A) ∉ 𝔭)
def emb (p : num_denom_same_deg 𝒜 𝔭) : localization.at_prime 𝔭 :=
localization.mk p.num ⟨p.denom, p.denom_not_mem⟩
def homogeneous_localization : Type* :=
quotient (setoid.ker $ emb 𝒜 𝔭)
Structure sheaf¶
For an open set $U\subseteq\mathrm{Proj}$, take the sections on $U$ as subring of dependent functions $\prod_{x\in U}A^0_{(x)}$ that are locally fractions, i.e. $$ \left\{s\left|\text{for all $x\in U$, there are some $a, b$ of same degree and $b\not\in x$, such that $s(x)$ locally is $\frac a b$}\right.\right\} $$ and restriction map as restriction of function.
This is indeed a ring because:
- $0=\frac01$
- $1=\frac11$
if $s(x)=\frac a b$ on $V$ and $t(x)=\frac c d$ on $W$
- $(s+t)(x)=\frac{ad+bc}{bd}$ on $V\cap W$
- $(s\cdot t)(x)=\frac{ac}{bd}$
- $(-s)(x)=\frac{-a}{b}$
Implementation¶
- Prelocal predicate
variables {X : Top.{v}}
variables (T : X → Type v)
structure prelocal_predicate :=
(pred : Π {U : opens X}, (Π x : U, T x) → Prop)
(res : ∀ {U V : opens X} (i : U ⟶ V) (f : Π x : V, T x)
(h : pred f), pred (λ x : U, f (i x)))
- Local predicate
structure local_predicate extends prelocal_predicate T :=
(locality : ∀ {U : opens X} (f : Π x : U, T x)
(w : ∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U),
pred (λ x : V, f (i x : U))), pred f)
- Sheafify
def prelocal_predicate.sheafify
{T : X → Type v}
(P : prelocal_predicate T) : local_predicate T :=
{ pred := λ U f,
∀ x : U, ∃ (V : opens X) (m : x.1 ∈ V) (i : V ⟶ U),
P.pred (λ x : V, f (i x : U)),
res := _,
locality := _}
- In our case, we take
Tto be $\mathfrak p\to A^0_{(\mathfrak p)}$ and
def is_fraction
{U : opens (projective_spectrum.Top 𝒜)}
(f : Π x : U, at x.1) : Prop :=
∃ (i : ℕ) (r s : 𝒜 i),
∀ x : U, ∃ (s_nin : s.1 ∉ x.1.as_homogeneous_ideal),
(f x) = quotient.mk' ⟨i, r, s, s_nin⟩
def is_fraction_prelocal :
prelocal_predicate (λ (x : projective_spectrum.Top 𝒜), at x) :=
{ pred := λ U f, is_fraction f,
res := _ }
def is_locally_fraction :
local_predicate (λ (x : projective_spectrum.Top 𝒜), at x) :=
(is_fraction_prelocal 𝒜).sheafify
Then we can use subsheaf_to_Types which states the presheaf of $U\mapsto \{\prod_{x\in U} T x\}$ satisfying $P$ is a sheaf of sets.
def subsheaf_to_Types (P : local_predicate T) : sheaf (Type v) X := _
Then we can use the fact that a presheaf of rings is a sheaf if and only if the underlying presheaf of sets is sheaf.
variables (G : C ⥤ D)
variables [reflects_isomorphisms G]
variables [has_limits C] [has_limits D] [preserves_limits G]
variables {X : Top.{v}} (F : presheaf C X)
lemma is_sheaf_iff_is_sheaf_comp :
presheaf.is_sheaf F ↔ presheaf.is_sheaf (F ⋙ G) := _
$\mathrm{Proj}$ as a locally ringed space¶
We will prove that $\mathcal{O}_{\mathrm{Proj}, \mathfrak p}\cong A^0_{(\mathfrak p)}$ by constructing a bijective ring homomorphism. Then we are finished since $A^0_{(\mathfrak p)}$ is always a local ring.
- $\mathcal{O}_{\mathrm{Proj}, \mathfrak p}\to A^0_{(\mathfrak p)}$ is given by $$ \langle U, f\rangle\mapsto \frac a b $$ where $f(\mathfrak p)=\frac a b$ on some open neighbourhood of $\mathfrak p$. This is formally implemented using universal property of colimit by descending $f\in\mathcal{O}(U)\mapsto f(\mathfrak p)\in A^0_{(\mathfrak p)}$, hence is ring homomorphism by category theory.
- $A^0_{(\mathfrak p)}\to \mathcal{O}_{\mathrm{Proj}, \mathfrak p}$ is given by $$ \frac a b \mapsto \left\langle D(b), x\mapsto \frac a b \right\rangle $$
We don't need to prove the latter is a ring homomorphism, all we need is that the latter function is the right inverse of the former one.
An affine cover¶
$\mathrm{Proj}$ can be covered by basic open sets $D(f)$ for $f\in A_m$ with $0 < m$.
Let $\mathfrak p\in\mathrm{Proj}$, then $\bigoplus_{1\le i}A_i\not\subseteq\mathfrak p$, then for some $f\in\bigoplus_{1\le i}A_i$, $f\not\in \mathfrak p$.
Write $f=f_1+f_2+\cdots$ where $f_i\in A_i$, then for some $0<m$, $f_m\not\in\mathfrak p$. Then $\mathfrak p\in D(f_m)$.
We need $m$ to be strictly positive, because we will be using $m=(m-1)+1$ a lot.
So we will prove that for $f$ with positive degree $m$, $\mathrm{Proj}\mid_{D(f)}\cong\mathrm{Spec} A^0_f$ where $A^0_f$ is the subring of degree zero elements in the localized ring $A_f$, i.e. $$ A^0_f:=\left\{\frac a{f^i} \left| a\in A_{mi}\right.\right\} $$
To prove that these are isomorphic as locally ringed space, we need :
- a homeomorphism $h : \mathrm{Proj}\mid_{D(f)}\cong\mathrm{Spec} A^0_f$ and
- an isomorphism of sheaf $h_*\mathcal O_{\mathrm{Proj}\mid_{D(f)}}\cong \mathcal O_{\mathrm{Spec}A^0_f}$
In the following, we will fix an $f\in A_m$ with $0 < m$.
$\mathrm{Proj}\mid_{D(f)}\to\mathrm{Spec} A^0_f$¶
Given an $\mathfrak p\in \mathrm{Proj}\mid_{D(f)}$, i.e. a relevant homogeneous prime ideal in $A$, we need a point in $\mathrm{Spec}A^0_f$, i.e. a prime ideal.
So let's define $$ h(\mathfrak p):=\mathrm{span}\left\{\frac g1|g \in \mathfrak p\right\}\cap A^0_f=\mathrm{span}\left\{\frac g{f^i}|g\in \mathfrak p\cap A_{mi}\right\} $$
Then we need to check:
- $h(\mathfrak p)$ is prime:
- $h(\mathfrak p)\ne A^0_f$;
- if $x_1 x_2\in h(\mathfrak p)$, then either $x_1\in h(\mathfrak p)$ or $x_2 \in h(\mathfrak p)$;
- $h$ is continuous with respect to Zariski topology.
$h(\mathfrak p)\ne A^0_f$¶
If $h(\mathfrak p)= A^0_f$, then $1\in\mathrm{span}\left\{\frac g1|g \in \mathfrak p\right\}$. So write $$ 1 = \sum_i\frac{a_i}{f^{n_i}}\frac {g_i}1. $$
By multiplying a suitable power of $f$, we get $$ \frac{f^N} 1 = \frac{\sum_i a_i g_i f^{k_i}}1 $$
So $f^M f^N=f^M \sum_i a_i g_i f^{k_i}$, since the right handside is in $\mathfrak p$, the left handside is in $\mathfrak p$ too. Contradiction.
if $x_1 x_2\in h(\mathfrak p)$, then either $x_1\in h(\mathfrak p)$ or $x_2 \in h(\mathfrak p)$¶
Write $x_1=\frac{a_1}{f^{n_1}}$ and $x_2=\frac{a_2}{f^{n_2}}$, then $\frac{a_1a_2}{f^{n_1+n_2}}\in\mathrm{span}\left\{\frac g1|g \in \mathfrak p\right\}$, so write $$ \frac{a_1a_2}{f^{n_1+n_2}}=\sum_i \frac{c_i}{f^{n_i}}\frac{g_i}1. $$
By multiplying a suitable power of $f$, we get $$ \frac{a_1a_2f^N}1=\frac{\sum_i c_ig_if^{k_i}}1. $$
So $a_1a_2f^N f^M=f^M\sum_i c_ig_if^{k_i}$, since right handside is in $\mathfrak p$ and $f\not\in\mathfrak p$, either $a_1\in\mathfrak p$ or $a_2\in\mathfrak p$.
continuity¶
Since $\mathrm{Spec}A^0_f$ also has a topological basis of basic open set, we only need to consider preimage of basic open sets. Take $\frac{a}{f^n}$, then $h^{-1}\left(D\left(\frac a{f^n}\right)\right)=D(f)\cap D(a)$.
$D(f)\cap D(a)\subseteq h^{-1}\left(D\left(\frac a{f^n}\right)\right)$ because if $y\in D(f)\cap D(a)$ and $\frac a{f^n}\in h(y)$, then $$ \frac a{f^n}=\sum_i \frac{c_i}{f^{n_i}}\frac{g_i}1 $$
Then by multiplying suitable powers of $f$, $$ \frac{a f^N}1=\frac{\sum_i c_ig_if^{m_i}}1 $$ then this implies $a\in y$, contradiction.
If $h(y)\in D\left(\frac a{f^n}\right)$ and $a\in y$, then $\frac a 1\in h(y)$, contradiction because $\frac a{f^n}=\frac a1\frac1{f^n}\in h(y)$.
$\mathrm{Spec} A^0_f\to\mathrm{Proj}\mid_{D(f)}$¶
In this case, given a prime ideal in $A^0_f$ we need to construct an relevant homogeneous prime ideal of $A$. We define the following $$ g:x \mapsto \left\{a\left|\text{for all $i\in\mathbb N$, $\frac{a_i^m}{f^i}\in x$}\right.\right\}. $$
Then we need to prove that
- $g(x)$ is an ideal;
- $g(x)$ is homogeneous;
- $g(x)$ is prime;
- $g(x)$ is relevant;
- $g$ is continuous.
$g(x)$ is an ideal¶
$0\in g(x)$
$g(x)$ is an ideal¶
if $a,b\in g(x)$, then $a + b\in g(x)$ because $$ \begin{equation*} \begin{aligned} \left(\frac{(a_i+b_i)^m}{f^i}\right)^2 &=\frac{(a_i+b_i)^{2m}}{f^{2i}} \\ &= \frac{\sum_{j=0}^{2m}{2m\choose j}a_i^j b_i^{2m-j}}{f^{2i}} \\ &= \sum_{j=0}^{2m}{2m\choose j}\frac{a_i^j b_i^{2m-j}}{f^{2i}} \end{aligned} \end{equation*} $$ if $m\le j$, we write $$ \frac{a_i^j b_i^{2m-j}}{f^{2i}} = \frac{a_i^m}{f^i}\frac{a_i^{j-m}b_i^{2m-j}}{f^i}; $$ otherwise, we write $$ \frac{a_i^j b_i^{2m-j}}{f^{2i}} =\frac{b_i^m}{f^i}\frac{a_i^jb_i^{m-j}}{f^i} $$
$g(x)$ is an ideal¶
if $a, b \in A$ and $b\in g(x)$, then $ab\in g(x)$. We induction on $a$
- if $a = 0$, then $(ab)_i=0$;
- if $a\in A_n$ and $n\le i$ then $(ab)_i=ab_{n-i}$;
- if the result hold for $a_1, a_2$, then $(a_1+a_2)b=a_1b+a_2b\in g(x)$.
$g(x)$ is homogeneous¶
If $a\in g(x)$ then for any $i\in\mathbb N$, $a_i\in g(x)$, for $\left(a_i\right)_j=a_i$ or $0$.
$g(x)$ is prime¶
For a homogeneous ideal, prime condition is equivalent to being homogeneously prime, i.e. $\mathfrak p$ is prime if and only if $1\not\in\mathfrak p$ and for any $a\in A_i$ and $b\in A_j$, $ab\in\mathfrak p$ implies $a\in\mathfrak p$ or $b\in\mathfrak p$. $1 \not\in g(x)$ because the zeroth projection of $1$ is $1$.
Suppose $a\in A_i$ and $b\in A_j$, suppose $a,b\not\in g(x)$ then $\frac{a_n^m}{f^n}\not\in x$ for some $n\in\mathbb N$ and $\frac{b_k^m}{f^k}\not\in x$ for some $k\in\mathbb N$. Then $n=i$ for otherwise $0\not\in x$ and similarly $k=j$. So $\frac{(ab)_{i+j}^m}{f^{i+j}}=\frac{a_i^m}{f^i}\frac{b_j^m}{f^j}\not\in x$.
$g(x)$ is relevant¶
If $\bigoplus_{1\le i}A_i\le g(x)$ then
- $f\not\in g(x)$, for otherwise $1=\frac{f_m^m}{f^m}\in x$, but $x\ne A^0_f$
- also $f\in\bigoplus_{1\le i}A_i$, since $f_0=0$. Contradicting $\bigoplus_{1\le i}A_i\le g(x)$ and $f\not\in g(x)$.
$h\circ g=1$¶
$h(g(x))\le x$ because if $z\in h(g(x))$ then $z\in\mathrm{span}\left\{\frac c{f^i}|c\in g(x)\cap A_{mi}\right\}$. So we write $$ z=\sum_i \frac{a_i}{f^{n_i}}\frac{c_i}{f^{k_i}} $$ since $c_i\in g(x)\cap A_{mk_i}$, $\frac{c_i^m}{f^{mk_i}}\in x$, so $\left(\frac{c_i}{f^{k_i}}\right)^m\in x$, so we are done since $x$ is prime.
$x\le h(g(x))$ because if $\frac{a}{f^k} \in x$ for $a\in A_{mk}$, then $a\in g(x)$ for $\frac{a_i^m}{f^i}=\frac{a^m}{f^{mk}}=\left(\frac{a}{f^k}\right)^m\in x$ if $i=mk$ or $0$ otherwise. Thus $\frac{a}{f^k}\in\mathrm{span}\left\{\frac c1|c \in g(x)\right\}\cap A^0_f$ since $\frac{a}{f^k}=\frac a 1\frac1{f^k}$.
$g\circ h=1$¶
$g(h(x))\le x$. If $z\in g(h(x))$, we need to show $z_i\in x$. Since $\frac{z_i^m}{f^i}\in h(x)$, we write $$ \frac{z_i^m}{f^i}=\sum_j\frac{c_j}{f^{n_j}}\frac{d_j}1, $$ with $d_j\in x$, by multiplying a suitable power of $f$, we get $$ z_i^mf^N=\sum_jc_jd_jf^{N_j}. $$ So $z_i\in x$.
$x\le g(h(x))$. If $z\in x$, then $z_i\in x$ because $x$ is homogeneous. So $\frac{z_i^m}{f^i}=\frac1{f^i}\left(\frac{z_i}1\right)^m\in h(x)$ because $\frac{z_i}1\in h(x)$.
Now we know that $h$ and $g$ are both bijective.
continuity¶
$\mathrm{Proj}|_{D(f)}$ has a basis of the form $D(f)\cap D(a)$, so we check preimages of these are open. We consider $h(D(f)\cap D(a))=h\left(D(f)\cap\bigcup_iD(a_i)\right)=\bigcup_i h(D(f)\cap D(a_i))$. Each $h(D(f)\cap D(a_i))$ is open because $h(D(f)\cap D(a_i))=D\left(\frac{a_i^m}{f^i}\right)$ in $\mathrm{Spec} A^0_f$. To prove $h(D(f)\cap D(a_i))=D\left(\frac{a_i^m}{f^i}\right)$, it is sufficient to prove $h^{-1}(D\left(\frac{a_i^m}{f^i}\right))=D(f)\cap D(a)$ and this proven in continuity of $h$.
Now we only need to prove the preimage of $D(f)\cap D(a)$ is $h(D(f)\cap D(a))$, this can be easily proved by the fact that $h\circ g$ and $g\circ h$ are both identity.
Thus we have proven that $\mathrm{Proj}|_{D(f)}\cong \mathrm{Spec} A^0_f$ as topological spaces.
$\phi:h_*\mathcal O_{\mathrm{Proj}\mid_{D(f)}}\to \mathcal O_{\mathrm{Spec}A^0_f}$¶
Fix an open set $U\subseteq\mathrm{Spec}A^0_f$, so we need a ring homomorphism $\mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(U))\to\mathcal O_{\mathrm{Spec}A^0_f}(U)$.
Fix a $s:\prod_{z\in h^{-1}(U)}A^0_{(z)}$. If $x\in U$, then $g(x)\in h^{-1}(U)$. Then we have $s(g(x))=\frac n d\in A^0_{(g(x))}$ for some $n, d \in A_i$.
Thus define $$ \phi_U(s)(x)=\frac{\frac{nd^{m-1}}{f^i}}{\frac{d^m}{f^i}}. $$
One can check that this is well defined. Assuming that this is indeed a ring homomorphism, it is easy to check the following diagram commute. $$ \require{AMScd} \begin{CD} \mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(U)) @>{\phi_U}>> \mathcal O_{\mathrm{Spec}A^0_f}(U) \\ @VVV @VVV \\ \mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(V)) @>{\phi_V}>> \mathcal O_{\mathrm{Spec}A^0_f}(V) \end{CD}\\ $$
$\phi_U(1)(x)=1$¶
Suppose $1=s(g(1))=\frac n d$ where $n,d\in A_i$, so for some $c\not\in g(1)$, $nc=dc$. Since $c\not\in g(1)$, there is some $j\in\mathbb N$, $\frac{c_j^m}{f^j}\not\in x$. Then $(nc)_{i+j}=(dc)_{i+j}=nc_j=dc_j$. Then $$ \frac{c_j^m}{f^j}\frac{nd^{m-1}}{f^i}=\frac{c_j^mnd^{m-1}}{f^{i+j}}=\frac{(dc_j)^m}{f^{i+j}}=\frac{c_j^m}{f^j}\frac{d^m}{f^i}, $$ i.e. $\phi_U(1)(x)=1$.
Similarly one can prove that $\phi_U(0)(x)=0$.
$\phi_U(s_1+s_2)(x)=\phi_U(s_1)(x)+\phi_U(s_2)(x)$¶
Let's say $s_1(g(x))=\frac{n_1}{d_1}$ with $n_1,d_1\in A_{i_1}$, $s_2(g(x))=\frac{n_2}{d_2}$ with $n_2, d_2\in A_{i_2}$ and $(s_1+s_2)(g(x))=\frac{n_{12}}{d_{12}}=\frac{n_1}{d_1}+\frac{n_2}{d_2}$ with $n_{12}, d_{12}\in A_{i_{12}}$. So our goal is to check $$ \begin{equation} \frac{\frac{n_{12}d_{12}^{m-1}}{f^{i_{12}}}}{\frac{d_{12}^m}{f^{i_{12}}}}=\frac{\frac{n_1d_1^{m-1}}{f^{i_1}}}{\frac{d_1^m}{f^{i_1}}} + \frac{\frac{n_2d_2^{m-1}}{f^{i_2}}}{\frac{d_2^m}{f^{i_2}}}. \end{equation} $$
From $\frac{n_{12}}{d_{12}}=\frac{n_1}{d_1}+\frac{n_2}{d_2}=\frac{n_1d_2+n_2d_1}{d_1d_2}$, so we can find a $c\not\in g(x)$, such that $$ n_{12}d_1d_2c=(n_1d_2+n_2d_1)d_{12}c. $$ Since $c\not\in g(x)$, there is some $j\in\mathbb N$ such that $\frac{c_j^m}{f^j}\not\in x$. Then by taking the $i_1+i_2+i_{12}+j$-th projection $$ n_{12}d_1d_2c_j=(n_1d_2+n_2d_1)d_{12}c_j. $$
Using this, one can check that by multiplying $\frac{c_j^m}{f^j}$, the desired equality can be proved.
Similarly $\phi_U(s_1s_2)(x)=\phi_U(s_1)(x)\phi_U(s_2)(x)$.
$\phi_U(s)$ is locally quotient¶
Since $s$ is locally quotient, for any $x\in U$, there is some open set $V\subseteq \mathrm{Proj}$ such that $g(x)\in V\subseteq h^{-1}(U)$ such that $s(y)=\frac a b$ for all $y\in V$ where $a,b\in A_n$ and $b\not\in y$.
To check $\phi_U(s)$ is locally quotient, use the open subset $h(V)$ and check that for all $z\in h(V)$ $$ \phi_U(s)(z)=\frac{ab^{m-1}}{b^m}. $$
$\psi:\mathcal O_{\mathrm{Spec}A^0_f}\to h_*\mathcal O_{\mathrm{Proj}\mid_{D(f)}}$¶
Fix an open set $U\subseteq\mathrm{Spec}A^0_f$, so we need a ring homomorphism $\mathcal O_{\mathrm{Spec}A^0_f}(U)\to \mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(U))$.
Let $s\in \mathcal O_{\mathrm{Spec}A^0_f}(U)$ and $y\in h^{-1}(U)$, then $h(y)\in U$, so we can write $$ s(h(y))=\frac{a}{b} $$ where $a,b\in A^0_f$. Then we can write $a=\frac{n_a}{f^{i_a}}$ for some $n_a\in A_{mi_a}$ and $b=\frac{n_b}{f^{i_b}}$ for some $n_b\in A_{mi_b}$.
Then we can define $$ \psi_U(s)(y)=\frac{n_af^i_b}{n_bf^{i_a}} $$.
One can check this is well defined. Assuming that this is a ring homomorphism, it is easy to check the following diagram commute. $$ \require{AMScd} \begin{CD} \mathcal O_{\mathrm{Spec}A^0_f}(U)) @>{\psi_U}>> \mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(U)) \\ @VVV @VVV \\ \mathcal O_{\mathrm{Spec}A^0_f}(V)) @>{\psi_V}>> \mathcal O_{\mathrm{Proj}\mid_{D(f)}}(h^{-1}(V)) \end{CD}\\ $$
$\psi_U(1)(y)=1$¶
Suppose $\frac11=1(h(y))=\frac a b$ where $a,b\in A^0_f$, then for some $\frac c{f^l}\not\in h(y)$ $$ \frac {n_ac}{f^{i_a+l}}=\frac {n_bc}{f^{i_b+l}} $$ Thus, for some $n_1\in\mathbb N$ $$ n_acf^{i_b+l+n_1}=n_bcf^{i_a+l+n_1} $$ Thus $$ \psi_U(1)(y)=\frac{n_af^{b_i}}{n_bf^{i_a}}=1. $$
Similarly $\psi_U(0)(y)=0$.
$\psi_U(s_1s_2)(y)=\psi_U(s_1)(y)\cdot\psi_U(s_2)(y)$¶
Let's write $$ s_1(h(y))=\frac{\frac{a_1}{f^{i_1}}}{\frac{b_1}{f^{j_1}}}, s_2(h(y))=\frac{\frac{a_2}{f^{i_2}}}{\frac{b_2}{f^{i_2}}}, (s_1s_2)(h(y))=\frac{\frac{a_{12}}{f^{i_{12}}}}{\frac{b_{12}}{f^{j_{12}}}}. $$
Then $\frac{\frac{a_1a_2}{f^{i_1+i_2}}}{\frac{b_1b_2}{f^{j_1+j_2}}}=\frac{\frac{a_{12}}{f^{i_{12}}}}{\frac{b_{12}}{f^{j_{12}}}}$, i.e. for some $\frac{c}{f^l}$, we have
$$ \frac{a_1a_2b_{12}c}{f^{i_1+i_2+j_{12}+l}}=\frac{a_{12}b_1b_2c}{f^{i_{12}+j_1+j_2+l}}, $$i.e. for some $L\in\mathbb N$, we have
$$ a_1a_2b_{12}cf^{i_{12}+j_1+j_2+l+L}=a_{12}b_1b_2cf^{i_1+i_2+j_{12}+l+L}. $$We can use this to prove that $$ \frac{a_{12}f^{j_{12}}}{b_{12}f^{i_{12}}}=\frac{a_1f^{j_1}}{b_1f^{i_1}}\cdot\frac{a_2f^{j_2}}{b_2f^{i_2}}. $$
Similarly, we can prove that $\psi_U(s_1+s_2)(y)=\psi_U(s_1)(y)+\psi_U(s_2)(y)$.
$\psi_U(s)$ locally is fraction¶
Since $s$ locally is a fraction, there are open sets $h(y)\in V\subseteq U$, such that for all $z\in V$, $$ s(z)=\frac{\frac{a}{f^{l_1}}}{\frac{b}{f^{l_2}}}. $$
Then we use $h^{-1}(V)$ and verify that locally $$ \psi_U(s)(y)=\frac{af^{l_2}}{bf^{l_1}}. $$
$\psi\circ\phi=1$¶
Let $s\in\mathcal O_{\mathrm{Proj}|_{D(f)}}(h^{-1}(U))$, then for $x\in h^{-1}(U)$ $$ \phi_U(s)=x\mapsto \frac{\frac{nd^{m-1}}{f^i}}{\frac{d^m}{f^i}}, $$ where $s(x)=\frac n d$.
Thus $$ \psi_U(\phi_U(s))(x)=\frac{nd^{m-1}f^i}{d^mf^i}=\frac n d=s(x) $$
$\phi\circ\psi=1$¶
Let $s\in\mathcal O_{\mathrm{Spec}A^0_f}(U)$, then for $x\in U$ $$ \psi_U(s)=x\mapsto \frac{n_af^{i_b}}{n_bf^{i_a}} $$ where $$s(x)=\frac{\frac{n_a}{f^{i_a}}}{\frac{n_b}{f^{i_b}}}.$$
Thus $$ \phi_U(\psi_U(s))(x)=\frac{\frac{n_af^{i_b}\left(n_bf^{i_a}\right)^{m-1}}{f^{j}}}{\frac{\left(n_bf^{i_a}\right)^m}{f^{j}}}=\frac{\frac{n_a}{f^{i_a}}}{\frac{n_b}{f^{i_b}}}=s(x). $$