Now that we have overcome the main difficulty concerning binary products, we are equipped to tackle exponentials, and then to show that S does in fact have the monadic property for which it was designed. We still rely on injectivity, first re-casting Proposition 5.2 in terms of the double transpose of h.
Lemma 6.1
There is a natural bijection between S-maps
H:{Y ∣ E}→Σ^{U} and S-maps p:U→Σ^{Y}
such that p=p;E.
Proof Let H↦ p=η_{U};H, which satisfies p=p;E by Lemma 4.6. Conversely, let p↦H=E;η_{Y};Σ^{p}, which is a composite of S-maps {Y ∣ E}↣ Y→Σ^{U}.
Then H↦ E;η_{Y};Σ^{p}= E;η_{Y};Σ^{H};Σ^{ηU}= H;η_{ΣU};Σ^{ηU}= H by Definition 4.5 and the unit law. Conversely, p↦ η_{U};H=η_{U};Σ^{2} p;Σ^{ηY};E= p;η_{ΣY};Σ^{ηY};E= p;E=p by naturality for η and the unit law.
For naturality, let F:{Y′ ∣ E′}→{Y ∣ E} and g:U′→ U. Then p becomes g;p;F. ▫
Proposition 6.2
S has and S→S preserves powers of Σ, where
Σ^{{Y ∣ E}} ≡ {Σ^{Y} ∣ Σ^{E}} and Σ |
| ≡ F. |
Proof S-maps H:X_{1}× X_{2}→Σ correspond bijectively to p:1→Σ^{Y1× Y2} in S such that p=p;E_{1}^{Y2};E_{2}^{Y1}, by Lemma 6.1. By Remark 5.10, this is equivalent to p;E_{1}^{Y2}=p=p;E_{2}^{Y1}. Let k:Y_{1}→Σ^{Y2} and q:Y_{2}→Σ^{Y1} be the exponential transposes of p, which satisfy k=k;E_{2} and q=q;E_{1}. But then q corresponds to K:X_{1}→Σ^{Y2} by Lemma 6.1, and K=K;E_{2} by the other equation, so it factors through Σ^{X2}. Conversely, K defines k, q, p and H in the same way.
Now let F_{1}:X′_{1}→ X_{1} and F_{2}:X′_{2}→ X_{2}, whose product is F_{1}^{X′2};F_{2}^{X1} by Proposition 5.12. Then by the naturality part of the Lemma, p becomes p;F_{2}^{X1};F_{1}^{X′2} and K becomes F_{1};K;F_{2}. ▫
Lemma 6.3
η_{X}:X→Σ^{2} X in S
is given by E;η_{Y}:Y−×Σ^{2} Y.
Proof From functoriality in the Proposition, Σ^{2} takes the inclusion E to Σ^{E}. Then for η to be natural on S, we need η_{X}=E;η_{Y};Σ^{E}. But this expression is the left hand side of the defining equation for the nucleus E (Definition 4.3), the right hand side being E;η_{Y}.
Alternatively, we may see η_{{Y ∣ E}} as the double transpose of id_{{Y ∣ E}}≡E. This correspondence is that between k and q on the right hand side of the Proposition, in the case of X_{1}=Σ^{X}, X_{2}=X. Then K=id_{ΣX}=E=k and q=η_{Y};Σ^{E}, so η_{{Y ∣ E}}=E;q=E;η_{Y}. ▫
Corollary 6.4
Alg_{S}≃Alg_{KSS}≅Alg_{KS}, cf. Alg_{SS}≅Alg_{S} in Lemma A 7.3.
Proof Let (A,α) be an algebra over S, with A ≡ {Y ∣ E}. Then A◁Σ^{2} A◁Σ^{2} Y, so A may as well be in KS, since this is fully embedded in S by Corollary 4.13. ▫
Lemma 6.5 S-maps H:X_{1}−× X_{2} are given by
H:Σ^{Y2}→Σ^{Y1} such that H;E_{1} = H = E_{2};H. |
So HS⊂KHS is the full subcategory consisting of those objects (X,E) for which E is a nucleus.
Proof An HS-map H:X_{1}−× X_{2} is a S-map H:Σ^{X2}→Σ^{X1}. We have just shown that these exponentials are retracts, so this map is H:Σ^{Y2}→Σ^{Y1} (now just in S) such that E_{2};H=H=H;E_{1}. This is also how morphisms of KHS are defined (Remark 4.1). ▫
Lemma 6.6
An HS-map H:X_{1}−× X_{2} is first class (a S-map)
iff it respects naturality of η,
i.e. η_{X1};Σ^{2}H=H;η_{X2},
or H:Σ^{X2}→Σ^{X1} is a homomorphism.
Proof Using the previous two lemmas,
η_{X1};Σ^{2} |
| = |
| ;η_{Y1};Σ^{2} |
| and |
| ;η_{X2} = |
| ; |
| ;η_{Y2} = |
| ;η_{Y2}. |
Equality of these is the second equation in Definition 4.5. ▫
Corollary 6.7
Every homomorphism K:Σ^{X2}→Σ^{X1} in
S is of the form K=Σ^{H} for some unique
S-map H:X_{1}→ X_{2}.
From Section A 7 we deduce that
all objects of S are sober, that SS≅S and that
X×(−) distributes over such colimits as exist in S. ▫
Notation 6.8
Recall from Definition A 6.3
that we wrote force:Σ^{2} X−× X for the HS-map
η_{ΣX}, and that this is natural with respect to
HS-maps H:X−× Y.
Similarly, we now write
admit for |
| : Y −× {Y ∣ E}. |
Like the identity, the inclusion i:(Y⇉ Z)↪ Y and its splitting I are both encoded as E. In Section 8 we shall add an operator admit to the λ-calculus, just as we introduced focus in Section A 8, and they both have side-conditions. However, we shall not on this occasion give different names to the operator in S and the map in HS.
Lemma 6.9
force_{{Y ∣ E}} = Σ^{2} i ; force_{Y} ; admit.
Hence if Γ⊢ P:Σ^{2} {Y ∣ E} is prime then so is Γ⊢Σ^{2} i P:Σ^{2} Y and
focus_{{Y ∣ E}} P = admit(focus_{Y}(Σ^{2} i P)). |
Proof The diagram shows naturality of force with respect to admit in HS, i.e. of η with respect to E in S. Recall from Lemma A 4.3 that P is prime iff it has equal composites with Σ^{2}η_{(−)} and ηΣ^{2}(−), which are natural with respect to i:{Y ∣ E}↣ Y. ▫
Now we can show that S has the new structure that it was introduced to provide.
Proposition 6.10
Σ-split equalisers exist in S,
and Σ^{(−)} sends them to coequalisers. Indeed
{{Y ∣ E_{1}} ∣ E_{2}} = {Y ∣ E_{2}} |
where X ≡ {Y ∣ E_{1}} is a S-object and E_{2} data on it for a S-object {X ∣ E_{2}}.
Proof The defining equations for E_{2} to be an HS-map and to be a nucleus (Definition 4.3), i.e. to define an S-object, are
| ; |
| = |
| = |
| ; |
| and |
| ;η_{X};Σ^{E2} = |
| ;η_{X}, |
the first of which says that E_{2}⊂E_{1} in the sense of Notation 4.4. The second equation, between HS-maps, reduces to
| ;η_{Y};Σ^{E2} = |
| ;η_{Y} |
in HS, but this is just the definition of a nucleus E_{2} on Y. Hence {Y ∣ E_{2}} as a S-object, which Lemma 4.12 expresses as the equaliser of a Σ-split pair Y⇉Σ^{2} Y:
Finally, Σ^{(−)} acts on this diagram in S just as it does in S, taking it to a split coequaliser, as in Proposition 4.14. ▫
Corollary 6.11
(S,Σ) is monadic and S≃Alg_{KS}^{op}.
Proof Recall that being monadic means that S≃Alg_{S}^{op}. By Theorem 3.3, this happens iff all objects are sober (which they are by Corollary 6.7) and all algebras are spatial. The latter follows from the previous result by Proposition 3.8. Finally, the equivalence with Alg_{KS}^{op} is given by Corollary 6.4. ▫
Theorem 6.12
(S,Σ) is the (Karoubi and)
monadic completion of (S,Σ):
Let (D,Σ_{D}) be monadic and suppose that idempotents split in D (so D has products, powers of Σ_{D}, equalisers of Σ_{D}-split pairs and Σ_{D}^{(−)} sends them to coequalisers.) Let F:S→D be a functor that preserves products and powers of Σ. Then there is a functor F:S→D that also preserves these things and makes the square commute, and it is unique up to equivalence.
Proof Any object of S is interpreted as a Σ-split equaliser diagram in S as in Proposition 4.14. Such diagrams are preserved by the functor F, but the diagram in D has an equaliser, which is the required image of the given S-object. F commutes with the representation of × and Σ^{(−)} in Propositions 5.12 and 6.2. ▫
Remark 6.13 The sober, Karoubi and monadic completions are related by the diagram
in which ↣ denotes a full inclusion and = an equivalence. We leave the interested reader to find a properly general recursive idempotent on ℕ (so SKS≠KSS, cf. Remark A 9.12), and to show that any retract of a sober object is sober (so KSS=SKSS). ▫
The development so far has been entirely set in the abstract situation of a category S with an exponentiating object Σ, for which all objects are sober. In the intended applications to topology and computation, Σ is a distributive lattice and satisfies the Euclidean principle [C]; this structure is preserved by the inclusion S→S since it preserves products and powers of Σ.
We also want S to have a natural numbers object ℕ, i.e. to admit primitive recursion at all S-types, although sobriety of ℕ means that general recursion is also defined (Section A 9–10). The extension of recursion to S-types follows essentially the same argument as in Proposition 4.15 for colimits.
Proposition 6.14
The inclusion S→S preserves ℕ.
Proof The recursion data in the fully parametrised version of this result consist of
z:Γ→{Y ∣ E} and s:Γ×ℕ×{Y ∣ E} → {Y ∣ E}, |
and we shall prove it symbolically like this in Lemma 8.14. Here, for brevity, we omit the parameters in s.
First, {Y ∣ E} may be expressed as an equaliser as shown.
Then use injectivity to extend s:{Y ∣ E}→{Y ∣ E} to endofunctions of Σ^{2} Y and Σ^{4} Y, so that s becomes a mediator between equalisers. Then recursion in S defines a map ℕ→Σ^{2}Y that makes the squares commute and also has equal composites to Σ^{4} Y. Finally, the required map ℕ→{Y ∣ E} mediates to the equaliser. ▫