5.3 Specifications
An atom condition is a pair \( (s, t) \) where \( s, t : \operatorname {\mathsf{Set}}\kappa \). A \( \beta \)-near-litter condition is either
a flexible condition, consisting of a set \( s : \operatorname {\mathsf{Set}}\kappa \); or
an inflexible condition, consisting of an inflexible \( \beta \)-path \( I = (\gamma ,\delta ,\varepsilon ,A) \), a \( \delta \)-coding function \( \chi \), and two \( \delta \)-trees \( R^{\mathcal A}, R^{\mathcal N}\) of relations on \( \kappa \).
A \( \beta \)-specification is a pair \( (\sigma ^{\mathcal A}, \sigma ^{\mathcal N}) \) where
\( \sigma ^{\mathcal A}\) is a \( \beta \)-tree of enumerations of atom conditions; and
\( \sigma ^{\mathcal N}\) is a \( \beta \)-tree of enumerations of \( \beta \)-near-litter conditions.
Let \( S \) be a \( \beta \)-support. Then its specification is the \( \beta \)-specification \( \sigma = \operatorname {\mathsf{spec}}(S) \) given by the following constructors.
Whenever \( (i, a) \in S_A^{\mathcal A}\), we have \( (i, (s, t)) \in \sigma _A^{\mathcal A}\) where
\[ s = \{ j : \kappa \mid (j, a) \in S_A^{\mathcal A}\} ;\quad t = \{ j : \kappa \mid \exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a \in N \} \]Whenever \( (i, N) \in S_A^{\mathcal N}\) and \( N^\circ \) is \( A \)-flexible, we have \( (i, c) \in \sigma _A^{\mathcal N}\) where \( c \) is the flexible condition given by
\[ s = \{ j : \kappa \mid \exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N^\circ = {N’}^\circ \} \]Whenever \( I = (\gamma ,\delta ,\varepsilon ,A) \) is an inflexible \( \beta \)-path, \( t : \mathsf{Tang}_\delta \), and \( (i, N) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) is such that \( N^\circ = f_{\delta ,\varepsilon }(t) \), we have \( (i, c) \in \sigma _{{A_\varepsilon }_\bot }^{\mathcal N}\) where \( c \) is the inflexible condition given by path \( I \) and coding function \( \chi _t \), and \( R^{\mathcal A}\) and \( R^{\mathcal N}\) are the \( \delta \)-trees of relations given by the constructors
\begin{align*} & \forall i,\, \forall j,\, \forall a,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\to (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\to (i, j) \in R_B^{\mathcal A}\\ & \forall i,\, \forall j,\, \forall N,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\to (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}\to (i, j) \in R_B^{\mathcal N}\end{align*}
Let \( S, T \) be \( \beta \)-supports. Then \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \) if and only if 1
\( \operatorname {\mathsf{coim}}S_A^{\mathcal A}= \operatorname {\mathsf{coim}}T_A^{\mathcal A}\) and \( \operatorname {\mathsf{coim}}S_A^{\mathcal N}= \operatorname {\mathsf{coim}}T_A^{\mathcal N}\).
(atom condition) Whenever \( (i, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2) \in T_A^{\mathcal A}\), we have
\[ \forall j,\, (j, a_1) \in S_A^{\mathcal A}\leftrightarrow (j, a_2) \in T_A^{\mathcal A} \]and
\[ \forall j,\, (\exists N,\, (j, N) \in S_A^{\mathcal N}\wedge a_1 \in N) \leftrightarrow (\exists N,\, (j, N) \in T_A^{\mathcal N}\wedge a_2 \in N) \](flexible condition) Whenever \( (i, N_1) \in S_A^{\mathcal N}\) and \( (i, N_2) \in T_A^{\mathcal N}\), if \( N_1^\circ \) is \( A \)-flexible, then so is \( N_2^\circ \), and
\[ \forall j,\, (\exists N',\, (j, N') \in S_A^{\mathcal N}\wedge N_1^\circ = {N’}^\circ ) \leftrightarrow (\exists N',\, (j, N') \in T_A^{\mathcal N}\wedge N_2^\circ = {N’}^\circ ) \](inflexible condition) Let \( I = (\gamma ,\delta ,\varepsilon ) \) be an inflexible \( \beta \)-path and let \( t : \mathsf{Tang}_\delta \). Then whenever \( (i, N_1) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) and \( (i, N_2) \in T_{{A_\varepsilon }_\bot }^{\mathcal N}\) are such that \( N_1^\circ = f_{\delta ,\varepsilon }(t) \), there is some \( \delta \)-allowable permutation \( \rho \) such that \( N_2^\circ = f_{\delta ,\varepsilon }(\rho (t)) \), and
\begin{align*} \forall j,\, \forall a,\, (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}& \to \forall i,\, (i, a) \in S_{{A_\delta }_B}^{\mathcal A}\leftrightarrow (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\\ \forall j,\, \forall N,\, (j, N) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal N}& \to \forall i,\, (i, N) \in S_{{A_\delta }_B}^{\mathcal N}\leftrightarrow (i, \rho _B(N)) \in T_{{A_\delta }_B}^{\mathcal N}\end{align*}
We will only sketch the fourth bullet point of this proof; the remainder is direct (but quite long to write down on paper). Moreover, we will show this for atoms; the result for near-litters is identical. The specifications \( \operatorname {\mathsf{spec}}(S) \) and \( \operatorname {\mathsf{spec}}(T) \) give rise to the same trees \( R^{\mathcal A}\) precisely when
We must show that this holds if and only if
This can be concluded by appealing to the basic behaviour of \( \rho \) and noting the coinjectivity of \( \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\).
Let \( \rho \) be \( \beta \)-allowable, and let \( S \) be a \( \beta \)-support. Then \( \operatorname {\mathsf{spec}}(\rho (S)) = \operatorname {\mathsf{spec}}(S) \).
We appeal to proposition 5.12. Clearly the coimage condition holds.
For the atom condition, we must check that if \( (i, a) \in S_A^{\mathcal A}\), we have
and
both of which are trivial.
For the flexible condition, we must check that if \( (i, N) \in S_A^{\mathcal N}\) and \( N^\circ \) is \( A \)-flexible, then \( \rho _A(N)^\circ \) is also \( A \)-flexible (which is direct, and should already be its own lemma), and that
which is similarly trivial.
Finally, for the inflexible condition, suppose that \( I = (\gamma ,\delta ,\varepsilon ) \) is an inflexible \( \beta \)-path and \( t : \mathsf{Tang}_\delta \). Let \( (i, N) \in S_{{A_\varepsilon }_\bot }^{\mathcal N}\) be such that \( N^\circ = f_{\delta ,\varepsilon }(t) \). Then by the coherence condition,
We must check that
which again is trivial.
Let \( S \) and \( T \) be base supports. We define the relations \( \operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}\) by the constructors 2
Note that \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal A}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal A}\) and \( {\operatorname {\mathsf{conv}}_{S,T}^{\mathcal N}}^{-1} = \operatorname {\mathsf{conv}}_{T,S}^{\mathcal N}\).
Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is one-to-one.
If \( (a_1, a_2), (a_1, a_3) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\), then there are \( i, j \) such that \( (i, a_1), (j, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2), (j, a_3) \in T_A^{\mathcal A}\). By proposition 5.12, we deduce \( (j, a_1) \in S_A^{\mathcal A}\leftrightarrow (j, a_2) \in T_A^{\mathcal A}\), so by coinjectivity of \( T_A^{\mathcal A}\), we deduce \( a_2 = a_3 \). Hence \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is coinjective. By symmetry, \( \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) is one-to-one.
Let \( S, T \) be supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\) and \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( a_1 \in N_1 \) if and only if \( a_2 \in N_2 \).
As \( (a_1, a_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}\), there is \( i \) such that \( (i, a_1) \in S_A^{\mathcal A}\) and \( (i, a_2) \in T_A^{\mathcal A}\), and as \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), there is \( j \) such that \( (j, N_1) \in S_A^{\mathcal N}\) and \( (j, N_2) \in T_A^{\mathcal N}\). By proposition 5.12, we deduce that
If \( a_1 \in N_1 \), then as \( (j, N_1) \in S_A^{\mathcal N}\), we deduce that there is a near-litter \( N' \) such that \( (j, N') \in T_A^{\mathcal N}\) and \( a \in N' \). But \( T_A^{\mathcal N}\) is coinjective, so \( N' = N_2 \), giving \( a \in N_2 \). The converse holds by symmetry.
Let \( S, T \) be supports such that \( T \) is strong and \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). If \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\), then \( N_1^\circ = N_2^\circ \) if and only if \( N_3^\circ = N_4^\circ \).
There are \( i, j \) such that \( (i, N_1), (j, N_2) \in S_A^{\mathcal N}\) and \( (i, N_3), (j, N_4) \in T_A^{\mathcal N}\). Suppose that \( N_1^\circ = N_2^\circ \); we show that \( N_3^\circ = N_4^\circ \).
First, suppose that \( N_1^\circ \) is \( A \)-flexible. Then by proposition 5.12, we have
So as \( (j, N_2) \in S_A^{\mathcal N}\) and \( N_1^\circ = N_2^\circ \), there is \( N' \) with \( (j, N') \in T_A^{\mathcal N}\) and \( N_3^\circ = {N’}^\circ \), but clearly \( N' = N_4 \), giving the result.
Now suppose that \( N_1^\circ \) is \( A \)-inflexible, so there is an inflexible \( \beta \)-path \( (\gamma ,\delta ,\varepsilon ,B) \) and tangle \( t : \mathsf{Tang}_\delta \) such that
Then by proposition 5.12, there is some \( \delta \)-allowable \( \rho \) such that \( N_3^\circ = f_{\delta ,\varepsilon }(\rho (t)) \) and
But as \( N_1^\circ = N_2^\circ \), we draw the same conclusion about \( N_2 \) and \( N_4 \), giving a \( \delta \)-allowable permutation \( \rho ' \) such that \( N_4^\circ = f_{\delta ,\varepsilon }(\rho '(t)) \); note that the inflexible path and tangle in question will be the same for both pairs. We also have
Combining these, we obtain
We claim that \( \rho (\operatorname {\mathsf{supp}}(t)) = \rho '(\operatorname {\mathsf{supp}}(t)) \). As \( T \) is strong, for each atom \( a \) such that \( (j, a) \in \operatorname {\mathsf{supp}}(t)_B^{\mathcal A}\), there is some \( k \) such that \( (i, \rho _B(a)) \in T_{{A_\delta }_B}^{\mathcal A}\). Thus \( \rho _B(a) = \rho '_B(a) \). The same conclusion may be drawn for near-litters. Thus \( \rho (\operatorname {\mathsf{supp}}(t)) = \rho '(\operatorname {\mathsf{supp}}(t)) \), giving \( \rho (t) = \rho '(t) \), and hence \( N_3^\circ = N_4^\circ \).
Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( (N_1, N_3), (N_2, N_4) \in \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}\),
As \( S \) is strong, we have \( \operatorname {\mathsf{interf}}(N_1, N_2) \subseteq \operatorname {\mathsf{im}}S_A^{\mathcal A}\). But \( \operatorname {\mathsf{coim}}\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}= \operatorname {\mathsf{im}}S_A^{\mathcal A}\), as required. 3 The result for \( \operatorname {\mathsf{interf}}(N_3, N_4) \) then follows by symmetry.
Let \( S, T \) be strong \( \beta \)-supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then for each \( A \), we define the base action \( \operatorname {\mathsf{conv}}_{S_A, T_A} \) to be \( (\operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal A}, \operatorname {\mathsf{conv}}_{S_A, T_A}^{\mathcal N}) \); this is a base action by ??. We now define the \( \beta \)-action \( \operatorname {\mathsf{conv}}_{S,T} \) by \( (\operatorname {\mathsf{conv}}_{S,T})_A = \operatorname {\mathsf{conv}}_{S_A,T_A} \).
Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then \( \operatorname {\mathsf{conv}}_{S,T} \) is coherent.
Suppose that \( (N_1, N_2) \in \operatorname {\mathsf{conv}}_{S_A,T_A}^{\mathcal N}\), so there is \( i \) such that \( (i, N_1) \in S_A^{\mathcal N}\) and \( (i, N_2) \in T_A^{\mathcal N}\).
Suppose that \( N_1^\circ \) is \( A \)-flexible. By proposition 5.12, we immediately conclude that \( N_2^\circ \) is \( A \)-flexible as required.
Now suppose that \( N_1^\circ \) is \( A \)-inflexible with inflexible \( \beta \)-path \( I = (\gamma ,\delta ,\varepsilon ,B) \) and tangle \( t : \mathsf{Tang}_\delta \). By proposition 5.12, there is some \( \delta \)-allowable permutation \( \rho \) such that \( N_2^\circ = f_{\delta ,\varepsilon }(\rho (t)) \) and
We must show that \( ((\operatorname {\mathsf{conv}}_{S,T})_B)_\delta (\operatorname {\mathsf{supp}}(t)) = \rho (\operatorname {\mathsf{supp}}(t)) \). We will show the result for atoms; the result for near-litters is identical. Let \( (j, a) \in \operatorname {\mathsf{supp}}(t)_C^{\mathcal A}\). Then as \( S \) is strong, there is \( k \) such that \( (k, a) \in S_{{B_\delta }_C}^{\mathcal A}\). Then by the equation above, \( (k, \rho _C(a)) \in T_{{B_\delta }_C}^{\mathcal A}\). Hence \( (a, \rho _C(a)) \in (((\operatorname {\mathsf{conv}}_{S,T})_B)_\delta )_C \) as required.
Let \( S, T \) be strong supports such that \( \operatorname {\mathsf{spec}}(S) = \operatorname {\mathsf{spec}}(T) \). Then there is an allowable permutation \( \rho \) such that \( \rho (S) = T \).
By proposition 5.20, we may apply theorem 4.38 to \( \operatorname {\mathsf{conv}}_{S,T} \) to obtain an allowable permutation \( \rho \) that \( \operatorname {\mathsf{conv}}_{S,T} \) approximates, which directly gives \( \rho (S) = T \) as required.