- Boxes
- definitions
- Ellipses
- theorems and lemmas
- Blue border
- the statement of this result is ready to be formalized; all prerequisites are done
- Orange border
- the statement of this result is not ready to be formalized; the blueprint needs more work
- Blue background
- the proof of this result is ready to be formalized; all prerequisites are done
- Green border
- the statement of this result is formalized
- Green background
- the proof of this result is formalized
- Dark green background
- the proof of this result and all its ancestors are formalized
- Dark green border
- this is in Mathlib
If \((I_i)_{i \in I}\) is a family of radical ideals, then \(\bigcap _{i \in I} I_i\) is radical.
A frame homomorphism from a presented frame is completely determined by its action on generators.
An affine scheme is a locally ringed locale of the form \((\mathrm{Spec} R, \mathcal{O}_{\mathrm{Spec} R})\) for some commutative ring \(R\), where:
\(\mathrm{Spec} R = \mathrm{Rad}(R)\) is the Zariski locale
\(\mathcal{O}_{\mathrm{Spec} R}\) is the structure sheaf constructed in Definition 38
For \(f \in R\), define the basic open set (in the Zariski locale):
where \((f)\) is the principal ideal generated by \(f\).
A closed sublocale of \(\mathrm{Spec} R\) corresponds to a radical ideal \(I \in \mathrm{Rad}(R)\) and is denoted \(V(I)\). The closed sublocale is:
with the induced lattice operations from \(\mathrm{Rad}(R)\).
A frame is a complete lattice \((L, \leq )\) satisfying the infinite distributive law (frame distributivity):
for all \(a \in L\) and all families \((b_i)_{i \in I}\) of elements of \(L\).
A map \(f: L \to M\) between frames is a frame homomorphism if it:
Preserves arbitrary joins: \(f(\bigvee _{i \in I} a_i) = \bigvee _{i \in I} f(a_i)\)
Preserves finite meets: \(f(a \land b) = f(a) \land f(b)\) and \(f(\top ) = \top \)
For a ring homomorphism \(\phi : R \to S\), define:
by:
for each radical ideal \(I \in \mathrm{Rad}(R)\).
A locale \(X\) is irreducible if the frame \(\mathcal{O}(X)\) has no non-trivial prime elements... wait, that doesn’t seem right. Let me reconsider.
Actually, a locale is irreducible if it is non-empty and is not the union of two proper closed sublocales.
A scheme \(X\) is irreducible if its underlying locale is irreducible, i.e., the only way to write \(\top = u \lor v\) (where \(u, v\) are opens) is if \(u = \top \) or \(v = \top \).
A locale is a formal dual of a frame. The category \(\mathbf{Loc}\) has:
Objects: Frames (understood as the lattice of open sets of a generalized space)
Morphisms: \(\mathrm{Hom}_{\mathbf{Loc}}(X, Y) := \mathrm{Hom}_{\mathbf{Frame}}(\mathcal{O}(Y), \mathcal{O}(X))\) (contravariant)
For \(f \in R\), define \(R_f\) as the localization of \(R\) at the multiplicative set \(\{ 1, f, f^2, \ldots \} \):
with the obvious ring operations.
A locally ringed locale is a pair \((X, \mathcal{O}_X)\) where:
\(X\) is a locale (a frame)
\(\mathcal{O}_X\) is a sheaf of rings on \(X\)
For every open \(u \in X\), the stalk \(\mathcal{O}_{X,\bar{u}}\) is a local ring (has a unique maximal ideal)
A morphism of affine schemes from \(\mathrm{Spec} R\) to \(\mathrm{Spec} S\) is a morphism of locally ringed locales, i.e., a pair \((f_{\# }, f^{\sharp })\) where:
\(f_{\# }: \mathrm{Spec} R \to \mathrm{Spec} S\) is a locale morphism (i.e., a frame homomorphism \(f_{\# }^*: \mathrm{Rad}(S) \to \mathrm{Rad}(R)\))
\(f^{\sharp }: \mathcal{O}_S \to f_{\# *} \mathcal{O}_R\) is a morphism of sheaves of rings respecting the local ring structure
An open sublocale of a locale \(X\) is determined by an open \(u \in X\). The frame of opens of the sublocale is:
with the induced lattice operations from \(X\).
A frame presented by a set of generators \(G\) and a set of relations \(R\) is denoted:
This is the free frame on generators \(G\) quotiented by the frame congruence generated by \(R\).
An element \(p\) of a frame \(L\) is prime if whenever \(p \leq a \lor b\), we have \(p \leq a\) or \(p \leq b\).
An ideal \(\mathfrak {p} \in \mathrm{Rad}(R)\) is prime if it is a prime element in the frame \(\mathrm{Rad}(R)\).
Equivalently: \(\mathfrak {p}\) is prime if \(\mathfrak {p} \neq R\) and whenever \(fg \in \mathfrak {p}\), we have \(f \in \mathfrak {p}\) or \(g \in \mathfrak {p}\).
For a ring homomorphism \(\phi : R \to S\) and an ideal \(I \triangleleft R\), the pushforward is:
This is the ideal of \(S\) generated by \(\phi (I)\).
An ideal \(I \triangleleft R\) of a commutative ring \(R\) is radical if \(I = \sqrt{I}\), where
The set of all radical ideals of \(R\) is denoted \(\mathrm{Rad}(R)\).
For radical ideals \(I, J \in \mathrm{Rad}(R)\):
Order: \(I \leq J :\iff I \subseteq J\) (set inclusion)
Meet (Infimum): \(I \land J := I \cap J\) (intersection)
Join (Supremum): For a family \((I_i)_{i \in I}\), we define \(\bigvee _i I_i := \sqrt{\sum _i I_i}\)
Top: \(\top := R\) (the whole ring, which is radical)
Bottom: \(\bot := \sqrt{(0)} = \mathrm{Nil}(R)\) (the nilradical)
A scheme is a locally ringed locale \((X, \mathcal{O}_X)\) such that \(X\) has an open cover \(\{ u_i : i \in I\} \) (where \(\bigvee _i u_i = \top \)) with the property that:
The restriction \((u_i, \mathcal{O}_X|_{u_i})\) to each open is isomorphic to an affine scheme \(\mathrm{Spec} R_i\)
The transition functions between affine pieces are given by ring homomorphisms
Let \(L\) be a frame (viewed as a category with objects being elements of \(L\) and morphisms being the order relations \(u \leq v\)). A sheaf on \(L\) with values in a category \(\mathcal{C}\) is a functor \(\mathcal{F}: L^{\mathrm{op}} \to \mathcal{C}\) such that for every family \((u_i)_{i \in I}\) with \(\bigvee _i u_i = u\):
is an equalizer diagram in \(\mathcal{C}\).
For a sheaf \(\mathcal{F}\) on a locale \(X\) and an element \(u \in X\), the stalk is defined as:
where \(\downarrow u := \{ v \in X : v \leq u\} \) is the principal order filter at \(u\).
For a radical ideal \(I \in \mathrm{Rad}(R)\), extend the structure sheaf by:
the inverse limit of localizations as \(f\) ranges over \(I\).
For \(I \leq J\) (i.e., \(I \subseteq J\)), the restriction map is induced by the universal property of limits.
Define \(\mathcal{O}_{\mathrm{Spec} R}\) on the basic opens by:
For a inclusion \(D(f) \leq D(g)\) (i.e., \(f \in \sqrt{(g)}\), so \(f^n = rg\) for some \(r\) and \(n \geq 1\)):
\(D(f) \land D(g) = D(fg)\)
\(D(f) \lor D(g) = \sqrt{D(f) + D(g)} = D(f) \lor D(g)\) (not generally a basic open)
More generally, for a family \((f_i)_{i \in I}\): \(\bigvee _i D(f_i) = \sqrt{(f_i : i \in I)}\)
The basic opens satisfy:
\(D(1) = \sqrt{(1)} = R = \top \)
\(D(0) = \sqrt{(0)} = \sqrt{\{ 0\} } = \{ x : \exists n, x^n = 0\} = \bot \) (the nilradical)
\(D(fg) = D(f) \land D(g)\)
\(D(f^n) = D(f)\) for all \(n \geq 1\)
For any \(f \in R\), the ideal \(D(f) = \sqrt{(f)}\) is radical.
Arbitrary intersections of closed sublocales are closed: if \((I_j)_{j \in J}\) are radical ideals, then \(V(I_j)\) are closed and \(\bigcap _j V(I_j) = V(\sum _j I_j) = V(\bigvee _j I_j)\).
For \(f \in R\) and a family \((g_i)_{i \in I}\) of elements of \(R\):
For the identity ring homomorphism \(\mathrm{id}_R : R \to R\):
If \(I, J \in \mathrm{Rad}(R)\), then \(I \cap J \in \mathrm{Rad}(R)\).
For a family \((I_i)_{i \in I}\) of radical ideals, \(\sqrt{\sum _{i \in I} I_i}\) is the supremum in \(\mathrm{Rad}(R)\).
Composition of locale morphisms is well-defined and associative.
There is a canonical ring homomorphism \(\iota _f: R \to R_f\) sending \(r \mapsto r/1\).
If \(f\) is a unit in \(R\), then \(R_f = R\).
If \(f\) is nilpotent, then \(R_f\) is the zero ring.
For a family \((I_j)_{j \in J}\) of radical ideals:
For \(I, J \in \mathrm{Rad}(R)\):
A radical ideal \(\mathfrak {p}\) is prime iff: \(\mathfrak {p} \leq I \lor J \implies \mathfrak {p} \leq I \text{ or } \mathfrak {p} \leq J\) for all radical ideals \(I, J\).
For ideals \(I, J \triangleleft R\):
If \(I \in \mathrm{Rad}(R)\), then \(\phi ^*(I) = \sqrt{\phi (I) \cdot S} \in \mathrm{Rad}(S)\).
For \(f \in R\) and \(I \in \mathrm{Rad}(R)\):
For \(D(f) \leq D(g) \leq D(h)\), the restriction maps satisfy:
For \(f \in \sqrt{(g)}\) (so \(f^n = rg\)), the map \(\rho _{g,f}\) is a well-defined ring homomorphism.
Let \(L = \mathrm{Fr}\langle G \mid R \rangle \) be a presented frame, and let \(M\) be another frame. A frame homomorphism \(f: L \to M\) is determined by:
A function \(\phi : G \to M\)
A verification that the relations \(R\) are respected: for every relation in \(R\), \(\phi \) satisfies it in \(M\)
Every affine scheme \((\mathrm{Spec} R, \mathcal{O}_{\mathrm{Spec} R})\) is a locally ringed locale.
There exists a contravariant functor:
defined by:
Objects: \(\mathrm{Spec}(R) := \mathrm{Rad}(R)\) (viewed as a locale)
Morphisms: For \(\phi : R \to S\) in \(\mathbf{CRing}\), \(\mathrm{Spec}(\phi ) := (\phi ^*)^{\mathrm{op}}: \mathrm{Spec}(S) \to \mathrm{Spec}(R)\)
with:
\(\mathrm{Spec}(\mathrm{id}_R) = \mathrm{id}_{\mathrm{Spec}(R)}\)
For \(\phi : R \to S\) and \(\psi : S \to T\): \(\mathrm{Spec}(\psi \circ \phi ) = \mathrm{Spec}(\phi ) \circ \mathrm{Spec}(\psi )\)
For a ring homomorphism \(\phi : R \to S\), the map \(\phi ^*: \mathrm{Rad}(R) \to \mathrm{Rad}(S)\) is a frame homomorphism.
A radical ideal \(\mathfrak {p} \in \mathrm{Rad}(R)\) is prime iff \(\mathfrak {p}\) is the set of elements that specialize to a fixed point in the topological spectrum (if we were to use points). Pointfree, this means \(\mathfrak {p}\) is exactly the closure of the empty set in the principal filter \(\uparrow \mathfrak {p}\).
The structure \((\mathrm{Rad}(R), \leq , \land , \bigvee , \top , \bot )\) with operations as in Definition 10 forms a complete lattice.
The complete lattice \((\mathrm{Rad}(R), \leq , \land , \bigvee , \top , \bot )\) satisfies the infinite distributive law:
for all \(I \in \mathrm{Rad}(R)\) and all families \((K_j)_{j \in J}\) of radical ideals.
Every ring homomorphism \(\phi : S \to R\) induces a morphism of affine schemes:
The structure sheaf \(\mathcal{O}_{\mathrm{Spec} R}\) is a sheaf on the Zariski locale \(\mathrm{Rad}(R)\).
Schemes form a category with morphisms being locale morphisms respecting the ringed structure. Affine schemes are the full subcategory of schemes admitting a single affine open cover.
The Zariski frame of a commutative ring \(R\) admits the presentation:
where the relations \(\mathcal{R}\) are:
\(D(1) = \top \)
\(D(0) = \bot \)
\(D(fg) = D(f) \land D(g)\)
\(D(f^n) = D(f)\) for all \(n \geq 1\)
For any family \((f_i)_{i \in I}\) with \(1 \in (f_i : i \in I)\): \(\bigvee _i D(f_i) = \top \)