What you've said here might be a reasonable reply in your head, but for me, reading its parent, and this reply, I can't work out what you're trying to say.
You need to be really careful about things like "infinitely large map" ... if you want to talk about really large things then they are really large. But if you want to talk about infinite sized things then you need to be careful. There are traps in infinities, and this theorem is about finite maps (or equivalently, graphs).
Proving that a small, local sub-section doesn't require five colours is helpful, but no one has been able to extend that, because there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
You are saying the sorts of things I've seen many times before, but you need to try to make complete, precise statements about exactly what you propose. So far all you've said is that you can't arrange five regions that all touch each other, and that's true. Now, exactly how do you extend that to a map with billions of regions?
It was the comment I replied to that introduced infinitely large maps - but regardless I wasn't trying to be as clever as you might be trying to assume (and of course not finding it :)) - I would have said the same about 'really large' or indeed 'just a bit larger than the 4 or 5 regions I described initially'.
> there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
This is the bit I can't grasp - I honestly appreciate the responses and attempts to explain it, but it just (mistakenly, I can accept even if I don't understand) seems counter-intuitive to me. As in, intuitive that it extends, or that there's no such problem.
Maybe I just need to play with it on paper a bit, stumble into such a spooky action to get it.
> Now, exactly how do you extend that to a map with billions of regions?
I don't have the background for the precision you'd like I'm afraid (if I did, I'm sure I'd understand anyway!) but loosely - divide and conquer; a similar thing happens at the interface of all the 'sub-maps'?
>> there is a kind of "spooky action at a distance" that can happen
> This is the bit I can't grasp
OK. Let me give you a collection of statements, each of which I can expand on, but which might give you a sense of the problem.
* Instead of colouring regions in a map we can colour vertices of a graph;
(put a vertex in each region and connect vertices if their regions share a border)
* If a graph can be three-coloured then it can be four-coloured;
(Any three colouring is a four colouring, but with no vertices of the fourth colour)
* An instance of colouring an arbitrary graph can be converted into an instance of colouring a planar graph;
(There is a "widget" that uncrosses edges)
* Given a number to factor, we can construct a graph such that three-colouring the graph will produce a factorisation[0];
(Graph three-colouring is NP-Complete, so this is even easier than that)
Broadly, we can construct a graph that has exactly one (up to permutation of colours) valid three-colouring. As you start to colour it you find that you have to make choices, on average about $4/3$ choices per vertex[1]. But the wrong choice results in not being able to complete the colouring, and you don't know which choice or choices were wrong.
So you get this "spooky action at a distance" thing going on.
Sometimes a planar graph can't be coloured with three colours, and sometimes it can but a colouring is hard to find. When we allow the extra colour it turns out that it's always possible, but it's not obvious that that should be the case.
That's an #ISS-level view of the ideas ... hope it helps.
I'm sure I'm mistaken, but I believe the conversion to a graph loses exactly the information I'm trying to use: a vertex with three edges, where each of those vertices are also all interconnected, can have a fourth edge to a fifth vertex which also has an edge to each of the others; on the map this is not possible. Right?
From my napkin sketch to satisfy myself, I think you can show the same thing equivalently by saying 'and the edges are not allowed to cross' - but I don't know if that's something that exists in graph theory? (If so, it seems to me it should be used here? And if it is, well, finally we have a modicum of precision for what I'm trying to get at!)
If you have a map in which you want to colour the regions, you can convert to a graph by putting a capital city in each region, then putting a road between two capitals of countries that share a border. Colouring the capital cities vertices) so that any joined by roads (edges) get different colours is exactly the same problem.
The graph-colouring problem is more general now, but every planar graph is equivalent to a map and vice-versa ... there is a one-to-one correspondence between these problems.
Now we move to the NP-Completeness of the 3-colouring of general graphs. That shows that this sort of thing is hard for the reasons I gave in the grandparent post.
"But" I hear you say "That's for general graphs, and not for planar graphs!"
Yes, but there is a way to convert a graph-colouring problem on a non-planar graph into an equivalent graph-colouring problem on a planar graph, so we neither gain nor lose much by consider just planar graphs.
So 3-colouring planar graphs is NP-Complete.
Then you get into my comments about making bad choices and having to backtrack, and spooky action at a distance.
I have no idea what that guy is talking about, but your post reminded me of a fun trick. If you have a colouring of every finite subgraph then you can show the existence of a colouring of the whole graph by using Tychonoff's theorem.
What poset should we set up on which to invoke Zorn's lemma directly? Anything I can think of does seem to me more easily understood via compactness/the ultrafilter lemma, but that may just be a fact about my own psychology.
Yes, but invoking Zorn's lemma on that poset does nothing useful. This just proves the trivial fact that the big graph exists. How do you prove that a coloring of the big graph exists?
And if we take the poset to be partial colorings ordered by inclusion, it's not the case that a maximal partial coloring must color the entire graph. Some partial colorings have made choices which prevent them from being extended any further.
[To be clear, whenever I say "coloring", I mean from a fixed set of colors. E.g., a 4-coloring.]
Put another way, it actually is important here that the set of colors we are talking about is finite. It's NOT the case that just having every finite subgraph be C-colorable entails that the entire graph is C-colorable, when C is infinite. For example, if G is the complete graph on an uncountable set of nodes and C is a countably infinite set, then every finite subgraph of G is C-colorable, but G itself is not.
So somewhere in the argument, the finiteness of C must play a role. This is in ensuring compactness.
You need to be really careful about things like "infinitely large map" ... if you want to talk about really large things then they are really large. But if you want to talk about infinite sized things then you need to be careful. There are traps in infinities, and this theorem is about finite maps (or equivalently, graphs).
Proving that a small, local sub-section doesn't require five colours is helpful, but no one has been able to extend that, because there is a kind of "spooky action at a distance" that can happen. Local decisions about colours can lead to implications across the other side of the structure. Proving that your local decisions can always be made in a way that doesn't cause problems elsewhere is the problem.
You are saying the sorts of things I've seen many times before, but you need to try to make complete, precise statements about exactly what you propose. So far all you've said is that you can't arrange five regions that all touch each other, and that's true. Now, exactly how do you extend that to a map with billions of regions?