A basis for a vector space is exactly (the data for) an isomorphism with ℝ^{N}, where N is the dimension of the space. It is not important for the analogy that the field of scalars be ℝ, or that the dimension be finite. The significance of ℝ^{N} is that it carries a standard structure (in which the nth basis vector has a 1 in the nth coordinate and 0 elsewhere), which is transferred by the isomorphism to the chosen structure on the space under study. The standard object in our case is the object Σ^{N} (or the corresponding algebra Σ^{ΣN}), for which Axiom 4.10 defined a basis.
Bases for lattices are actually more like spanning sets than (linearly independent) bases for vector spaces, since we may add unions of members to the basis as we please, as we do in Lemma 8.4 below. Consequently, instead of isomorphisms with the standard structure, we have Σsplit embeddings X↣Σ^{N}. We shall see that these embeddings capture several well known constructions involving ℝ and locally compact objects.
Definition 7.1 i:X↣ Y is a Σsplit subobject
if (it is the equaliser of some pair [B] and)
there is a map I:Σ^{X}→Σ^{Y} such that
Σ^{i}· I=id_{ΣX}.
Using Notation 5.13, we write
The effect of this is that X carries the subspace topology inherited from Y, in a canonical way: for an open subobject φ of X, it provides a particular open subobject Iφ of Y for which the restriction Σ^{i}(Iφ) is φ.
In the case where X is an open subobject of Y (Lemma 3.8), Iφ≡∃_{i}φ is the least such extension, whilst for a closed subobject, Iφ≡∀_{i}φ is the greatest one, but in general it need not be either of these.
The computational significance of Σsplit embeddings is that any observation (computation of type Σ) on the subobject extends canonically, though not uniquely, to the whole object.
Warning 7.2 Let Y⇉ Z be a parallel pair of continuous functions
between locally compact sober spaces
and X≡{y:Y ∣ f y=g y:Z} the subset of points that satisfy
the equation.
We give X the subspace topology,
i.e. its open subspaces are the restrictions of those of Y.
This is the equaliser X↣ Y⇉ Z
in the category of sober topological spaces,
but X need not be locally compact (or have an effective basis).
Equalisers also exist in the category of locales,
but again need not be locally compact, or even spatial.
Σsplit subspaces are therefore a very special case.
Remark 7.3 For this reason,
the formulation of ASD that we gave in Axiom 3.3(c)
does not provide general equalisers.
It formally adjoins
(Section B 4) a Σsplit subobject i:X≡{Y ∣ E}↣ Y of Y
with I:Σ^{X}◁Σ^{Y}
such that Σ^{i}· I=id_{ΣX} and I·Σ^{i}=E,
given any endomorphism E:Σ^{Y}→Σ^{Y}
that satisfies the appropriate equation.
We shall consider the formulation of this equation
in Section 10.
The λcalculus developed in
Section B 8 allows arbitrarily complicated combinations of Σsplit subobjects
and exponentials,
but in this section and the next we reduce them to
Σsplit subobjects of Σ^{N}.
The following results link three (d–f) of the abstract characterisations of local compactness in the Introduction.
Lemma 7.4 Any object X that has an effective basis
(β^{n},A_{n}) indexed by N is a Σsplit subobject of
Σ^{N}.
Proof Using the basis (β^{n},A_{n}), define

Then Σ^{i}(Iφ) = λ x.(Iφ)(i x) = λ x.∃ n. A_{n}φ∧β^{n} x = φ. We also recover
x = focus(∃ n.A_{n}∧ξ n). ▫ 
Incidentally, notice the use of letters here: we write x:X, φ:Σ^{X} and F:Σ^{ΣX} for the object under study, but n:N, ξ:Σ^{N} and Φ:Σ^{ΣN} for its basis, the idea being that x and φ are represented by ξ and Φ under the embedding.
Conversely, any Σsplit subobject inherits the basis of the ambient object, using the inverse images of the basic open subobjects along i:X↣ Y. However, for the compact subobjects, we use their direct images along the “second class” map
in the sense of Remark 5.14. Since I need not preserve meets, nor need the modal operator Σ^{I} A≡ A· I. This is why we find bases in which A_{n} need not preserve ⊤ and ∧.
Lemma 7.5 Let (β^{n},A_{n}) be an effective basis
for Y and i:X↣ Y a Σsplit subobject.
Then (Σ^{i}β^{n},Σ^{I} A_{n}) is an effective basis for X.
If an ∨ or ∧basis was given, the result is one too.
If A_{n} is a filter and I preserves ⊤ and ∧
then Σ^{I} A_{n} is also a filter.
In other words, Σsplit subobjects of locally compact objects are again locally compact.
Proof For φ:Σ^{X}, Iφ:Σ^{Y} has basis decomposition
Iφ ⇔ ∃ n.A_{n}(Iφ)∧β^{n} ≡ ∃ n.(Σ^{I} A_{n})φ∧β^{n}. 
Since Σ^{i} is a homomorphism, it preserves scalars, ∧ and ∃, so
φ = Σ^{i}(Iφ) = Σ^{i}(∃ n.A_{n}(Iφ)∧β^{n}) = ∃ n.A_{n}(Iφ)∧Σ^{i}β^{n}. ▫ 
Corollary 7.6 4.10) defined a basis on
Σ^{N}. ▫
These two constructions are not inverse: given an Nindexed effective basis on X, we obtain a Σsplit embedding X↣Σ^{N}, and then a basis indexed by Fin(N). In Lemma 15.6 we shall want to recover the original, Nindexed, basis.
Lemma 7.7
An embedding X↣Σ^{N} arises from a basis
according to Lemma 7.4 iff each Iφ preserves joins.
It’s then a filter basis iff, for each n,
λφ.Iφ{n} also preserves finite meets.
Proof For any basis, ξ↦ Iφξ≡∃ n. A_{n}φ∧ξ n preserves joins. Conversely, with
β^{n} ≡ λ x.i x n and A_{n} ≡ λφ.Iφ 

we recover φ x ≡ (Iφ)(i x) ⇔ ∃ n.Iφ{n}∧ i x n ⇔ ∃ n. A_{n}φ∧β^{n} x so long as Iφ preserves the join i x=∃ n.i x n∧{n}. ▫
In the rest of this section we consider the classical interpretations of the Σsplit embedding that arises from an effective basis, starting with traditional topology. Recall from [Joh82, Theorem II 1.2] that the free frame on N is ΥK N (the lattice of upper subsets of K N), and that this is isomorphic to the lattice of Scottopen subsets of the powerset ℘(N).
Theorem 7.8 Let X be a locally compact sober space with
Nindexed basis (U^{n},K^{n}). Then X is a Σsplit subspace
of ℘(N).
Proof The embedding in Lemma 7.4 takes

The second map, I, is Scottcontinuous because it takes ⋃_{s}^{↑} V_{s} to
{ℓ ∣ ∃ n∈ℓ.K^{n}⊂⋃_{s}^{↑} V_{s}} = {ℓ ∣ ∃ n∈ℓ.∃ s.K^{n}⊂ V_{s}} = ⋃_{s}^{↑}{ℓ ∣ ∃ n∈ℓ.K^{n}⊂ V_{s}}. 
The composite Σ^{i}· I takes V⊂ X to ⋃ {⋂_{n∈ℓ}U^{n} ∣ ∃ n∈ℓ.K^{n}⊂ V}, and by Definition 1.1, this contains V={x ∣ ∃ n.x∈ U^{n}⊂ K^{n}⊂ V}. For the converse, if x∈Σ^{i}(I V) then ∃ℓ.∀ n∈ℓ. x∈ U^{n}∧ ∃ m∈ℓ.K^{n}⊂ V, so ∃ n.x∈ U^{n}⊂ K^{n}⊂ V. ▫
Example 7.9 A compact Hausdorff space has a basis determined by a family
of disjoint pairs (U^{n}⋔ V_{n}) of open subspaces.
In this case, the embedding is

Consider in particular the embedding of ℝ in Σ^{N}, where N indexes a basis of open and closed intervals (Examples 1.4 and 6.10). This is closely related to one of the first examples that Dana Scott used to show how continuous lattices could be used as a model of computation [Sco70].
Definition 7.10
The lattice of intervals, Iℝ^{⊤},
of ℝ is the set of convex closed subspaces
(including the empty one),
ordered by reverse inclusion, and given the Scott topology.
The domain of intervals, Iℝ⊂Iℝ^{⊤},
consists of the inhabited such subspaces.
Amongst these, points of ℝ are identified with
the maximal elements.
Classically, the members of Iℝ are of the form
[r±δ], with r∈ℝ and 0≤δ≤∞.
Remark 7.11 In ASD, closed subobjects under reverse inclusion
correspond to their coclassifiers under the (forward) intrinsic order,
and to the “complementary” open subobjects under inclusion.
When the closed subobject is convex, the open one is δ∨υ,
where δ is lower and υ upper in the arithmetical order,
so the pair (δ,υ) is almost a Dedekind cut [I],
except that it is disjoint but need not be “located”.
It has this last property exactly when the closed subobject is a singleton.
Intervals [p,q] or [r±δ] with specified endpoints are of this form, but (in ASD and other constructive forms of analysis), not every inhabited convex closed bounded subobject need have endpoints. It does so iff it is also overt [J]. In particular, a directed join in Iℝ of subobjects with endpoints need not itself have them.
It is, however, not necessary to appreciate this issue in order to see the relationship between Iℝ and our representation of ℝ as a Σsplit subobject of Σ^{N}.
where N is the set of pairs, written <q±є>, with є>0 and q rational.
(Recall that the square tail indicates a closed inclusion.)
Proof The embedding takes r∈ℝ to [r±0] and then to λ<q±є>.r∈(q±є), which is (the exponential transpose of) a continuous function. The retraction is defined by intersection:
Any compact interval of the T_{1} space ℝ is saturated in the sense of Lemma 5.15. It is therefore the intersection of its open neighbourhoods, amongst which open intervals suffice. Hence the composite is Iℝ^{⊤}→Σ^{N}→Iℝ^{⊤} is the identity.
The projection Iℝ^{⊤}↞Σ^{N} is Scottcontinuous because it clearly takes directed unions of sets of codes to codirected intersections of compact subspaces. Classically, Lemma 5.17 showed that such intersections correspond to unions of neighbourhood filters, whilst in ASD they correspond to the unions of the complementary open subobjects δ∨υ. Hence the inclusion Iℝ^{⊤}↣Σ^{N} is also Scottcontinuous.
The inverse image of ⊤ under Iℝ^{⊤}↞Σ^{N} is the open subobject classified by the inconsistency predicate
InCon(φ) ≡ ∃<q_{1}±є_{1}><q_{2}±є_{2}>. (q_{1}+є_{1}< q_{2}−є_{2}) ∧φ<q_{1}±є_{1}>∧φ<q_{2}±є_{2}>. 
The complementary closed subobject of Σ^{N} is of course not classified, as it’s not open, but when we restrict attention to its (overt discrete collection of) finite elements, we find that consistency is characterised by the decidable formula
Con(ℓ) ≡ ∃ x:ℚ.∀<q±є>∈ℓ.x∈<q±є>, 
so
InCon(λ<q±є>.<q±є>∈ℓ) = ¬Con(ℓ). ▫ 
Remark 7.13
The idea behind the domain of intervals is not hard to generalise.
Indeed, we may embed any locally compact sober space as a subspace of
its continuous preframe of compact saturated subspaces (Theorem 5.18),
each point being represented by its saturation in
the sense of Lemma 5.15.
That the image consists of the maximal points (excluding ∅)
plainly depends on starting with a T_{1}space,
so can’t be an essential feature of the construction.
Another interesting aspect of the general construction is the decidable consistency predicate on finite elements. Scott developed these into what became a standard form of domain theory [Sco82]. The subobject of Σ^{N} that is determined by the consistent elements is closed, but also overt [F].
We shall develop our own construction of the real line via Dedekind cuts, and also discuss the interval domain further, in [I].
Now we give the localic version of Theorem 7.8. This result is the most efficient way of establishing the connection between locally compact locales and ASD.
Theorem 7.14
Let L be any Nbased continuous distributive lattice.
Then there is a frame homomorphism H and a Scottcontinuous function I
with H· I=id_{L}, as shown:
Conversely, any lattice L that admits such a pair of functions is continuous and distributive.
Proof [⇒] Let (β^{n}) be a basis for the continuous lattice L and A_{n}≡λφ.(β^{n}≪φ). Let H:ΥK N→ L be the unique frame homomorphism that extends β^{(−)}:N→ L, so
for U∈ΥK N, HU = ⋁_{ℓ∈U}⋀_{n∈ℓ}β^{n} ∈ L, 
and define I:L→ΥK N by Iφ = {ℓ ∣ ∃ n∈ℓ.β^{n}≪φ}. This is Scottcontinuous by a similar argument to that in Theorem 7.8, with β^{n}≺≺φ_{s} instead of K^{n}⊂ V_{s}. Then

from which we deduce H(Iφ)=φ, because (β^{n}) is a basis.
[⇐] Conversely, if such a diagram exists then I· H is a Scottcontinuous idempotent on a continuous lattice, so its splitting L is also continuous [Joh82, Lemma VII 2.3]. As H preserves joins, it has a right adjoint, H⊣ R, so id≤ R· H≡ j=j· j, and R preserves meets but not necessarily directed joins. Since H also preserves finite meets, so does j, and this is a nucleus in the sense of locale theory [Joh82, Section II 2.2], so its splitting L is a frame. ▫
Any locally compact locale is therefore determined by a Scottcontinuous idempotent E on ΥK N. It is not just an idempotent, however, since the surjective part of its splitting must be a frame homomorphism. Since the latter preserves ⊤ and ⊥ by monotonicity, and ⋁^{↑} as E is Scottcontinuous, it is enough to identify the condition on E the ensures preservation of the two binary lattice connectives, which we may treat exactly alike. (This is where Remark 3.4 came from.)
Lemma 7.15 Let I and H be monotone functions between two
semilattices, with H· I=id. Then H preserves ∧ iff
E≡ I· H satisfies the equation E(φ∧ψ) =
E(Eφ∧ Eψ).
Proof If H preserves ∧ then

For the converse, note first that we have H(φ∧ψ)≤ Hφ∧ Hψ and I(φ′∧ψ′)≤ Iφ′∧ Iψ′ by the definition of ∧. Then

so H(φ∧ψ)≤ Hφ∧ Hψ≤ H(φ∧ψ). ▫
Corollary 7.16 Any Nbased locally compact locale is determined by
a Scottcontinuous endofunction of the frame ΥK N
(or by a locale endomorphism of Σ^{ΣN}) such that
E(φ∧ψ) = E(Eφ∧ Eψ) and E(φ∨ψ) = E(Eφ∨ Eψ). ▫ 
We now have to concentrate on the logical development within abstract Stone duality, and will only return to the connection with traditional topology in Section 17. The first task is to show that every definable object has an effective basis, and is therefore a Σsplit subobject of Σ^{N}. Such subobjects are determined by idempotents E on Σ^{ΣN} satisfying the equation that we have just identified, along with its counterpart for ∨. However, even that characterisation depends on the use of bases (Lemma 10.7ff).