Simply connected complements in the sphere

Stream: maths

[Geoffrey Irving]

Does mathlib have (or almost have) the result that the complement of a connected open set in the sphere is simply connected? Or equivalently, that a compact set in the plane is simply connected if its complement is connected?

[Jireh Loreaux]

That's just not true. Consider an annulus (on the sphere or the plane). It's connected but it's complement is not simply connected.

[Geoffrey Irving]

Apologies, one also needs to assume the compact set is connected. I.e., I want that a compact, connected subset of the sphere is simply connected if its complement is connected. In other words, connectedness of the complement upgrades connectedness to simply connectedness.

[Jireh Loreaux]

This feels like it's nearly equivalent to the Jordan curve theorem (is it? I think not), which makes me suspect we don't have it.

[Kyle Miller]

This is an application of Alexander duality, which I don't think we have.

(With the annulus example, the theorem predicts that $H_1$ of the complement is $0$ and $H_0$ of the complement is $\mathbb{Z}^2$. So, while it might not be simply connected, at least its first homology group is right. And, if we had it, a consequence of the Hurewicz theorem would be that each connected component is simply connected.)

[Geoffrey Irving]

@Kyle Miller Thank you (despite the disappointment :))!