I don't think anything goes wrong if AC fails as far as establishing a distributive law is concerned. No doubt much further discussion would be needed to understand well what happens, precisely, but note that many AA (e.g. principal filters) have non-empty C(AA). In any case, a sub-example obtains replacing P with the finite subsets monad, in which case no AC is needed. Ernie ----- Original Message ----- From: "Steve Vickers" <s.j.vickers@cs.bham.ac.uk> To: <categories@mta.ca> Sent: Wednesday, February 16, 2005 5:23 AM Subject: categories: Re: double covariant power set
Ernie Manes wrote:
In a paper under preparation on distributive laws, joint with Philip Mulry, we show that the families monad arises by a distributive law of the power set monad P over itself.
Though this self-distributivity of P is formally elegant, it seems (unless I've missed something) to need the axiom of choice and I wondered what its constructive content was.
I encountered a similar problem in [1], albeit with the Kuratowski powerset F instead of P. For constructivist reasons I had to use not Ernie's C(AA) of choice *functions*, but a set Ch(AA) of finite total choice *relations* - in other words, you are allowed to choose more than one element from each set. But then
AA |-> {I(x) | x in Ch(AA)}
does not give a distributivity (though I never thought of looking at this at the time).
If you generalize from sets to preorders the problem seems to go away, at least for F, and my sense is that the danger arises when you ignore the natural order on FX when calculating FFX. However, the two copies of F become two different monads F_L and F_U, corresponding to two preorders (lower and upper) on FX when X is preordered. I haven't ploughed through all the details, but I am reasonably confident that the two monads distribute over each other using the "Ch(AA)" construction, and commute. (The category of preorders has to be one in which the morphisms are equivalence classes of monotone functions.) In any case, it is known that if you work with partial orders and factor out equivalence modulo the preorders, then you find that F_L and F_U give free join and meet semilattices, and their composite (either way round) is the free distributive lattice.
Related phenomena appear in the category of locales [2] - the lower and upper powerlocale monads P_L and P_U distribute mutually and commute. Intriguingly [2], the composite double powerlocale monad PP can be expressed as an iteration of a contravariant functor PX = $^X (where $ = Sierpinski), and [3] this makes sense even in the non-locally compact case where the exponential $^X doesn't exist.
Steve Vickers.
Papers available from www.cs.bham.ac.uk/~sjv :
[1]: @ARTICLE{EntSys, AUTHOR={Vickers, Steven}, TITLE={Entailment Systems for Stably Locally Compact Locales}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, VOLUME={316}, PAGES={259--296}, YEAR={2004} }
[2]: @ARTICLE{PPExp, AUTHOR={Vickers, S.J.}, TITLE={The Double Powerlocale and Exponentiation: A Case Study in Geometric Reasoning}, JOURNAL={Theory and Applications of Categories}, VOLUME={12}, YEAR={2004}, PAGES={372--422} }
[3]: @ARTICLE{UniCharPP, AUTHOR={Vickers, S.J. and Townsend, C.F.}, TITLE={A Universal Characterization of the Double Powerlocale}, JOURNAL={Theoretical Computer Science}, ISSN={0304-3975}, VOLUME={316}, YEAR={2004}, PAGES={297--321} }
17-Feb-2005 15:44:27 -0400,5941;000000000000-00000000