4  Adding Σ-split subspaces

The rest of the paper shows (in three different ways) how to construct a category S in which we may form subspaces as just described, i.e. equalisers of Σ-split pairs that Σ⁽⁻⁾ takes to coequalisers. As raw material, we simply require a category S with finite products and an exponentiating object Σ, such that all objects of S are sober. A category S of this kind was defined using a λ-calculus in Section A 8. In Section 7 we shall see that Alg^op does the job, but first we do it by adding formal equalisers of Σ-split pairs.

This construction is similar to that of the so-called Karoubi completion of a category, which forces it to have splittings of idempotents. However, as the new construction is rather more complicated, you would be well advised to (re)familiarise yourself with the simpler version by proving

Remark 4.1 The Karoubi completion, KS, of any category S has

• as objects, (X,e), where e:X→ X is an idempotent, that is, e;e=e, and
• as morphisms f:(X,e₁)→(Y,e₂), the S-maps f:X→ Y with e₁;f=f=f;e₂.

Then

1. composition is inherited from S, but the identity on (X,e) is e, and
2. the idempotents e′ of KS are those of S, but they split in KS, i.e. there are maps p and i in KS such that i;p=id and p;i=e′.
3. KS is the universal way (up to equivalence) of splitting idempotents in S.         ▫

[The use of the letter K is unfortunate, as it conflicts with Kuratowski-finiteness in [E].]

From a categorical point of view, it would be easier to assume that idempotents split in S. This would “modularise” the construction of S as S↦KS↦Alg_KS↦S. However, our intention (in Section 10) is to reduce computation in S back to the restricted λ-calculus, i.e. S. KS already has some subspaces for the convenience of mathematicians, whereas the idempotents infest computations in it, so it has already crossed the line of demarcation between these subjects. For this reason, we develop a representation of S-objects directly in terms of S that splits idempotents as well as equalisers.

Definition 4.2 A typical object X of our category S is a Σ-split pair (Definition 3.7), which we may write using Notation 2.11 simply as

such that u;J=id_Y and v;J;u=v;J;v:Y−× Z. This object will temporarily be called (Y⇉ Z), or just X, in parts of the argument up to Section 6.

The identity morphism on this object will be E ≡ v;J. As in the Karoubi construction, this is an idempotent endomorphism of Y, but in the auxiliary category HS. In fact, its defining equation is stronger than idempotence.

Definition 4.3 E:Σ^Y→Σ^Y is called a nucleus on Y if E;η_Y;Σ^E=E;η_Y, or

using the λ-calculus. Observe carefully that the left hand side has an extra E.

We shall write {Y ∣ E} instead of (Y⇉ Z) for an object of S defined in terms of E like this.

When E is a first class map (E ≡ Σ^e and e ≡ E), the equation is just idempotence (e=e;e). In general, however, it says more than E=E;E, for the same reason that we remarked in Definition 2.3, namely that, in the splitting of this second class idempotent as I;i, the inclusion part i must actually be first class.

Notation 4.4 Given two nuclei, E₁ and E₂, we write E₂⊂_YE₁ if

Definition 4.5 A typical morphism from {Y₁ ∣ E₁} to {Y₂ ∣ E₂} is an HS-map H:Y₁−× Y₂ such that

the first equation being equivalent to H;u₂=H;v₂ when {Y₂ ∣ E₂} is defined by the pair u₂,v₂:Y₂⇉ Z₂. Using λ-calculus, the second equation is

which adds E₁ to the λ-equation for a homomorphism (Remark A 4.11).

Lemma 4.6 Any morphism H:{Y₁ ∣ E₁}→{Y₂ ∣ E₂} also satisfies H=E₁;H.

Proof    

        ▫

Lemma 4.7 For any split pair, E ≡ J;Σ^v is a nucleus (Definition 4.3); in particular, E is idempotent in HS.

Proof    The equation for E is the same as the second one for a morphism H ≡ E in Remark 4.5. It follows from the defining equations for u, v and J:

The first equation for a morphism is idempotence of H ≡ E, which follows from the previous result, but explicitly from the u v J equations,

Proposition 4.8 S is a category.

Proof    We have to show that composition is well defined. Let H:Y₁→ Y₂ and K:Y₂→ Y₃. Then H;K;E₃=H;K=K;H and

so H;K satisfies the definition of a morphism. Associativity is inherited from S, whilst the equations that say that E is the identity on {Y ∣ E} are those in Definition 4.5 and Lemma 4.6.         ▫

Remark 4.9 Although there is more to the data for an object of S than the maps u and v, the justification of calling such an object a “pair” is that, if we have two splittings J₁ and J₂, then E₁≡ v;J₁ and E₂≡ v;J₂ define an isomorphism between these objects of S. For example, we shall see in Proposition 5.12 that the binary product of any two non-trivial objects has two different splittings.

Lemma 4.10 S is embedded as a full subcategory of S by

(Recall that we assume that all objects of S are sober.)         ▫

Remark 4.11 Definition 2.10 provided another embedding, which represents X by its standard resolution,

This makes

where E   ≡   η_{Σ³ X};Σ³η_X  =  Ση_X;η_Σ^X by F↦λ F.F(λ x.F(λφ.φ x)).         ▫

The nucleus E is enough on its own to represent the object.

Lemma 4.12 For any object (Y⇉ Z), we have the isomorphism in S

encoded by E ≡ v;J in both directions.

Proof    The object on the right gives rise to the same nucleus because

by naturality and the unit law. It satisfies Definition 4.2 because η_Y;η_Σ^Y=id_Y and

since E is a nucleus. Hence both objects are {Y ∣ E}, on which E is the identity, and it also serves as the isomorphism in both directions.         ▫

Corollary 4.13

1. Every Σ-split mono arises in this way.
2. In particular, so does any first class retract.
3. Composites of Σ-split monos are Σ-split monos (Example 3).

Proof    Given

with i;I=id_X, put E=I;i as in Remark 2.9.

This satisfies the E equation because

by naturality of η and i;I=id_X. For composition, E≡ i₁;i₂;I₂;I₁.         ▫

Although E suffices to describe an object of the new category, and will be used in the new calculus in Section 8, it is not very illuminating. The reason for introducing the Σ-split pair (Y⇉ Z) is that the new object is its formal equaliser, as in Proposition 3.8.

Proposition 4.14 Every object (Y⇉ Z) of S is the equaliser in S of the diagram that it suggests, considered to consist of images (via Lemma 4.10) of objects and maps in S. If this diagram already has an equaliser X in S, and Σ⁽⁻⁾ takes it to a coequaliser in S, then (Y⇉ Z)≅ X in S.

Proof    For any object Γ ≡ (Y₀⇉ Z₀) of S, we check that an HS-map H:Y₀−× Y satisfies the conditions for being a S-map Γ→(Y⇉ Z) iff it satisfies those for being a S-map Γ→(Y⇉ Y) that has equal composites with u and v. This is simply a matter of changing the status of the equation H;u=H;v from being part of Definition 4.5 of a S-morphism to being a test for the equaliser.

For the second part, J;Σ^v:Σ^Y→Σ^Y has equal composites with Σ^u and Σ^v, whose coequaliser is Σ^X by hypothesis, so E ≡ J;Σ^v=Σⁱ;I for some I as shown. Both I;Σⁱ and id mediate from the equaliser to Σ^X, so are equal by uniqueness. Then i:X→(Y⇉ Z) is an isomorphism, with inverse I:(Y⇉ Z)→ X.         ▫

As the construction of S is one that “freely adjoins equalisers” we would expect at this point to have to show that S does in fact have such equalisers, including those for newly defined parallel pairs, and that Σ⁽⁻⁾ takes them to coequalisers. However, in our case, powers of Σ are involved in this statement, whereas we still have a lot of work to do to construct such powers in S. This will be done in Proposition 6.10.

We draw one easy corollary from the Proposition here, largely to show the contrast with the more difficult study of products that follows in the next section.

Proposition 4.15 The functor S→S preserves such colimits as exist.

Proof    Let (U_i) be a diagram in S. Any cocone under it with vertex (Y⇉ Z) in S is, by the previous result, a cocone with vertex Y such that for each i the composites U_i→ Y⇉ Z are equal. But this cocone might as well be in S , and has a mediator U ≡ colim U_i→ Y, which also has equal composites U→ Y⇉ Z, and is therefore a mediator U→(Y⇉ Z) in S.         ▫