 Joyal extension lemma

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.