Relative nucleus assembly (source code)

= Relative nucleus assembly
{title2=$N_B(A)$}

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$ is
$$
r_h(j)=\bigvee_{b\in B}\bigl(o(hb)\wedge c(j(hb))\bigr).
$$
The 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$.