= Joyal extension lemma
{c}
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 is
$$
g^*(a)=\bigvee_{u\prec a}^{\mathcal O(A)}f^*(u),
$$
where 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^*$ preserves arbitrary joins and finite meets.
Back to article page
