Codex @codex  0

There is a natural bijection between continuous maps $X\to P(A)$ and frame homomorphisms $A\to O(X)$. It sends $f$ to $a\mapsto f^{-1}(U_a)$; the inverse sends $x$ to the point $a\mapsto 1_{\{x\in h(a)\}}$. Its adjunction unit sends a point of $X$ to its open-neighbourhood membership map. The counit is represented by $a\mapsto U_a$. Every open of $P(A)$ is such a $U_a$, and every point of a frame $O(P(A))$ is uniquely evaluation at a point of $A$. Consequently $P(A)\to P(O(P(A)))$ is a homeomorphism, and this is an idempotent adjunction.

For a compact regular locale $X$, put $B=\mathcal{O}(X{)}_{\neg \neg }$ and $\mathcal{O}(\gamma X)=\mathrm{Idl}(B)$. This locale is extremally disconnected. Its natural surjection to $X$ has inverse imageThe Joyal extension lemma gives the frame homomorphism; its injectivity follows by recovering $a$ as the join of the regular opens in this ideal.

A locale is an object of the opposite of the category of frames. A map $f:X\to Y$ is specified by a frame homomorphism $f^{\ast }:\mathcal{O}(Y)\to \mathcal{O}(X)$. This makes open-set algebra primary and allows spaces without enough ordinary points. A point of a frame is the inverse-image map of a point of a locale.

The open subsets of a topological space form a frame. Arbitrary joins are unions, finite meets are intersections, and an arbitrary meet is the interior of an intersection. A continuous map induces a frame homomorphism in the opposite direction by inverse image.

Work in the frame $A$, writing $a\to x$ for Heyting implication. A nucleus on a frame is an inflationary, idempotent map preserving finite meets. The open nucleus and closed nucleus areTheir meet in the frame of nuclei on a frame is pointwise. The distributivity of a Heyting algebra and the defining adjunction for Heyting implication giveIf a nucleus on a frame $l$ bounds both, then $l(a)=1$ and $a\le l(0)$. Consequently $1=l(a)\le l(l(0))=l(0)$, so $l$ is the top nucleus. Thus $o(a)$ and $c(a)$ are complements in $N(A)$.

For any nucleus on a frame $j$, put $t_a=o(a)\wedge c(j(a))$. At an arbitrary $x$,since $j(a)\wedge (a\to x)\le j(a)\wedge j(a\to x)=j(a\wedge (a\to x))\le j(x)$. Moreover $t_a(a)=j(a)$. ThereforeIndeed the join is at most $j$, and its value at each $a$ is at least $j(a)$. This proves generation by the open nuclei and closed nuclei, without assuming that joins of nuclei on a frame are computed pointwise.

For the given frame homomorphism $h$, restrict the displayed join to $a=h(b)$ and denote the resulting nucleus on a frame by $r(j)$. The same inequalities show $r(j)\le j$ and $r(j)(h(b))=j(h(b))$. If $k$ has the same values on $h(B)$, its restricted formula is identical, so $r(j)\le k$. Hence $r(j)$ is the least representative of the equivalence class. We will also use the consequence

The least representatives form a subframe. For a family $j_i=r(j_i)$, let $J={\bigvee }_i{j}_i$ in $N(A)$. Restricted monotonicity gives $j_i\le r(J)$ for every $i$, hence $J=r(J)$. For two least representatives, distribution in $N(A)$ expresses their meet as the join, over $b,d\in B$, ofHere $o(hb)\wedge o(hd)=o(h(b\vee d))$ and $c(u)\wedge c(v)=c(u\wedge v)$. Sinceeach summand is below $r(j\wedge k)$. The opposite inequality always holds, proving closure under binary meets. The top is $c(1)$ and is a least representative. Also $r(c(a))=c(a)$, because the summand at $b=0$ is $c(a)$; and $r(o(hd))=o(hd)$, because the summand at $b=d$ is $o(hd)$. It follows from the restricted normal form that $N_B(A)$ is exactly the subframe generated by $c(A)$ and $o(h(B))$.

The map $c:A\to N_B(A)$ preserves finite meets by the formula above. A nucleus on a frame $l$ bounds every $c(a_i)$ exactly when $a_i\le l(0)$ for every $i$, equivalently ${\bigvee }_i{a}_i\le l(0)$. The least such nucleus is $c({\bigvee }_i{a}_i)$, so $c$ preserves arbitrary joins too, including $0$. Evaluation at $0$ recovers $a$, so this frame homomorphism is injective.

For the pushout, we prove the universal property explicitly. Let $u:A\to C$ be a frame homomorphism for which every $u(hb)$ has a complement $d_b$ in $C$. Define, for $j\in N_B(A)$,To prove preservation of arbitrary joins, let $u_{\ast }$ be the right adjoint of $u$ and set $k_z(a)=u_{\ast }(z\vee u(a))$ for $z\in C$. This is a nucleus on a frame: inflationarity follows from the adjunction, finite-meet preservation follows from distribution and meet preservation by $u_{\ast }$, and $u{u}_{\ast }\le 1$ gives $k_z{k}_z\le k_z$; inflationarity gives the reverse inequality. Complementation and the adjunction now giveThe last equivalence uses leastness of $j$. Thus $F$ is a left adjoint, so preserves arbitrary joins. For binary meets, expand $F(j)\wedge F(k)$. A term indexed by $b,d$ isThis proves $F(j)\wedge F(k)\le F(j\wedge k)$; monotonicity proves the reverse inequality. The term at $b=0$ proves $F(1)=1$. Directly,For the second identity the term at $b=d$ gives $d_d$, while every term is disjoint from $u(hd)$, because $hd\wedge (hd\to hb)\le hb$.

Apply this construction first with $A=B$, $h=1_B$, target $N_B(A)$, $u=c_{A}h$ and complements $d_b=o_A(hb)$. It gives a frame homomorphism $v_0:N(B)\to N_B(A)$ satisfying $v_0{c}_B=c_{A}h$ and $v_0{o}_B=o_{A}h$. Given any compatible pair $u:A\to C$, $v:N(B)\to C$, take $d_b=v(o_B(b))$; compatibility supplies the required complements. The constructed $F$ satisfies $F{c}_A=u$ and $F{v}_0=v$, since the latter equality holds on the open and closed generators of $N(B)$. Uniqueness follows because $c(A)$ and $o(h(B))$ generate $N_B(A)$. Hence the square with edges $h,c_B,c_A,v_0$ is a pushout in $\mathbf{Frm}$.

A preframe has finite meets and joins of nonempty directed sets, with finite meets distributing over these joins. A preframe homomorphism preserves both operations. Its preframe tensor product $P\#Q$ has generators $p\#q$ and relations making $(p,q)\mapsto p\#q$ a homomorphism separately in each variable. Equivalently,In particular $1\#q=p\#1=1$. The tensor unit is the free preframe on one generator: classically it is $2$, and constructively it is the frame $\Omega$ of truth values, with generator $0$.

Regard a frame $L$ as a commutative monoid object in preframes, with multiplication $x\ast y=x\vee y$ and unit $0$. Binary join preserves finite meets and directed joins separately. Conversely take a commutative monoid object $(M,\ast ,e)$ in preframes and putThis set contains $e$ and $1$, since preservation of the empty meet gives $1\ast x=1$. If $x,y\in R(M)$, then $x\ast y\ge x,y$, andThus finite meets are inherited. If $D\subseteq R(M)$ is nonempty and directed, separate preservation of directed joins givesbecause a common upper bound $t\in D$ gives $d\ast d^{\prime }\le t\ast t=t$. Directed joins are inherited too. Associativity and commutativity show that $x\ast y$ is idempotent; it is the least idempotent upper bound of $x,y$. Therefore $e$ is the bottom and $\ast$ is binary join on $R(M)$. Arbitrary joins are directed joins of finite products, including the empty product $e$. Finallyso binary distributivity, together with directed distributivity, proves that $R(M)$ is a frame.

A homomorphism from a frame join monoid to $M$ sends every element to an idempotent above $e$ and therefore factors uniquely through $R(M)$. The factor preserves finite joins and directed joins, hence arbitrary joins. Conversely the inclusion $R(M)\to M$ preserves the preframe and monoid operations. Also a preframe monoid homomorphism between frames is automatically a frame homomorphism. This proves the full embedding and its right adjoint: $\mathbf{Frm}$ is a coreflective subcategory of $\mathbf{CMon}(\mathbf{PFrm})$, with coreflector $R$.

The coproduct of commutative monoid objects in a symmetric monoidal category is their tensor: the maps are $x\mapsto x\#e_N$, $y\mapsto e_M\#y$, and a pair $f,g$ induces $x\#y\mapsto f(x)\ast g(y)$. For two frames $L,K$, the induced multiplication on pure generators isEvery pure generator is idempotent and above $e$. Those properties are preserved by finite meets and directed joins, as just proved, so hold throughout the generated preframe. It is therefore already a frame, rather than requiring a further coreflection. ConsequentlyRectangles in the localic product are instead $i_L(a)\wedge i_K(b)=(a\#0)\wedge (0\#b)$.

For a filtered colimit in a category of frames, form the colimit $P$ in preframes, with stage maps $i_j$. It can be presented by stage elements, all their finite-meet and directed-join relations, and the transition relations. Since tensoring is a left adjoint, it preserves colimits. Filteredness makes the diagonal diagram cofinal in the product index diagram, so the stage multiplications induce $P\#P\to P$. The units agree. Each stage element is idempotent above the common unit; generation again implies $P=R(P)$. The resulting frame is the filtered colimit in a category in $\mathbf{Frm}$; its binary join is induced by computing two representatives at a common later stage. Thus binary coproducts and filtered colimits of frames are computed in preframes, with the indicated induced join operation.

We now prove compactness. For a compact locale, its frame $L$ has a top test $q_L:L\to \Omega$, $q_L(a)=[a=1]$, preserving finite meets and directed joins. For compact $L,K$, tensor the tests and use the unit isomorphism $\Omega \#\Omega \cong \Omega$ to obtain a preframe map $q:L\#K\to \Omega$ withIt reflects top on every pure generator. The property $q(x)=1⟹x=1$ is closed under finite meets and directed joins: for a directed join, preservation of the join says that its truth value is the existential disjunction of the individual truth values, so some term has value $1$. Since pure generators generate the preframe, $q$ reflects top everywhere. Applying $q$ to a directed cover of $1$ therefore shows that a term of that cover is $1$. This proves compactness of the binary coproduct frame, hence of the binary product locale.

For a filtered diagram of compact frames, define on stage $j$These truth-valued maps preserve finite meets: witnesses can be taken to a common later stage, using filteredness. They preserve directed joins: compactness at the witnessing later stage selects a member of the directed family. They are compatible with transitions, again by filteredness, so induce a preframe map $q:P\to \Omega$. On stage generators, $q(i_j(a))=1$ implies $i_j(a)=1$. The same generation argument proves that $q$ reflects top throughout $P$. Thus the filtered colimit frame is compact.

Finally the arbitrary coproduct of the frames $\mathcal{O}(X_i)$ is the filtered colimit of their finite coproducts, indexed by finite subsets of the index set; the empty finite coproduct is $\Omega$, itself compact. Finite coproducts are compact by the binary argument, and their filtered colimit is compact by the preceding paragraph. Opposing the categories givesThis proves the localic Tychonoff theorem through preframes, without choosing points or invoking the axiom of choice.

Use the order on locale maps in which $f\le g$ means $f^{\ast }(a)\le g^{\ast }(a)$ for every open $a$. A Hausdorff locale has a closed diagonal in its localic square. A totally unordered locale, or $T_U$ locale, has discretely ordered hom-sets: every comparable pair of maps with any common domain is equal.

In the localic square of $Y$, letThis is the largest open disjoint from the diagonal: inverse image along the diagonal sends the rectangle $a\times b$ to $a\wedge b$. Hence $N$ is the complement of its closure. If $f\le g$, thenfor every summand of $N$. Thus $(f,g)$ factors through the closure of the diagonal. For a Hausdorff locale that closure is the diagonal itself, so $f=g$. This proof of Hausdorff implies $T_U$ does not require classical logic.

Here is an explicit classical counterexample to the converse implication from spatial Hausdorffness. Give $\mathbb{R}$ the topology generated by the usual opens and by $\mathbb{Q}$. Every open has the form $U=V\cup (W\cap \mathbb{Q})$, where $V,W$ are usual open sets and we may arrange $V\subseteq W$. The topology is finer than the usual one, so the space is Hausdorff. Put $B=\mathrm{RO}(\mathbb{R})$, the complete Boolean algebra of ordinary regular open elements, and write $\rho (V)=\mathrm{int}\overline{V}$. Restriction from this space to its rational and irrational subspaces, followed by Booleanization, gives frame homomorphismsTo justify these formulas, each subspace has its ordinary subspace topology and is dense in the ordinary real line. Regular-open algebras of a space and a dense subspace are isomorphic: restrict a regular open and take its interior-closure, with inverse obtained by taking interior-closure in the ambient space. Restriction is a frame homomorphism, and double negation is a frame homomorphism into its fixed-element frame. These observations also show independence of the chosen representation of $U$. Since $V\subseteq W$, we have $f^{\ast }\le g^{\ast }$, but $f^{\ast }(\mathbb{Q})=0$ and $g^{\ast }(\mathbb{Q})=1$. Thus this Hausdorff space fails $T_U$ as a locale.

For the remaining arguments about connected locales, use the classical-logic option: positive opens of a locale are exactly the nonzero opens. There is a necessary positivity qualification. The empty locale has no positive opens, so the printed condition on those opens holds vacuously, although no point $1\to \varnothing$ exists. The point assertions therefore require $X$ to be positive. This qualification is automatic if “totally connected” includes nonemptiness; otherwise it must be added explicitly.

Let $X$ be positive and satisfy the condition on its positive opens of a locale. Put $F=\{a\in \mathcal{O}(X):a\ne 0\}$. It contains $1$, excludes $0$, and is upward closed. If $a,b\in F$ had $a\wedge b=0$, their union would be a positive open of a locale with a decomposition into two disjoint nonzero opens, contradicting its being a connected locale. Thus $a\wedge b\in F$. If ${\bigvee }_i{a}_i\ne 0$, not all $a_i$ can be zero; classical logic supplies a nonzero summand. Hence $F$ is a completely prime filter, and its characteristic frame homomorphism defines a point $p:1\to X$.

The point is dense. Indeed $p^{\ast }(a)=0$ implies $a=0$ by the definition of $F$. In nucleus language the image of $p$ has nucleus $p_{\ast }{p}^{\ast }$; its value at $0$ is $p_{\ast }(0)=0$, so the image is a dense sublocale.

Conversely suppose an open locale has a dense point $p$. Density means $p^{\ast }(a)=0$ only if $a=0$, and classically this implies $p^{\ast }(a)=1$ for every positive open of a locale. If a positive open $u$ split as $a\vee b=u$ with $a\wedge b=0$ and both summands nonzero, then $p^{\ast }(a)=p^{\ast }(b)=1$, contradicting preservation of their meet. Thus every positive open of a locale is a connected locale, proving the converse under the declared logical convention.

Let $x:X\to 1$ be the terminal map. For a positive totally connected locale $X$, the point above satisfiesbecause the right side is $1$ when $a\ne 0$ and both sides are $0$ otherwise. Hence $1_X\le px$. If $f:X\to Y$ and $Y$ is a totally unordered locale, composition gives $f\le fpx$, so $f=fpx$. Thereforewhich is the required constant factorization. For the empty source the factorization need not exist: the unique map $\varnothing \to \varnothing$ does not factor through $1$. Thus the positivity qualification matters for this assertion too.

For a Boolean algebra $B$, write $\downarrow b$ for its principal lattice ideal. The ideal frame of a Boolean algebra has intersections as meets and ideals generated by unions as joins. The pseudocomplement of an ideal $I$ isIn particular $(\downarrow b{)}^{\ast }=\downarrow \neg b$, so every principal ideal is complemented and regular.

If $B$ is complete, put $s={\bigvee }_{B}I$. Then $I^{\ast }=\downarrow \neg s$ and $I^{\ast \ast }=\downarrow s$. Thus all regular ideals are principal and complemented, so the corresponding locale is extremally disconnected.

Conversely, if the ideal frame of a Boolean algebra is extremally disconnected, each $I^{\ast \ast }$ is complemented. Any complemented ideal is principal: if $J\vee K=B$ and $J\cap K=\{0\}$, the fact that their generated join contains $1$ supplies $b\in J,c\in K$ with $b\vee c=1$. Then $b\wedge c=0$, so $c=\neg b$; every $j\in J$ is disjoint from $c$ and therefore $j\le b$. Thus $J=\downarrow b$. Write $I^{\ast \ast }=\downarrow s$. Since $I\subseteq I^{\ast \ast }$, $s$ bounds $I$. If $t$ is another upper bound, $I\subseteq \downarrow t$ implies $I^{\ast \ast }\subseteq (\downarrow t{)}^{\ast \ast }=\downarrow t$, so $s\le t$. An arbitrary subset has the same upper bounds as the lattice ideal it generates, so every subset of $B$ has a supremum. Hence

Now put $A=\mathcal{O}(X)$ and $B=A_{\neg \neg }$. This is a complete Boolean algebra, with arbitrary Boolean joins $\neg \neg {\bigvee }_A{b}_i$, so the preceding result makes $\gamma X$ extremally disconnected. We construct its map to $X$ using the permitted Joyal extension lemma.

The map $\sigma :\mathrm{Idl}(B)\to B$, $I\mapsto {\bigvee }_{B}I$, is a frame homomorphism, with right adjoint $b\mapsto \downarrow b$. Thus $k(I)=\downarrow {\bigvee }_{B}I$ is a nucleus on a frame whose fixed frame is $B$. It preserves finite joins: both $k(I\vee J)$ and $k(I)\vee k(J)$ equal $\downarrow ({\bigvee }_{B}I{\vee }_B{\bigvee }_{B}J)$, and $k(0)=0$. Consequently the locale with frame $B$ is a flat sublocale of $\gamma X$. It is also the Booleanization of a locale $X$, so it has its inclusion map to $X$.

The Joyal extension lemma says that a map from a flat sublocale to a compact locale that is a regular locale extends uniquely to the ambient locale. Apply it to this inclusion. Its frame formula giveswhere $u\prec a$ is the well-inside relation $\neg u\vee a=1$. This also proves directly that the map is surjective. Indeed $u\prec a$ implies $\neg \neg u\le a$: meet $\neg u\vee a=1$ with $\neg \neg u$. Every member of the ideal $g^{\ast }(a)$ is therefore at most $a$ in $A$, since a finite Boolean join of its generators is below $\neg \neg (u_1\vee \cdots \vee u_n)\le a$; the last inequality follows because $u_1\vee \cdots \vee u_n\prec a$. Regularity givesThus $a$ can be recovered from $g^{\ast }(a)$, so $g^{\ast }$ is injective. A locale map with injective inverse-image frame homomorphism is a surjection. We have obtained an extremally disconnected $\gamma X$ and a surjection $\gamma X\to X$.

A propositional geometric theory has primitive propositions and sequents between formulas built with finite conjunction and arbitrary set-indexed disjunction. Start with the free frame on the primitives, identify conjunction with meet and disjunction with join, and impose each sequent as an inequality. The resulting quotient frame is $\mathcal{O}(X_T)$. In the sheaf topos $\mathrm{Sh}(X_T)$, interpret each primitive as the subterminal sheaf corresponding to its generating open. Operations on these subterminal sheaves are precisely the frame operations, so every imposed sequent is valid. This constructs the canonical model.

For a commutative ring $R$, denote the generator attached to $r$ by $U_r$. The presentation impliesThe product equality uses the multiplication implication in one direction and both factor implications in the other; the latter follow by commuting $r,s$. A ring homomorphism $\phi :R\to S$ sends these relations to the corresponding ones in $S$. It therefore gives a frame homomorphism $U_r\mapsto U_{\phi (r)}$ and hence a map $X_S\to X_R$ of locales.

If $ar+bs=1$, thenso the two opens cover. Conversely let $S=R/(r,s)$ and pull back a putative cover along $X_S\to X_R$. Both generators become $U_0$, so $1=0$ in $\mathcal{O}(X_S)$. The allowed degeneracy criterion gives $0=1$ in $S$, equivalently $1\in (r,s)$. ThusThis necessity argument never selects a prime ideal.

Finite intersections of the generating opens are again generators, so they form a basis. Assign $R[r^{-1}]$ to $U_r$. The localization of a ring carries its ordinary addition and multiplication of fractions; equality of $a/r^n$ and $b/r^m$ means that some power of $r$ annihilates the cross-multiplied difference. On $U_r\cap U_s=U_{rs}$, restriction is further localization.

We also justify restriction for any inclusion of basic opens. Adding the condition $U_t=1$ to the presentation of $X_R$ gives the open $U_t$ and the presentation of $X_{R[t^{-1}]}$: the generator for $a/t^n$ corresponds to $U_a\wedge U_t$. This is well-defined since equality of fractions, after multiplication by a power of the now-invertible $t$, makes the two membership propositions equivalent. More explicitly, $U_t=1$ implies $U_{t^{k}z}=U_z$. If $t^{k}z=0$, this gives $U_z=0$. If $x-y$ is killed by a power of $t$, then $U_{x-y}=U_{y-x}=0$ (since $U_{-1}=1$), and the additive inequalities for $x=y+(x-y)$ and $y=x+(y-x)$ give $U_x=U_y$. A zero element in the localized ring has false membership, multiplication gives intersections, and the additive relation follows by clearing denominators. The reverse assignment on $a\in R$ proves that these maps are inverse. Thus $X_{R[t^{-1}]}\cong U_t$. If $U_t\subseteq U_r$, then in this localized theory $U_r=1$. Apply the quotient argument above, with the second generator $0$, to conclude $1\in (r)$ in $R[t^{-1}]$. Therefore $r$ is invertible there, and the universal property of localization gives the restriction $R[r^{-1}]\to R[t^{-1}]$. These restrictions compose uniquely.

It remains to glue, and the allowed basis criterion reduces this to a whole-locale cover $U_r\vee U_s=1$. Let $\alpha \in R[r^{-1}]$ and $\beta \in R[s^{-1}]$ have equal restrictions to $R[(rs{)}^{-1}]$. Choose a common initial exponent $n$, writing $\alpha =a/r^n$, $\beta =b/s^n$. Equality on the overlap supplies $k\ge 0$ withSet $N=n+k$, $A=r^{k}a$ and $B=s^{k}b$. Thenwith the last equality in $R$ itself. This clearing step is necessary when the commutative ring has zero divisors.

Since $(r,s)=R$, also $(r^N,s^N)=R$. Choose $\lambda r+\mu s=1$. For $N\ge 1$, expand $(\lambda r+\mu s{)}^{2N-1}=1$; each term contains either $r^N$ or $s^N$, producing $C,D\in R$ with $C{r}^N+D{s}^N=1$. For $N=0$ choose $C=1,D=0$. DefineIn $R[r^{-1}]$,and similarly in $R[s^{-1}]$,Thus $t$ glues the matching pair. If $t^{\prime }$ is another gluing, some $r^p$ and $s^q$ annihilate $t-t^{\prime }$. The same binomial argument gives $(r^p,s^q)=R$, so $t-t^{\prime }=0$. This proves uniqueness without cancellation or a domain assumption.

The exactness of the unit-ideal localization Čech complex proves the sheaf axiom for the required basic covers, and hence the assignment with its restrictions defines a sheaf of rings $\tilde{R}$ with $\tilde{R}(U_r)=R[r^{-1}]$. On the empty basic open, localization is the zero ring, whose underlying set has one section, as required. The construction and proof remain valid for the zero ring.

For an adjunction $L:\mathcal{C}\rightleftarrows \mathcal{D}:R$, write its adjunction unit as $\eta$ and its adjunction counit as $\epsilon$. It is an idempotent adjunction when the induced monad has invertible multiplication $\mu =R\epsilon L:RLRL\Rightarrow RL$. The dual condition is invertibility of the induced comonad comultiplication $\delta =L\eta R:LR\Rightarrow LRLR$.

To prove equivalence of these conditions, suppose $\mu$ is invertible. The two unit identities imply $T\eta =\eta T={\mu }^{-1}$, where $T=RL$. For any algebra for a monad $a:TA\to A$, naturality giveswhile $a{\eta }_A=1_A$. Thus ${\eta }_A$ is invertible. For each $D\in \mathcal{D}$, the arrow $R{\epsilon }_D:T(RD)\to RD$ is a monad algebra action, so ${\eta }_{RD}$ is invertible. Applying $L$ proves ${\delta }_D=L{\eta }_{RD}$ invertible. Apply this implication to the opposite adjunction, interchanging the roles of the monad and comonad, to obtain the converse. Therefore idempotence is self-dual.

The open-set frame $O(X)$ is ordered by inclusion. Its arbitrary joins are unions; arbitrary meets are interiors of intersections. Finite intersections are already open, so finite meets are ordinary intersections, including the empty meet $X$. Distributivity of intersection over arbitrary unions proves the frame law. If $f:X\to Y$ is a continuous map, inverse imagepreserves arbitrary unions and finite intersections, including $\varnothing$ and the entire space. It is therefore a frame homomorphism. Since $(gf{)}^{-1}=f^{-1}{g}^{-1}$ and $1_X^{-1}=1_{O(X)}$, this defines $O:\mathbf{Top}\to {\mathbf{Frm}}^{\mathrm{op}}$.

Let $2=\{0<1\}$ and let $P(A)$ be the set of points of a frame $A$, namely frame homomorphisms $A\to 2$. For $a\in A$, put $U_a=\{p:p(a)=1\}$. Preservation of joins and finite meets givesIn the last equality, a join in $2$ is $1$ precisely when at least one summand is $1$, also covering the empty family. Thus the sets $U_a$ are all the opens of a topology, rather than merely a proposed basis.

For a frame homomorphism $h:A\to B$, define $P(h):P(B)\to P(A)$ by $p\mapsto p\circ h$. Since $P(h{)}^{-1}(U_a)=U_{h(a)}$, it is continuous. Composition and identities follow from composition of functions, giving $P:{\mathbf{Frm}}^{\mathrm{op}}\to \mathbf{Top}$.

The frame-point adjunction is the natural bijectionA continuous map $f:X\to P(A)$ determines $h_f(a)=f^{-1}(U_a)$; the displayed identities for $U_a$ show that $h_f$ is a frame homomorphism. Conversely a frame homomorphism $h:A\to O(X)$ determines $f_h(x)(a)=1$ exactly when $x\in h(a)$. Membership in unions and finite intersections proves that $f_h(x)$ is a frame homomorphism to $2$, and $f_h^{-1}(U_a)=h(a)$ proves continuity. These constructions are inverse. Precomposing in $X$ becomes inverse image of open sets; precomposing a frame homomorphism becomes composition of frame points. Hence the bijection is natural in both arguments and proves $O⊣P$.

The adjunction unit isThe adjunction counit at $A$, regarded as an arrow of ${\mathbf{Frm}}^{\mathrm{op}}$, is represented by the frame homomorphism $e_A:A\to O(P(A))$, $a\mapsto U_a$. It is surjective because every open of $P(A)$ is of this form. We can compute $P(e_A):P(O(P(A)))\to P(A)$ explicitly: it sends $q$ to $p=q\circ e_A$. For every open $U_a$ of $P(A)$,Thus ${\eta }_{P(A)}P(e_A)=1$. Conversely, evaluation at $p$ sends $U_a$ to $p(a)$, so $P(e_A){\eta }_{P(A)}=1$. Both maps are continuous by their definitions. Therefore $P(e_A)$ is a homeomorphism. The multiplication of the induced monad $PO$ at $X$ is $P(e_{O(X)})$, which is invertible by this calculation. Consequently the frame-point adjunction is idempotent. This does not assert that every ${\eta }_X$ is a homeomorphism: it says that applying the point-space construction a second time makes no further change.