adding

- Max Zeuner,
*A univalent formalization of affine schemes*, 20 October 2022 (slides, video)

Anonymous

]]>Adding reference

- Anders Mörtberg, Max Zeuner,
*A Univalent Formalization of Affine Schemes*(arXiv:2212.02902)

Anonymous

]]>I feel like some things could be stated in a stronger and more categorical way. I found some of what was written confusingly weak, but maybe I’m getting something wrong.

The stated bijection is natural [1], i.e. this is really an adjunction $\mathrm{CRing}(T, \Gamma_Y\mathcal O\Gamma \dashv \mathrm{Spec}$ between $\mathrm{CRing}^\mathrm{op}$ and Scheme. Furthermore not only exists there some fully faithful functor from the affine schemes to the category of rings as stated in Proposition 2.1, but Spec is fully faithful, i.e. $\mathrm{CRing}^\mahrm{op}$ is a full reflective subcategory of Schemes, equivalent to it’s image, the affine schemes 2.

Lastly the statement that $h : \mathrm{Scheme}(\mathrm{Spec}(-), -) : \mathrm{Scheme} \to \mathrm{PSh}(\mathrm{CRing})$ being fully faithful is the same as saying that Spec is a dense functor or that the affine schemes are a dense subcategory of the category of schemes. This might be nice to state explicitly, as I was struggling to find anything about whether this was the case, though, maybe it’s just not interesting.

[1]: Hartshorn, exercise II.2.4

]]>Added redirect: Zariski duality. To satisfy a link at duality between geometry and algebra.

]]>Affine schemes are really isomorphic to prime spectra, not locally isomorphic; the statement would have been correct for general schemes qua locally ringed spaces.

Anonymous

]]>Made explicit the fully faithfulness of $\mathcal{O} \colon Schemes_{Aff} \to Ring^{op}$ (here) and added pointer to Hartschorne’s “Algebraic Geometry”, chapter II, prop. 2.3 for proof.

]]>What’s a canonical citation for the equivalence between the category of affine schemes and the opposite of finitely generated reduced algebras?

(The reference [21] given on Wikipedia here seems to be broken. Following it, I find no prop. 2.3 at all in chapter II. (?))

]]>Nice! I’ll add both mnemonics to the article.

]]>Another mnemonic is that such dualities work the same way as ordinary Galois connections between power sets. If $R \in P(X \times Y)$ is a relation, then the Galois connection it induces between $P X$ and $P Y$ looks like $T \leq S \backslash R$ iff $S \leq R/T$. You’re always homming *into* (not out of) the functorial construction.

At *affine scheme*, the fundamental theorem on morphisms of schemes was stated the other way round. I fixed that.

As a handy mnemonic, here is a quick and down-to-earth way to see that the claim “$Sch(Spec R, Y) \cong CRing(\mathcal{O}_Y(Y), R)$” is wrong. Take $Y = \mathbb{P}^n$ and $R = \mathbb{Z}$. Then the left hand side consists of all the $\mathbb{Z}$-valued points of $\mathbb{P}^n$. On the other hand, the right hand side only contains the unique ring homomorphism $\mathbb{Z} \to \mathbb{Z}$, since $\mathcal{O}_{\mathbb{P}^n}(\mathbb{P}^n) \cong \mathbb{Z}$.

]]>