By the factorization theorem, s is surjective. Now, assume that T implicitly defines P over
L . Then, by definition, for x = P/~1 , g(x) = P/~2 ~ 2/~2 = h^x^ ' ^ n c e - * *s a n
equalizer, there is a (unique) y e E such that i(y) = x, and since s is surjective, there is
z = p/~Q e A , p an L-formula, such that s{z) = y, hence f (z) = i s (z) = x , which is
to say that T \- p-— P as promised.
An appropriate "PC-"generalization of Beth (of a kind that is well-known in model
theory) can in fact be shown to be equivalent, via the process of translation from propositional
theories and Boolean algebras and back, to the factorization theorem for Boolean algebras.
Our proof of the factorization theorem will be an application of the Stone duality theory.
The idea of the proof is simple; the duality theory presents the opposite of Boole as a certain
well-understood category Stone , that of Stone spaces. Since the latter is sufficiently
algebraic, the regular factorization in it is the standard one. By duality, the regular factorization
in Stone corresponds to the coregular factorization in Boole . It takes a little further
argument to conclude the result.
We will state the Stone theory to the extent, and in the form, that we need it. In
particular, no topology will be involved; this is important for the 2-categorical generalization we
use for the main purpose.
A concrete category is just a category C with a functor (called "forgetful") to Set .
Many categories in practice appear as concrete categories, because a natural forgetful functor is
present. One usually makes assumptions about the forgetful functor (e.g. that it is faithful); we
will state those explicitly as we need them. An arrow in a concrete category is surjective or
injective if its image under the forgetful functor in Set is a surjective or injective function,
The Zawadowski setup, by definition, consists of an adjunction between two concrete
Aup S, F-\G ( e : counit)
G *
with the following conditions imposed:
ZO. A and S are finitely complete and cocomplete, the forgetful functor on A
preserves equalizers and reflects isomorphisms.
Zl. e :A—FGA (in A ) is injective for all As A.
X GA injective
Z2. (transpose) I ;
A FX surjective
that is, the transpose of an injective arrow in S is surjective in A .
Previous Page Next Page