6  Structure in S

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;Σ² 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

Proof    S-maps H:X₁× X₂→Σ correspond bijectively to p:1→Σ^{Y₁× Y₂} in S such that p=p;E₁^Y₂;E₂^Y₁, by Lemma 6.1. By Remark 5.10, this is equivalent to p;E₁^Y₂=p=p;E₂^Y₁. Let k:Y₁→Σ^Y₂ and q:Y₂→Σ^Y₁ be the exponential transposes of p, which satisfy k=k;E₂ and q=q;E₁. But then q corresponds to K:X₁→Σ^Y₂ by Lemma 6.1, and K=K;E₂ by the other equation, so it factors through Σ^X₂. Conversely, K defines k, q, p and H in the same way.

Now let F₁:X′₁→ X₁ and F₂:X′₂→ X₂, whose product is F₁^X′₂;F₂^X₁ by Proposition 5.12. Then by the naturality part of the Lemma, p becomes p;F₂^X₁;F₁^X′₂ and K becomes F₁;K;F₂.         ▫

Lemma 6.3 η_X:X→Σ² X in S is given by E;η_Y:Y−×Σ² Y.

Proof    From functoriality in the Proposition, Σ² 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₁=Σ^X, X₂=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◁Σ² A◁Σ² 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₁−× X₂ are given by

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₁−× X₂ is a S-map H:Σ^X₂→Σ^X₁. We have just shown that these exponentials are retracts, so this map is H:Σ^Y₂→Σ^Y₁ (now just in S) such that E₂;H=H=H;E₁. This is also how morphisms of KHS are defined (Remark 4.1).         ▫

Lemma 6.6 An HS-map H:X₁−× X₂ is first class (a S-map) iff it respects naturality of η, i.e. η_X1;Σ²H=H;η_X2, or H:Σ^X₂→Σ^X₁ is a homomorphism.

Proof    Using the previous two lemmas,

Equality of these is the second equation in Definition 4.5.         ▫

Corollary 6.7 Every homomorphism K:Σ^X₂→Σ^X₁ in S is of the form K=Σ^H for some unique S-map H:X₁→ X₂. 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:Σ² X−× X for the HS-map η_Σ^X, and that this is natural with respect to HS-maps H:X−× Y. Similarly, we now write

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}} = Σ² i ; force_Y ; admit.

Hence if Γ⊢ P:Σ² {Y ∣ E} is prime then so is Γ⊢Σ² i P:Σ² Y and

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 Σ²η₍₋₎ and ηΣ²(−), 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

where X ≡ {Y ∣ E₁} is a S-object and E₂ data on it for a S-object {X ∣ E₂}.

Proof    The defining equations for E₂ to be an HS-map and to be a nucleus (Definition 4.3), i.e. to define an S-object, are

the first of which says that E₂⊂E₁ in the sense of Notation 4.4. The second equation, between HS-maps, reduces to

in HS, but this is just the definition of a nucleus E₂ on Y. Hence {Y ∣ E₂} as a S-object, which Lemma 4.12 expresses as the equaliser of a Σ-split pair Y⇉Σ² 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

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 Σ² Y and Σ⁴ Y, so that s becomes a mediator between equalisers. Then recursion in S defines a map ℕ→Σ²Y that makes the squares commute and also has equal composites to Σ⁴ Y. Finally, the required map ℕ→{Y ∣ E} mediates to the equaliser.         ▫