The strength of prime separation, sobriety, and compactness theorems

We investigate in ZF set theory without choice principles a general lattice-theoretical prime separation lemma and compare it with diverse statements about variants of the sobriety concept for topological spaces. Some of these properties coincide in the presence of choice principles but differ in their absence. UP, the Ultrafilter Principle (or, equivalently, the Prime Ideal Theorem) is not only equivalent to the Separation Lemma, but also necessary and sufficient for the desired coincidences. Furthermore, we prove the equivalence of UP to several statements about filtered systems of compact sets, among them the Hofmann–Mislove Theorems, several compact intersection theorems, and an irreducible transversal theorem. Moreover, many fundamental dualities between certain categories of topological spaces and categories of ordered structures turn out to be equivalent to UP. But we also give choice-free proofs for such dualities, amending slightly the involved definitions.