$Spec R$, just as a topological space.

The type family over prime_spectrum R consisting of the localization over each point.

The predicate saying that a dependent function on an open U is realised as a fixed fraction r / s in each of the stalks (which are localizations at various prime ideals).

The predicate is_fraction is "prelocal", in the sense that if it holds on U it holds on any open subset V of U.

We will define the structure sheaf as the subsheaf of all dependent functions in Π x : U, localizations R x consisting of those functions which can locally be expressed as a ratio of (the images in the localization of) elements of R.

Quoting Hartshorne:

For an open set $$U ⊆ Spec A$$, we define $$𝒪(U)$$ to be the set of functions $$s : U → ⨆_{𝔭 ∈ U} A_𝔭$$, such that $s(𝔭) ∈ A_𝔭$$ for each $$𝔭$$, and such that $$s$$ is locally a quotient of elements of $$A$$: to be precise, we require that for each $$𝔭 ∈ U$$, there is a neighborhood $$V$$ of $$𝔭$$, contained in $$U$$, and elements $$a, f ∈ A$$, such that for each $$𝔮 ∈ V, f ∉ 𝔮$$, and $$s(𝔮) = a/f$$ in $$A_𝔮$$.

Now Hartshorne had the disadvantage of not knowing about dependent functions, so we replace his circumlocution about functions into a disjoint union with Π x : U, localizations x.

The functions satisfying is_locally_fraction form a subring.

The structure sheaf (valued in Type, not yet CommRing) is the subsheaf consisting of functions satisfying is_locally_fraction.

The structure presheaf, valued in CommRing, constructed by dressing up the Type valued structure presheaf.

Some glue, verifying that that structure presheaf valued in CommRing agrees with the Type valued structure presheaf.

The structure sheaf on $Spec R$, valued in CommRing.

This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.

The stalk at x is equivalent (just as a type) to the localization at x.

The section of structure_sheaf R on an open U sending each x ∈ U to the element f/g in the localization of R at x.

The canonical ring homomorphism interpreting an element of R as a section of the structure sheaf.

The canonical ring homomorphism interpreting an element of R as an element of the stalk of structure_sheaf R at x.

The canonical ring homomorphism interpreting s ∈ R_f as a section of the structure sheaf on the basic open defined by f ∈ R.

The canonical ring homomorphism from the localization of R at p to the stalk of the structure sheaf at the point p.

The ring homomorphism that takes a section of the structure sheaf of R on the open set U, implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates the section on the point corresponding to a given prime ideal.

The ring homomorphism from the stalk of the structure sheaf of R at a point corresponding to a prime ideal p to the localization of R at p, formed by gluing the open_to_localization maps.

The ring isomorphism between the stalk of the structure sheaf of R at a point p corresponding to a prime ideal in R and the localization of R at p.