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.
