Consequences of a space not being simply connected

A space whose fundamental group at some basepoint is nontrivial is not simply connected, and a non-simply-connected space inherits the standard topological obstructions: it is not contractible, and it is not homeomorphic to any simply connected space — in particular not to any real topological vector space nor to ℝ.

These facts use the space only through the (non-)triviality of its fundamental group, so they are stated once here for an arbitrary space and then specialised to concrete circles (AddCircle.*, UnitAddCircle.*, Circle.*). Non-simple-connectivity follows because a simply connected space has a subsingleton fundamental group; the homeomorphism statements consume Mathlib's transfer of SimplyConnectedSpace along a homotopy equivalence (ContinuousMap.HomotopyEquiv.simplyConnectedSpace, via Homeomorph.toHomotopyEquiv) and the contractibility of a real topological vector space (RealTopologicalVectorSpace.contractibleSpace). No Mathlib code is vendored.

Main declarations

• TauCeti.not_simplyConnectedSpace_of_nontrivial_fundamentalGroup: a space with a nontrivial fundamental group at some basepoint is not simply connected.
• TauCeti.not_contractibleSpace_of_not_simplyConnectedSpace: a non-simply-connected space is not contractible.
• TauCeti.isEmpty_homeomorph_of_not_simplyConnectedSpace, TauCeti.isEmpty_homeomorph_real_of_not_simplyConnectedSpace: a non-simply-connected space is not homeomorphic to a simply connected space, or to ℝ.

theorem TauCeti.not_simplyConnectedSpace_of_nontrivial_fundamentalGroup {X : Type u_1} [TopologicalSpace X] (x : X) [Nontrivial (FundamentalGroup X x)] : ¬SimplyConnectedSpace X

A space with a nontrivial fundamental group at some basepoint is not simply connected: a simply connected space has a subsingleton fundamental group.

theorem TauCeti.not_contractibleSpace_of_not_simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] (h : ¬SimplyConnectedSpace X) : ¬ContractibleSpace X

A not simply connected space is not contractible: a contractible space is simply connected.

theorem TauCeti.isEmpty_homeomorph_of_not_simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] (h : ¬SimplyConnectedSpace X) (Y : Type u_2) [TopologicalSpace Y] [SimplyConnectedSpace Y] : IsEmpty (X ≃ₜ Y)

A not simply connected space is not homeomorphic to any simply connected space: a homeomorphism is in particular a homotopy equivalence, and simple connectivity transfers along homotopy equivalences.

theorem TauCeti.isEmpty_homeomorph_real_of_not_simplyConnectedSpace {X : Type u_1} [TopologicalSpace X] (h : ¬SimplyConnectedSpace X) : IsEmpty (X ≃ₜ ℝ)

A not simply connected space is not homeomorphic to the real line: ℝ is contractible, hence simply connected.