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,
Alg(Σ^{A},B) = |
| (Y,Σ^{X}) ≅ |
| (X,Σ^{Y}) = Alg(Σ^{B},A), |
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
Σ^{ τΣX,W}: Σ^{ ΣΣ(X× W)} →Σ^{ (ΣΣX× W)}. |
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
τ_{A,W}:W×Σ^{A}→Σ^{AW} by x,φ↦λ f.φ(f x) |
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_{1}^{ΣB} and E_{2}^{ΣA}, where E_{1}≡α;η_{A} and E_{2}≡β;η_{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, Σ^{2}(A⊗ B) is also a pushout, enabling us to define the algebra structure Σ^{2}(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),
Alg(Σ^{C},Θ)×Alg(Σ^{D},Θ) ≅ Alg(Σ^{Θ},C)×Alg(Σ^{Θ},D) ≅ Alg(Σ^{Θ},C× D) ≅ Alg(Σ^{C× D},Θ) |
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
S(A,Θ)×S(B,Θ) ≅ Alg(Σ^{ΣA×ΣB}, Θ). |
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
Alg(A,Θ)×S(B,Θ) ≅ Alg(A^{ΣB}, Θ). ▫ |
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 {⌜π_{0}⌝} and {⌜π_{1}⌝}
in Σ^{Σ2}.
Proposition 7.11 Powers of Σ (as we write it) in S≡Alg^{op}
are given by
| ^{(A,α)}≡(Σ^{A},Σ^{ηA}) and η_{(A,α)}≡α, where |
| ≡(Σ^{Σ},Σ^{η1}). |
Proof Since A⊗ B was defined to have Alg(Σ^{A},B) as its set of global elements,
| (Γ× X,Σ) = Alg(Σ^{Σ},A⊗ B) = S(1,A⊗ B) = Alg(Σ^{A},B) = |
| (Γ,Σ^{X}) |
where A≡Σ^{Γ} and B≡Σ^{X}. ▫
Remark 7.12 For the other structure in terms of algebras,
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. ▫