= Solution
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,
$$
\operatorname{PFrm}(P\#Q,R)\cong\{\beta:P\times Q\to R:\beta\text{ preserves finite meets and directed joins separately}\}.
$$
In particular $1\#q=p\#1=1$. The tensor unit is the free <preframe> on one generator: classically it is $\mathbf2$, 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*y=x\vee y$ and unit $0$. Binary <join> preserves finite meets and directed joins separately. Conversely take a commutative <monoid object> $(M,*,e)$ in <preframes> and put
$$
R(M)=\{x\in M:e\leq x,\ x*x=x\}.
$$
This set contains $e$ and $1$, since preservation of the empty <meet> gives $1*x=1$. If $x,y\in R(M)$, then $x*y\geq x,y$, and
$$
(x\wedge y)*(x\wedge y)=(x*x)\wedge(x*y)\wedge(y*x)\wedge(y*y)=x\wedge y.
$$
Thus finite meets are inherited. If $D\subseteq R(M)$ is nonempty and directed, separate preservation of directed joins gives
$$
\left(\bigvee D\right)*\left(\bigvee D\right)=\bigvee_{d,d'\in D}d*d'=\bigvee D,
$$
because a common upper bound $t\in D$ gives $d*d'\leq t*t=t$. Directed joins are inherited too. Associativity and commutativity show that $x*y$ is <idempotent>; it is the least <idempotent> upper bound of $x,y$. Therefore $e$ is the bottom and $*$ is binary <join> on $R(M)$. Arbitrary joins are directed joins of finite products, including the empty product $e$. Finally
$$
(x\wedge y)*(x\wedge z)=(x*x)\wedge(x*z)\wedge(y*x)\wedge(y*z)=x\wedge(y*z),
$$
so 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>: \b[$\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)*g(y)$. For two <frames> $L,K$, the induced multiplication on pure generators is
$$
(a\#b)*(a'\#b')=(a\vee a')\#(b\vee b'),\qquad e=0\#0.
$$
Every 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. Consequently
$$
\boxed{L\amalg_{\mathbf{Frm}}K=L\#_{\mathbf{PFrm}}K,\qquad a\#b=i_L(a)\vee i_K(b).}
$$
Rectangles 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 \b[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$ with
$$
q(a\#b)=[a=1]\vee[b=1].
$$
It reflects top on every pure generator. The property $q(x)=1\Longrightarrow 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$
$$
q_j(a)=[\text{there is an arrow }j\to k\text{ for which }a\text{ becomes }1\text{ at stage }k].
$$
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 gives
$$
\boxed{\prod_{i\in I}X_i\text{ is compact whenever every }X_i\text{ is compact}.}
$$
This proves the <localic Tychonoff theorem> through <preframes>, without choosing points or invoking the <axiom of choice>.
Back to article page
