Pointless Schemes

1 Foundational Locale Theory

1.1 Frames and Basic Structure

Definition 1 Frame
#

A frame is a complete lattice \((L, \leq )\) satisfying the infinite distributive law (frame distributivity):

\[ a \land \bigvee _{i \in I} b_i = \bigvee _{i \in I} (a \land b_i) \]

for all \(a \in L\) and all families \((b_i)_{i \in I}\) of elements of \(L\).

Definition 2 Frame Homomorphism
#

A map \(f: L \to M\) between frames is a frame homomorphism if it:

  1. Preserves arbitrary joins: \(f(\bigvee _{i \in I} a_i) = \bigvee _{i \in I} f(a_i)\)

  2. Preserves finite meets: \(f(a \land b) = f(a) \land f(b)\) and \(f(\top ) = \top \)

Remark 3
#

Note that frame homomorphisms need not preserve \(\bot \). The category of frames and frame homomorphisms is denoted \(\mathbf{Frame}\).

Definition 4 Locale
#

A locale is a formal dual of a frame. The category \(\mathbf{Loc}\) has:

  1. Objects: Frames (understood as the lattice of open sets of a generalized space)

  2. Morphisms: \(\mathrm{Hom}_{\mathbf{Loc}}(X, Y) := \mathrm{Hom}_{\mathbf{Frame}}(\mathcal{O}(Y), \mathcal{O}(X))\) (contravariant)

Lemma 5 Locale Morphism Composition
#

Uses

Composition of locale morphisms is well-defined and associative.

Proof ▶

Let \(f: X \to Y\) and \(g: Y \to Z\) be locale morphisms. Then:

\begin{align*} (g \circ f)_{\mathrm{frame}} & := f_{\mathrm{frame}} \circ g_{\mathrm{frame}} : \mathcal{O}(Z) \to \mathcal{O}(X) \end{align*}

The composition of frame homomorphisms is a frame homomorphism (by definition of frame homomorphism).

For joins: \((f_{\mathrm{frame}} \circ g_{\mathrm{frame}})(\bigvee _{i} u_i) = f_{\mathrm{frame}}(g_{\mathrm{frame}}(\bigvee _i u_i)) = f_{\mathrm{frame}}(\bigvee _i g_{\mathrm{frame}}(u_i)) = \bigvee _i f_{\mathrm{frame}}(g_{\mathrm{frame}}(u_i))\).

For finite meets: similarly by composition of homomorphisms.

Associativity follows from associativity of function composition.

1.2 Frame Presentations

Definition 6 Presented Frame
#

A frame presented by a set of generators \(G\) and a set of relations \(R\) is denoted:

\[ \mathrm{Fr}\langle G \mid R \rangle \]

This is the free frame on generators \(G\) quotiented by the frame congruence generated by \(R\).

Lemma 7 Universal Property of Presented Frames
#

Uses

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:

  1. A function \(\phi : G \to M\)

  2. A verification that the relations \(R\) are respected: for every relation in \(R\), \(\phi \) satisfies it in \(M\)

Proof ▶

The universal property follows from the definition of the quotient of the free frame by a frame congruence.

Given \(\phi : G \to M\) respecting \(R\), it extends uniquely to a frame homomorphism \(\tilde{\phi }: \mathrm{Fr}(G) \to M\) on the free frame, since \(\mathrm{Fr}(G)\) is free.

Since \(\phi \) respects the relations \(R\) generating the congruence, the map \(\tilde{\phi }\) descends to a frame homomorphism \(\bar{\phi }: L \to M\).

Uniqueness follows from the universal property of the free frame and the quotient.

Corollary 8 Characterization by Generators and Relations
#

Uses

A frame homomorphism from a presented frame is completely determined by its action on generators.