A followup to Scott's "Finite Factored Sets", specifically the Applications part at the end where he talked about the infinite case.
As it turns out, there's a natural-seeming (at least to my mathematical tastes) way to generalize all the finite factored set stuff to the infinite case.
To be perfectly clear about what is being claimed:
1: It is possible to deal with arbitrary compact metric spaces, instead of just finite products of finite sets, with a minimum of fuss. In particular this means that we can have countably many axes/basis factors/coordinates now!
2: Orthogonality, time, history, and all that remain perfectly well-defined in the infinite-coordinate case, no meaningful differences crop up in comparision to how the finite case works.
4: Of the three ways to implement the extension to the infinite case which were suggested in Scott's post, it is closest in spirit to the second approach, with having the history of X be the intersection of all the sets C⊆B s.t. C⊢X. The proffered counterexample from Scott's post is forbidden by restricting the partitions to "sufficiently nice" ones, which makes everything Just Work.
5: Yes, the semigraphoid axioms, and everything not specifically mentioned, work out, with absolutely no special tricks needed besides the single starting restriction on only using "sufficiently nice" partitions and sets.
6: I was only able to get one direction of the fundamental theorem to work out (the conditional orthogonality to conditional probabilistic independence direction), since the nice attributes of ordinary vanilla polynomials don't last when you start mucking about with uncountable sums of countable products of variables. It's fairly plausible that the missing direction of the fundamental theorem does work out and I'm just not a good enough mathematician to show it, feel free to try it yourself. I suspect it'll require a different proof path than the original, though.
7: Daniel Filan has, completely independently of me, generalized all results in "Finite Factored Sets" to countable sets (note that in that case, there can still only be finitely many factors, while this version can have countably many factors. Daniel's version of things is unconstrained by the compactness restriction that I have, though.) Apparently everything works out perfectly, including the fundamental theorem, although the direction of it which I failed to show was also tricky for them, and TurnTrout contributed several essential pieces of the proof for that.
Let's get started.
Why Nice Partitions? What is "Nice" Anyways?
So, first off: where someone working in combinatorics sees a partition of a set, a topologist sees a quotient space.
If you've got a space S, then a partition X induces a function ∼X:S→X, which maps a point to the unique equivalence class it's in. Then, we just need to stick a topology on the set X, which ends up being "put as many open sets in X as you can while keeping the function ∼X continuous".
Basically, taking a quotient is the process of taking a space and using an equivalence relation to go "let's make a new space where all things in the same equivalence class is treated as the same point". Quotient spaces are generally written as something like S/∼.
So, if you're trying to generalize finite factored sets to the infinite case, and are working with various sorts of partitions, looking at the quotient spaces of the partitions is a very natural thing to do.
The teensy little problem is that taking quotients is just not a very well-behaved operation topologically. Operations like disjoint sum and products are very good at preserving toplogical properties. You take two "nice" spaces, for many definitions of "nice", take a product, and it'll probably be "nice" as well, for many definitions of "nice". Quotients... not so much. If you're dealing with arbitrary quotients, you can whip up some pretty hideous-looking spaces. The natural next question is whether there's some sort of topological property that is preserved by "sufficiently nice" quotients.
To cash out what "sufficiently nice" means, Hausdorffness is a very basic property on topological spaces, that's held by most spaces encountered in typical mathematical practice (type theory excepted), and topology gets a lot stranger if it isn't present. It's "given two distinct points, there are disjoint open neighborhoods around the two points". Basically, for any two distinct points x and y, it should be possible to come up with some notion of "close to x" and "close to y" that are mutually exclusive. So, we could demand that our quotient spaces at least be this nice.
Much nicer than that are compact metrizable spaces. Approximately, any space with a notion of distance, and for all ϵ, you can cover the space with finitely many patches of size ϵ. Well, actually, this isn't true, compactness is stronger than that, but I think it gets the spirit across. Examples of such spaces are finite batches of points, the space of all finite and infinite bitstrings, the space of probability distributions over a 256-dimensional hypersphere, the Mandelbrot set, and the space of all closed subsets of the interval [0,1]. They're extraordinarily nicely-behaved topologically while still managing to cover a healthy chunk of spaces that might be encountered in practice.
And, as it turns out, there is a lovely theorem that, for compact metrizable spaces S, if the quotient space S/∼ happens to be Hausdorff (ie, not terrible), the quotient space will also be compact metrizable (about as nice as possible). Or at least, that's what Math StackExchange says.
The rough idea behind the proof is that quotients of compact spaces are always compact, so that leaves metrizability. Using compactness of S and Hausdorffness of S/∼, it's possible to show the intermediate result that, for every set K⊆S that's a union of equivalence classes and closed, you can take an open neighborhood of K and it will contain a smaller open neighborhood which remains open when shoved through ∼. Using this ability to craft open neighborhoods that remain open even after applying ∼, you can push enough open sets forward into the quotient space S/∼ to show that it's second-countable and regular (the regularity argument was skipped in the linked post but it's not hard to fill in). And now, you can invoke the Urysohn Metrization Theorem to show the quotient space is metrizable.
A nifty related theorem that we won't use anywhere is that every compact metric space arises as a quotient of the space of infinite bitstrings. {0,1}ω is all you need.
So... what happens if we try to make all the stuff from "Finite Factored Sets" work with compact metrizable spaces, and we just restrict the sorts of partitions we're dealing with to the nice ones? (those where the resulting quotient space S/∼X is Hausdorff.) Well then, everything works out exactly as you'd expect and you have to change no important definitions, except one direction of the fundamental theorem gets really dang hard and I gave up on it. The nice behavior of the quotient spaces works miracles to tame the infinite case.
Let's start running through the Finite Factored Sets posts, flagging everywhere which requires special care. For all results not specifically mentioned, assume it works out perfectly with very little effort involved in cleaning things up for the infinite case. As usual, feel free to gloss over proofs if you want, but at least read the discussion and theorem statements.
Countably Factored Spaces: Introduction and Factorization
Not much really changes here, except now we aren't dealing with just a batch of sets, we've got some topological structure on them too. And the permissible quotients have to respect the topology appropriately.
The first differences start showing up around definition 8. Since we aren't permitting just any old partition anymore, we need to put in some work to check that the intersection of nice partitions is a nice partition, especially since there can be uncountably many partitions!
Proposition 1:Given a compact metrizable space S, and a set of partitions C s.t. for all c∈C, S/∼c is Hausdorff, the partition ⋁C, defined by s0∼⋁Cs1↔∀c∈C:s0∼cs1, has the property that S/∼⋁C is Hausdorff.
Proof: Fix two distinct points in S/∼⋁C. These correspond to equivalence classes in S, so we'll write them as [s0]⋁C and [s1]⋁C for some distinguished s0 and s1. From this point on, a superscript of p on an equivalence class like this means we'll be treating it as a point in a quotient space, a superscript of e means we'll be treating it as an subset of S.
Our task is to find open neighborhoods for those two points in S/∼⋁C which don't overlap. Since they're distinct points in the quotient, the corresponding equivalence classes in S are distinct, s0 and s1 are in different equivalence classes. There has to be somec∗∈C s.t. [s0]ec∗≠[s1]ec∗ (because otherwise, s0 and s1 would be in the same equivalence class according to ∼⋁C, which is impossible).
What now? Well, now that we've got a c∗ that thinks that s0 and s1 are noticeably different, make a function ϕ:S/∼⋁C→S/∼c∗ defined as ϕ([s]p⋁C):=[s]pc∗. Basically, you can think of a point in S/∼⋁C aka an equivalence class under ⋁C, as being associated with one equivalence class for each c∈C, by how the intersection equivalence class is defined. And that tells you what point to map it to in S/∼c∗.
Next up, we'll show that ϕ∘∼⋁C=∼c∗. This is easy, we just take some s∈S, and go:
ϕ(∼⋁C(s))=ϕ([s]p⋁C)=[s]pc∗=∼c∗(s)
Done. Alright, now that we've got enough setup out of the way, we can start building our disjoint open neighborhoods. The two points [s0]
A followup to Scott's "Finite Factored Sets", specifically the Applications part at the end where he talked about the infinite case.
As it turns out, there's a natural-seeming (at least to my mathematical tastes) way to generalize all the finite factored set stuff to the infinite case.
To be perfectly clear about what is being claimed:
1: It is possible to deal with arbitrary compact metric spaces, instead of just finite products of finite sets, with a minimum of fuss. In particular this means that we can have countably many axes/basis factors/coordinates now!
2: Orthogonality, time, history, and all that remain perfectly well-defined in the infinite-coordinate case, no meaningful differences crop up in comparision to how the finite case works.
4: Of the three ways to implement the extension to the infinite case which were suggested in Scott's post, it is closest in spirit to the second approach, with having the history of X be the intersection of all the sets C⊆B s.t. C⊢X. The proffered counterexample from Scott's post is forbidden by restricting the partitions to "sufficiently nice" ones, which makes everything Just Work.
5: Yes, the semigraphoid axioms, and everything not specifically mentioned, work out, with absolutely no special tricks needed besides the single starting restriction on only using "sufficiently nice" partitions and sets.
6: I was only able to get one direction of the fundamental theorem to work out (the conditional orthogonality to conditional probabilistic independence direction), since the nice attributes of ordinary vanilla polynomials don't last when you start mucking about with uncountable sums of countable products of variables. It's fairly plausible that the missing direction of the fundamental theorem does work out and I'm just not a good enough mathematician to show it, feel free to try it yourself. I suspect it'll require a different proof path than the original, though.
7: Daniel Filan has, completely independently of me, generalized all results in "Finite Factored Sets" to countable sets (note that in that case, there can still only be finitely many factors, while this version can have countably many factors. Daniel's version of things is unconstrained by the compactness restriction that I have, though.) Apparently everything works out perfectly, including the fundamental theorem, although the direction of it which I failed to show was also tricky for them, and TurnTrout contributed several essential pieces of the proof for that.
Let's get started.
Why Nice Partitions? What is "Nice" Anyways?
So, first off: where someone working in combinatorics sees a partition of a set, a topologist sees a quotient space.
If you've got a space S, then a partition X induces a function ∼X:S→X, which maps a point to the unique equivalence class it's in. Then, we just need to stick a topology on the set X, which ends up being "put as many open sets in X as you can while keeping the function ∼X continuous".
Basically, taking a quotient is the process of taking a space and using an equivalence relation to go "let's make a new space where all things in the same equivalence class is treated as the same point". Quotient spaces are generally written as something like S/∼.
So, if you're trying to generalize finite factored sets to the infinite case, and are working with various sorts of partitions, looking at the quotient spaces of the partitions is a very natural thing to do.
The teensy little problem is that taking quotients is just not a very well-behaved operation topologically. Operations like disjoint sum and products are very good at preserving toplogical properties. You take two "nice" spaces, for many definitions of "nice", take a product, and it'll probably be "nice" as well, for many definitions of "nice". Quotients... not so much. If you're dealing with arbitrary quotients, you can whip up some pretty hideous-looking spaces. The natural next question is whether there's some sort of topological property that is preserved by "sufficiently nice" quotients.
To cash out what "sufficiently nice" means, Hausdorffness is a very basic property on topological spaces, that's held by most spaces encountered in typical mathematical practice (type theory excepted), and topology gets a lot stranger if it isn't present. It's "given two distinct points, there are disjoint open neighborhoods around the two points". Basically, for any two distinct points x and y, it should be possible to come up with some notion of "close to x" and "close to y" that are mutually exclusive. So, we could demand that our quotient spaces at least be this nice.
Much nicer than that are compact metrizable spaces. Approximately, any space with a notion of distance, and for all ϵ, you can cover the space with finitely many patches of size ϵ. Well, actually, this isn't true, compactness is stronger than that, but I think it gets the spirit across. Examples of such spaces are finite batches of points, the space of all finite and infinite bitstrings, the space of probability distributions over a 256-dimensional hypersphere, the Mandelbrot set, and the space of all closed subsets of the interval [0,1]. They're extraordinarily nicely-behaved topologically while still managing to cover a healthy chunk of spaces that might be encountered in practice.
And, as it turns out, there is a lovely theorem that, for compact metrizable spaces S, if the quotient space S/∼ happens to be Hausdorff (ie, not terrible), the quotient space will also be compact metrizable (about as nice as possible). Or at least, that's what Math StackExchange says.
The rough idea behind the proof is that quotients of compact spaces are always compact, so that leaves metrizability. Using compactness of S and Hausdorffness of S/∼, it's possible to show the intermediate result that, for every set K⊆S that's a union of equivalence classes and closed, you can take an open neighborhood of K and it will contain a smaller open neighborhood which remains open when shoved through ∼. Using this ability to craft open neighborhoods that remain open even after applying ∼, you can push enough open sets forward into the quotient space S/∼ to show that it's second-countable and regular (the regularity argument was skipped in the linked post but it's not hard to fill in). And now, you can invoke the Urysohn Metrization Theorem to show the quotient space is metrizable.
A nifty related theorem that we won't use anywhere is that every compact metric space arises as a quotient of the space of infinite bitstrings. {0,1}ω is all you need.
So... what happens if we try to make all the stuff from "Finite Factored Sets" work with compact metrizable spaces, and we just restrict the sorts of partitions we're dealing with to the nice ones? (those where the resulting quotient space S/∼X is Hausdorff.) Well then, everything works out exactly as you'd expect and you have to change no important definitions, except one direction of the fundamental theorem gets really dang hard and I gave up on it. The nice behavior of the quotient spaces works miracles to tame the infinite case.
Let's start running through the Finite Factored Sets posts, flagging everywhere which requires special care. For all results not specifically mentioned, assume it works out perfectly with very little effort involved in cleaning things up for the infinite case. As usual, feel free to gloss over proofs if you want, but at least read the discussion and theorem statements.
Countably Factored Spaces: Introduction and Factorization
Not much really changes here, except now we aren't dealing with just a batch of sets, we've got some topological structure on them too. And the permissible quotients have to respect the topology appropriately.
The first differences start showing up around definition 8. Since we aren't permitting just any old partition anymore, we need to put in some work to check that the intersection of nice partitions is a nice partition, especially since there can be uncountably many partitions!
Proposition 1: Given a compact metrizable space S, and a set of partitions C s.t. for all c∈C, S/∼c is Hausdorff, the partition ⋁C, defined by s0∼⋁Cs1↔∀c∈C:s0∼cs1, has the property that S/∼⋁C is Hausdorff.
Proof: Fix two distinct points in S/∼⋁C. These correspond to equivalence classes in S, so we'll write them as [s0]⋁C and [s1]⋁C for some distinguished s0 and s1. From this point on, a superscript of p on an equivalence class like this means we'll be treating it as a point in a quotient space, a superscript of e means we'll be treating it as an subset of S.
Our task is to find open neighborhoods for those two points in S/∼⋁C which don't overlap. Since they're distinct points in the quotient, the corresponding equivalence classes in S are distinct, s0 and s1 are in different equivalence classes. There has to be some c∗∈C s.t. [s0]ec∗≠[s1]ec∗ (because otherwise, s0 and s1 would be in the same equivalence class according to ∼⋁C, which is impossible).
What now? Well, now that we've got a c∗ that thinks that s0 and s1 are noticeably different, make a function ϕ:S/∼⋁C→S/∼c∗ defined as ϕ([s]p⋁C):=[s]pc∗. Basically, you can think of a point in S/∼⋁C aka an equivalence class under ⋁C, as being associated with one equivalence class for each c∈C, by how the intersection equivalence class is defined. And that tells you what point to map it to in S/∼c∗.
Next up, we'll show that ϕ∘∼⋁C=∼c∗. This is easy, we just take some s∈S, and go:
ϕ(∼⋁C(s))=ϕ([s]p⋁C)=[s]pc∗=∼c∗(s)
Done. Alright, now that we've got enough setup out of the way, we can start building our disjoint open neighborhoods. The two points [s0]