Extension of finite partial prime-ideal diagrams

The finitely many atoms of $A$ have join $1$. At least one has $e$-value $1$, since $e(1)=1$; at most one does, since distinct atoms have meet $0$ whereas two value-$1$ atoms would have meet of value $1$. Let $a$ be this unique atom.

The atoms of $C$ below $a$ have join $a$: intersect the atomic decomposition of $1_C$ with $a$. Because $a\mathrm{\ne }0$, at least one such $C$-atom $c$ is nonzero. This chooses one element from one finite nonempty set, not a choice function on a family.

Define $e^{\mathrm{\prime }}(x)=1$ exactly when $c\le x$. Since $c$ is an atom, it lies below exactly one of $x,\mathrm{\neg }x$, and $c\le x\wedge y$ exactly when both $c\le x$ and $c\le y$; hence $e^{\mathrm{\prime }}$ preserves $0,1,\mathrm{\neg },\wedge$, and therefore $\vee$. Thus $e^{\mathrm{\prime }}:C\to \mathbf{2}$ is a Boolean homomorphism.

For $x\in A$, the selected $A$-atom $a$ lies below exactly one of $x,\mathrm{\neg }x$, and $c\le a$. If $e(x)=1$, uniqueness in step 1.1 forces $a\le x$, hence $e^{\mathrm{\prime }}(x)=1$; if $e(x)=0$, then $e(\mathrm{\neg }x)=1$, so $a\le \mathrm{\neg }x$ and $e^{\mathrm{\prime }}(x)=0$. Therefore $e^{\mathrm{\prime }}\mathrm{\mid }A=e$.

Given a finite $F\subseteq B$, take $C=⟨A\cup F⟩$. The cell description makes $C$ finite, step 4.1 extends the original diagram to $C$, and its domain contains $F$; this is precisely extension across $F$. It is not called a diagram deciding $F$, because the preceding definition reserves that phrase for a diagram whose domain is exactly $⟨F⟩$.