7  Algebras

A perhaps more obvious way to construct the monadic completion of S (as I did in 1993) is to consider the algebras, and in fact S≃Alg_KS^op does the job. As in other approaches, the central difficulty remains that of binary products in S, i.e. coproducts of algebras. For convenience, we assume in this section alone that idempotents split in S, so KS≃S.

The equivalence S≃Alg^op says that every algebra (A,α) is to be (Σ^X,Σ^η_X) for some new object X∈obS (Definition 3.1). This means that we have to prove properties of A on the basis of its algebra structure that would be obvious if we already knew that A=Σ^X. The key such property turns out to be the double exponential transposition,

where X and Y are the S-objects corresponding to the algebras A and B, and Σ^X corresponds to Σ^A because the functor S→S is supposed to preserve Σ⁽⁻⁾.

In effect, using algebras means that we insist on representing each S-object in “normal form” by means of its standard resolution

whereas Section 4 was much more flexible about Σ-split pairs. For example, Lemma 5.8 gave the obvious formula for (Y⇉ Z)× W, but this does not take standard resolutions to standard resolutions: the structure map α^W that it provides must be composed with a map

When we generalise from Σ^X to A, we must replace Σ^{X× W} by A^W.

Remark 7.1 For any algebra (A,α) and object W, the object A^W splits the idempotent E^W, where A itself splits E≡α;η_A. Then A^W carries a power algebra structure, Σ^τ_A,W;α^W, where the natural transformation

plays a similar role to that of the strength σ of the monad (Remark 5.9). If H:A→ B is a homomorphism them so is H^W:A^W→ B^W, by naturality of τ_(−),W.        ▫

In fact, for any strong monad T whose algebras are exponentiable, an algebra structure T(A^W)→ A^W is given by the transpose of

Remark 7.2 When X and Y are expressed by means of the standard resolution, the pullback in Remark 5.10 is as shown on the left. As Σ^{X×Σ2 Y}=(Σ^X)^{(Σ2 Y)}=A^ΣB, the corresponding diagram in Alg is the one on the right, and is to be a pushout of homomorphisms.

As often happens when we consider algebras, the homomorphisms on the bottom and right are split by functions, the two idempotents in Remark 5.10 being E₁^ΣB and E₂^ΣA, where E₁≡α;η_A and E₂≡β;η_B. When we construct the pushout, we shall find that the other two maps are also split, with the result that the pushout of functions, like the coequalisers that we have used, is absolute. In particular, Σ²(A⊗ B) is also a pushout, enabling us to define the algebra structure Σ²(A⊗ B)→(A⊗ B).

(The reason for using the symbol ⊗ for the coproduct of algebras is simply that the corresponding construction in locale theory is a tensor product of the underlying join semilattices.)

That is the plan for the later parts of the construction, but it also provides the idea for the central technical result. The composite B^ΣA→Σ^ΣA×ΣB→ A^ΣB takes G to λψ.α(λφ.ψ(Gφ)). We now make use of the corresponding external transformation. For A=Σ^X and B=Σ^Y, this is just the double exponential transposition S(Σ^ΣX,Σ^Y)≅S(Σ^ΣY,Σ^X).

Lemma 7.3 G↦Σ^G;α and F↦Σ^F;β restrict to a bijection Alg(Σ^A,B)≅Alg(Σ^B,A) that’s natural with respect to homomorphisms.

Proof    Whatever G is, F≡Σ^G;α is a homomorphism, being a composite of two homomorphisms. If G is itself a homomorphism then Σ^F;β=Σ^α;Σ^ΣG;β=Σ^η_B;G=G. Given homomorphisms u:A→ A′ and v:B→ B′, the correspondence takes Σ^v;F;u to Σ^u;G;v.         ▫

Remark 7.4 We can define an internal notion of “object of homomorphisms” (which should also have its own notation) by interpreting the external Eilenberg–Moore equation as the equaliser

or by a generalisation of the equaliser in Proposition 3.2 with B in place of Σ.

The argument in the Lemma internalises, to show that Alg(Σ^A,B) is a split equaliser (retract) of B^ΣA. Moreover, it is isomorphic in S to Alg(Σ^B,A), and we write A⊗ B for either of them. The same argument shows that A⊗ B is an absolute pushout in S, whence it carries a unique algebra structure that makes it a pushout of algebras.         ▫

From the external result we can deduce Lemma 5.7, that S→S preserves products of injectives (actually, just carriers of algebras, but that’s no handicap).

Lemma 7.5 If C,D∈obS are carriers of algebras then

is a coproduct diagram of algebras.

Proof    For any other algebra Θ (playing the role of Σ^Γ in Section 5),

using Lemma 7.3 three times. Lemma 5.5 gave the algebra structure on C× D.         ▫

Corollary 7.6 The algebra Σ^ΣA×ΣB has the universal property that

Proof    Put C≡Σ^A and D≡Σ^B and recall that S(A,Θ)≅Alg(Σ^ΣA,Θ).         ▫

Next we prove that the power algebra does the job for which it was introduced in Remark 7.1. Here A and D play the roles of Σ^{{Y ∣ E}} and W in Lemma 5.8

Lemma 7.7 For algebras A and D, the diagram A→ A^D ← Σ^D is a coproduct of algebras.

Proof    The left-hand column is a U-split coequaliser of algebras, i.e. an absolute coequaliser in S, which the functor (−)^D therefore preserves. So the middle column is a coequaliser of (power) algebras, in which the middle and bottom objects are coproducts by Lemma 7.5. But the universal properties of coproducts and coequalisers commute, cf. products and equalisers in Lemma 5.8.         ▫

Corollary 7.8 The algebra A^ΣB has the universal property that

Theorem 7.9 A⊗ B carries the structure of the coproduct of the algebras A and B.

Proof    By Remark 7.2, A⊗ B is an absolute pushout of the diagram in S, so there is a unique algebra structure on it that makes this diagram a pushout in Alg.

Hence we have isomorphic pullbacks in Set,

or, in plain English, if the functions A→Θ and B→Θ are actually both homomorphisms then they correspond to a homomorphism from A⊗ B. Therefore this has the universal property of the coproduct.         ▫

Example 7.10 Recall that any idempotent defines a partition and chooses an element from each equivalence class. In this case the two partitions are the same but the choices of elements are different. For example in the simplest case, A≡ B≡1, the two representations are embedded as the singletons {⌜π₀⌝} and {⌜π₁⌝} in Σ^Σ2.

Proposition 7.11 Powers of Σ (as we write it) in S≡Alg^op are given by

Proof    Since A⊗ B was defined to have Alg(Σ^A,B) as its set of global elements,

where A≡Σ^Γ and B≡Σ^X.         ▫

Remark 7.12 For the other structure in terms of algebras,

1. the terminal object is (Σ,Σ^η₁);
2. the natural numbers object is Σ^ℕ;
3. S≅S because Alg_S≅Alg_S.

The last part says that S=Alg^op is monadic, and therefore admits subspaces as described in Sections 3 and 6, since we assumed that idempotents split in S.         ▫