5  Injectives and products in S

We know from Section A 6, and from the work on continuations by others cited there, that binary products are the crucial issue. These studies have also taught us that we must take just one step at a time. In Section 7 below we sketch the construction of products in S as coproducts of algebras, but the motivation of that approach involves the anticipation of results that ought to follow from the conclusion itself.

In this section we argue forwards from the structure in the given category S, using basic (albeit pedestrian) categorical ideas, and sticking to the objects rather than their algebras of predicates. The plan is to regard S-objects as equalisers in S as in Proposition 4.14, and then use the given products in S.

However, the universal property of these given products is only tested by diagrams of the form Γ→ A× B with Γ∈obS, so we need to generalise this to Γ∈obS. This is more difficult than the situation for colimits in Proposition 4.15: in this case we need to be able to turn maps {Y ∣ E}→ A into Y→ A, which is just the property of injectivity from which we began in Remark 2.1.

Definition 5.1 An object A of S is said to be injective if, for any subspace inclusion {Y ∣ E}↣ Y and map f:{Y ∣ E}→ A, there is some (not necessarily unique) map h:Y→ A such that f=E;h.

Proposition 5.2 An object A of S is injective iff it is a retract of some Σ^U (by which we still mean the exponential in S). Indeed, when A∈obS is injective, there is a map α:Σ² A→ A such that η_A;α=id, though this need not satisfy the other equation that is required for (A,α) to be an Eilenberg–Moore algebra, namely µ_A;α=Σ²α;α.

Proof    (⇐) Suppose first that A ≡ Σ^U, and put α ≡ Σ^η_U. By Definition 4.5, any morphism H:{Y ∣ E}→ A in S satisfies

where h ≡ η_Y;Σ^H;α is in S. The result extends to retracts of Σ^U by composition with the inclusion and surjection.

(⇒) The composite {Y ∣ E}↣Σ² Y is a subspace by Corollary 4.13; injectivity says that this is split by h. When A ≡ Y∈obS, α ≡ h satisfies η_A;α=id.         ▫

Corollary 5.3 S has enough injectives: each object {Y ∣ E} is a subspace of some injective Σ² Y.         ▫

Examples 5.4 In LKSp, the injectives are the continuous lattices equipped with the Scott topology [Sco72a], whilst the algebras are also distributive. In Set, injectives are (sets that carry the structure of) complete lattices, and algebras are powersets (which, classically, are complete atomic Boolean algebras).         ▫

Lemma 5.5 Any finite product of injectives (or algebras) is again injective (respectively, an algebra).

Proof    For the terminal object, α ≡ !_Σ^Σ.

For injectives (A,α) and (B,β), we define P₀ ≡ Σ²π₀;α:Σ²(A× B)→ A and P₁ ≡ Σ²π₁;β :Σ²(A× B)→ B, and then η_{A× B};<P₀,P₁>=id. This follows from naturality of η, as illustrated in the right-hand trapezium below.

Moreover, if (A,α) and (B,β) are algebras then

so (A× B,<P₀,P₁>) is also an algebra.         ▫

Lemma 5.6 The functor S→S preserves the terminal object.

Proof    Since 1 is injective, E;!_Y is the only map H:{Y ∣ E}→1.         ▫

Lemma 5.7 The functor S→S preserves binary products of injectives.

Proof    Let F:{Y ∣ E}→ A and G:{Y ∣ E}→ B in S. Put

so F=E;f and G=E;g by Proposition 5.2, and <f,g> is given by the product in S.

Then H≡E;<f,g>:{Y ∣ E}→ A× B satisfies H;π₀=F and H;π₁=G.

Suppose that H and K both satisfy these equations. Using Lemma 5.5, put

so H=E;h and K=E;k by Proposition 5.2.

Since Σ^H;Σ²π₀=Σ^F=Σ^K;Σ²π₀, we have h;π₀=f=k;π₀ by the way in which h, k and f were constructed, and similarly h;π₁=g=k;π₁. Hence h=k=<f,g>, as these maps are in S, so H=K.         ▫

Now we can begin the main business of this section. In view of Corollary 5.3, we may assume that the S-objects of which we want to form the product are given by Σ-split pairs of maps between injectives. In fact this restriction will become redundant, as the argument below can be used first to show that all products are preserved, and then to construct products of non-injective pairs.

Lemma 5.8 Let (Y⇉ Z)∈obS and W∈obS. Then

is also an object of S. It is called (Y⇉ Z)× W because, at least when U, V and W are injective, this is the product in S. In the comprehension notation,

This is functorial with respect to

(recall that id_{{Y ∣ E}}=E) and to

Proof    Apply (−)^W to the equations in Definition 4.2 to get J^W;Σ^{u× W}=id and

Proposition 4.14 said that the formal pairs are equalisers, which property commutes with products. In comprehension notation, Σ^{v× W};J^W=E^W.

The formula for {Y ∣ E}× g is merely naturality of E⁽⁻⁾.

Using the injectivity of Y₂, we may write F as

for some (not necessarily unique) f, where (by Definition 4.5) F=F;E₂=E₁;f, so F=Σ^f;E₁. Applying (−)× W to the commutative square, the formula for F× W has to be E₁;(f× W)=G where G≡(Σ^f;E₁)^W=F^W.         ▫

Remark 5.9 Alternatively, one could show directly that E^g and F^W are morphisms, and that they satisfy the equations for the product functor. For F^W, we need to use the strength

for the monad, which is a natural transformation and obeys the equation shown.

Remark 5.10 The product of two Σ-split pairs must form a pullback (intersection) in S, in the same way that the product of any two maps in a category gives rise to a pullback.

Unfortunately, our “comprehension” notation does not admit intersections — either abstractly or in the leading example of LKLoc — so we still have to find an E on Y₁× Y₂ to describe the subspace. If E₁^Y₂ and E₂^Y₁ commute (as they do if E₁=Σ^e₁ or E₂=Σ^e₂) then their composite encodes the intersection. But it turns out that, even if E₁^Y₂;E₂^Y₁≠ E₂^Y₁;E₁^Y₂, either of them will do the job: of course products and pullbacks are unique up to isomorphism, but we have two representations of them.

Lemma 5.11 The composite

is an object of S, where

the inclusion on the last line being in the sense of Notation 4.4.

Proof    Clearly u;J=id, whilst

Using the given equations of the form v_i;J_i;u_i=v_i;J_i;v_i, we must prove this equation for the new Σ-split pair:

using centrality of u₂, and the same argument with v in place of u.

Finally, Y₁×E₂;E₁× Y₂;Y₁×E₂  =  Y₁×E₂;E₁× Y₂ by centrality of u₂ and v₂ with respect to E₁, and u₂;J₂=id.         ▫

Proposition 5.12 The category S has finite products, where

whilst the product of the morphisms F₁:X′₁→ X₁ and F₂:X′₂→ X₂ is F₁^Y′₂;F₂^Y₁.

Moreover, the functor S→S takes products in S to products in S.

Proof    First consider the product of two objects X₁,X₂∈obS, expressed in S by means of their standard resolutions, so the products Σ² X₁×Σ² X₂ etc. are preserved (Lemma 5.7). The formal product of the Σ-split pairs (Lemma 5.11) provides an equaliser in S (Proposition 4.14), which is the required product, isomorphic to X₁× X₂, i.e. this is preserved.

The construction is then applicable to any two Σ-split pairs, so all binary products exist in S. Functoriality follows from that in Lemma 5.8.         ▫

Remark 5.13 The abstract situation of idempotents є ≡ (E₂)^Y₁ and є′ ≡ (E₁)^Y₂ (in this case on the object Σ^{Y₁× Y₂}) such that є;є′ and є′;є are also idempotent is studied in Lemma D 7.1. It is shown there that the splittings of є;є′ and є′;є are isomorphic and form a pushout diagram, in our case of the algebras Σ^{X₁× X₂} etc. corresponding to objects in the above pullback.