Complete Heyting algebra

A frame is a complete lattice in which finite meets distribute over arbitrary joins:

A subframe is a subset of a frame closed under arbitrary ambient joins and finite ambient meets, including $0$ and $1$. The inclusion is a frame homomorphism. In contrast, the fixed elements of a nucleus on a frame usually need their own regularized joins and are not a subframe.

An upward-closed subset of a frame containing $1$, excluding $0$ and closed under finite meets is completely prime if membership of an arbitrary join implies membership of some summand. Its characteristic map is a point of a frame. Constructively the map takes values in the frame of truth values.

A preframe is a partially ordered set with finite meets and nonempty directed joins, with finite meets distributing over directed joins. Its homomorphisms preserve these operations. Forgetting the arbitrary joins of a frame leaves a preframe.

The tensor represents maps $P\times Q\to R$ preserving finite meets and directed joins in each variable separately. Its pure generators $p\#q$ satisfy the corresponding relations in each variable. The unit is the free preframe on one generator, the bottom of the frame of truth values. For frames, this tensor is their coproduct, with $p\#q=i(p)\vee j(q)$; it must not be confused with the rectangle $i(p)\wedge j(q)$.

For a commutative monoid object $(M,\ast ,e)$ in preframes, the indicated subset is a frame. Its bottom is $e$, its binary join is $\ast$, and its directed joins and finite meets are inherited. Every homomorphism from a frame regarded as a join monoid factors uniquely through this subset. This gives a coreflective subcategory.

A nucleus is an inflationary, idempotent, finite-meet-preserving map on a frame. Its fixed elements form a frame, whose joins are obtained by applying $j$ to ambient joins. The induced locale is a sublocale. The nuclei on a frame themselves form a frame in pointwise order; their meets are pointwise, but their joins usually are not.

For a frame homomorphism $h:B\to A$, nuclei are equivalent when their restrictions to $h(B)$ agree. The least representative of the class of $j$ isThe least representatives form a frame generated by $c(A)$ and $o(h(B))$. To see minimality, each summand is below $j$ and its value at $hb$ is $j(hb)$; any equivalent nucleus therefore bounds every summand. This construction gives the pushout of $B\to N(B)$ along $h$.

This nucleus on a frame determines the closed sublocale complementary to the open determined by $a$. It is the least nucleus on a frame taking $0$ to $a$. In the frame of nuclei on a frame, $c(a)$ and the open nucleus $o(a)$ are complements.

The Heyting implication defines a nucleus on a frame whose sublocale is the open determined by $a$. It is the least nucleus on a frame sending $a$ to $1$.

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.

Under classical logic a positive locale is connected when it cannot be written as the union of two disjoint nonzero opens. Equivalently its only complemented opens are $0$ and $1$. An open sublocale uses this criterion relative to its own top element. Positivity of the whole locale excludes the empty locale. This definition is stated with its logical convention; replacing positivity by negated nonemptiness is not a constructive step.

This relation says that the closure of the open $u$ is contained in $v$. A regular locale has $a={\bigvee }_{u\prec a}u$ for every $a$. If $u\prec a$, then $\neg \neg u\le a$ and $\neg \neg u\prec a$.

A locale is regular when every open is the join of opens well inside it. This expresses regularity without reference to points.

A locale is extremally disconnected when the closure of every open is open. Equivalently its regular open elements are complemented, or double negation preserves binary joins, or its Booleanization of a locale is a flat sublocale.

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.

An open, or overt, locale has a positivity map $\mathrm{Pos}:\mathcal{O}(X)\to \Omega$ left adjoint to the scalar inverse image ${!}^{\ast }:\Omega \to \mathcal{O}(X)$, satisfying Frobenius reciprocity. Thus $a\le {!}^{\ast }\mathrm{Pos}(a)$ and positivity preserves arbitrary joins. Classically every locale is overt, with positivity meaning $a\ne 0$.

A positive open locale is totally connected when every positive open of a locale is connected. Under classical logic its positive opens form a completely prime filter, hence specify a dense point. Positivity of the whole locale is essential: the empty locale satisfies the condition on positive opens vacuously but has no point.

An open is positive when its positivity truth value holds. Positivity gives a constructive witness of inhabitedness and must not be replaced by double-negated nonemptiness.

A locale is totally unordered when $f^{\ast }\le g^{\ast }$ for two maps into it implies $f=g$, for every common domain. This tests generalized points rather than just ordinary points. Every Hausdorff locale has this property: comparable maps annihilate the complement of the diagonal and hence factor through the diagonal.

A locale is Hausdorff when its diagonal into its localic square is a closed sublocale. Its complement is the join of rectangles $a\times b$ with $a\wedge b=0$. This is stronger than the underlying space being a Hausdorff space, because the localic square need not be spatial.

A locale is compact when every directed family of opens whose join is $1$ contains $1$. Equivalently every open cover has a finite subcover. The truth-valued test $a\mapsto [a=1]$ is a preframe homomorphism exactly when the locale is compact.

An arbitrary product of compact locales is compact. Finite products correspond to preframe tensor products, whose compactness follows by tensoring the top tests. An arbitrary product is obtained by the filtered colimit of finite frame coproducts; the eventual-top test proves that filtered colimits preserve compactness. No choice of points is required.

A sublocale is determined by a nucleus on a frame $j$ on $\mathcal{O}(X)$. Its frame consists of the fixed elements of $j$, with inherited meets and regularized joins. Increasing the nucleus makes the sublocale smaller.

The double-negation nucleus on a frame gives a dense sublocale whose frame is a complete Boolean algebra. Its elements are regular open elements, with Boolean joins $\neg \neg {\bigvee }_i{a}_i$.

A sublocale is flat when its nucleus on a frame preserves finite joins, including $0$. Equivalently its fixed elements are closed under ambient finite joins. In particular every flat sublocale is a dense sublocale.

Every map from a flat sublocale $A_j$ of $A$ to a compact locale that is also a regular locale extends uniquely to $A$. On frames the extension iswhere the terms are first regarded as fixed elements in the ambient frame. Regularity proves agreement after applying $j$; compactness reduces arbitrary covers to finite subcovers on a well-inside open, and flatness identifies those finite joins with ambient joins. These facts prove that $g^{\ast }$ preserves arbitrary joins and finite meets.

A sublocale is dense when its closure is the whole locale. For a map $f$, its image is dense when $f^{\ast }(a)=0$ implies $a=0$. Classically, a dense point belongs to every nonzero open.

The closed nucleus $c(a)$ determines the complement of the open $a$. A sublocale with nucleus $j$ is dense precisely when $j(0)=0$, since its closure is the closed sublocale defined by $j(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.

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.

A point is a frame homomorphism to the two-element frame $2=\{0<1\}$. Its inverse image of $1$ is a completely prime filter: membership of an arbitrary join forces membership of one term. The point space $P(A)$ has opens $U_a=\{p:p(a)=1\}$. Indeed $U_{a\wedge b}=U_a\cap U_b$ and $U_{{\bigvee }_i{a}_i}={\bigcup }_i{U}_{a_i}$, so these sets already form a topology.

A map between frames preserving every join and every finite meet, including the empty join $0$ and empty meet $1$. Such a map is automatically order-preserving. Inverse image under a continuous map is an example.

For a frame $L$, an $L$-valued matrix $f:A⇝B$ is a function $A\times B\to L$. Composition is matrix multiplication with join as addition and meet as multiplication.