Read on Twitter
*Thread*
Let D be the finite support probability monad, taking every set X to the set DX of f.s. probability distributions on it. D-algebras are called (abstract) convex sets, and are equivalently models of an algebraic theory first defined by Stone
https://ncatlab.org/nlab/show/convex+space
Let D be the finite support probability monad, taking every set X to the set DX of f.s. probability distributions on it. D-algebras are called (abstract) convex sets, and are equivalently models of an algebraic theory first defined by Stone
https://ncatlab.org/nlab/show/convex+space
Obviously every *actually* convex space, that is to say convex subsets of Banach spaces, are D-algebras. But there are also weird non-geometric examples
In particular, any semilattice is a convex set, by defining every *proper* mixture of x,y to be the join xvy...
In particular, any semilattice is a convex set, by defining every *proper* mixture of x,y to be the join xvy...
But every degenerate mixture (putting probability 0 or 1 on some points) has to be defined differently, eg. 1x + 0y must be interpreted as just x, not xvy in order to satisfy the algebra axioms
Making this definition requires excluded middle for real numbers...
Making this definition requires excluded middle for real numbers...
This makes me suspect that the category of D-algebras might be wildly different in classical vs constructive foundations
Stone proved that the "combinatorial type" algebras are ruled out by one additional "cancellativity" axiom. So...
Stone proved that the "combinatorial type" algebras are ruled out by one additional "cancellativity" axiom. So...
In classical foundations, the algebras of convexity + cancellativity are a small subclass of the algebras of convexity. But in constructive foundations they appear to be the same, possibly except some degenerate examples. But the convexity axioms don't imply cancellativity
In conclusion: I'm a bit confused about this
It may be that the monad D, or equivalently Stone's axioms (both of which involve real numbers) aren't suitable for constructive foundations, and the problem goes away if you change to a more suitable classically-equivalent definition
It may be that the monad D, or equivalently Stone's axioms (both of which involve real numbers) aren't suitable for constructive foundations, and the problem goes away if you change to a more suitable classically-equivalent definition
This thread was me talking about LEM for the twitter likes. In real life having the weird examples around makes the whole thing way more interesting, and I definitely wouldn't want to rule them out - it means that convex algebra is quite different from convex geometry
Tobias Fritz proved that every abstract convex set looks like *waves hands eloquently* a "topological fibre bundle" made of a bunch of pieces of Banach spaces living over a semilattice. The details of this are pretty subtle, and we're slowly making sense of it
