The circle is not simply connected

The circle computation π₁(AddCircle p) ≃* Multiplicative ℤ (AddCircle.fundamentalGroupMulEquiv) has an immediate qualitative payoff: since Multiplicative ℤ is nontrivial and infinite, so is the fundamental group of the circle, and therefore the circle is not simply connected. Being non-simply-connected, it is not contractible, and it is not homeomorphic to any simply connected space; in particular the circle is not homeomorphic to the real line nor to any real normed space.

These are the standard topological consequences of π₁(S¹) ≅ ℤ, and they realise the universal-covers roadmap Stage 4 "applications" (TauCetiRoadmap/UniversalCovers/README.md), extending the circle computation (item 12, π₁(S¹) ≅ ℤ) to the classical fact that the circle and the line are topologically distinct.

The nontriviality and infinitude of the fundamental group are transported from Multiplicative ℤ along the circle equivalence. Non-simple-connectivity then 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.

The same consequences for Mathlib's complex unit circle Circle follow from Circle.fundamentalGroupMulEquiv.

Main declarations

• AddCircle.nontrivial_fundamentalGroup, AddCircle.infinite_fundamentalGroup: the fundamental group of AddCircle p (p ≠ 0), at any basepoint, is nontrivial and infinite.
• AddCircle.not_simplyConnectedSpace: AddCircle p is not simply connected.
• AddCircle.not_contractibleSpace: AddCircle p is not contractible.
• AddCircle.isEmpty_homeomorph_of_simplyConnectedSpace, AddCircle.isEmpty_homeomorph_real: AddCircle p is not homeomorphic to a simply connected space, nor to ℝ.
• UnitAddCircle.*: the specialisations to the unit circle S¹ = ℝ ⧸ ℤ.
• Circle.nontrivial_fundamentalGroup, Circle.infinite_fundamentalGroup: the complex unit circle's fundamental group is nontrivial and infinite.
• Circle.not_simplyConnectedSpace, Circle.not_contractibleSpace: the complex unit circle is not simply connected or contractible.
• Circle.isEmpty_homeomorph_real: the complex unit circle is not homeomorphic to ℝ.

theorem AddCircle.nontrivial_fundamentalGroup (p : ℝ) (hp : p ≠ 0) (x : AddCircle p) : Nontrivial (FundamentalGroup (AddCircle p) x)

The fundamental group of the circle AddCircle p (p ≠ 0), based at any point x, is nontrivial. See fundamentalGroupMulEquiv for the full winding-number classification.

theorem AddCircle.infinite_fundamentalGroup (p : ℝ) (hp : p ≠ 0) (x : AddCircle p) : Infinite (FundamentalGroup (AddCircle p) x)

The fundamental group of the circle AddCircle p (p ≠ 0), based at any point x, is infinite. See fundamentalGroupMulEquiv for the full winding-number classification.

theorem AddCircle.nontrivial_fundamentalGroup_zero (p : ℝ) (hp : p ≠ 0) : Nontrivial (FundamentalGroup (AddCircle p) 0)

The fundamental group of the circle AddCircle p (p ≠ 0), based at 0, is nontrivial.

theorem AddCircle.infinite_fundamentalGroup_zero (p : ℝ) (hp : p ≠ 0) : Infinite (FundamentalGroup (AddCircle p) 0)

The fundamental group of the circle AddCircle p (p ≠ 0), based at 0, is infinite.

theorem AddCircle.not_simplyConnectedSpace (p : ℝ) (hp : p ≠ 0) : ¬SimplyConnectedSpace (AddCircle p)

The circle AddCircle p (p ≠ 0) is not simply connected: its fundamental group is nontrivial, whereas a simply connected space has a subsingleton fundamental group.

theorem AddCircle.not_contractibleSpace (p : ℝ) (hp : p ≠ 0) : ¬ContractibleSpace (AddCircle p)

The circle AddCircle p (p ≠ 0) is not contractible: a contractible space is simply connected, and the circle is not.

theorem AddCircle.isEmpty_homeomorph_of_simplyConnectedSpace (p : ℝ) (hp : p ≠ 0) (Y : Type u_1) [TopologicalSpace Y] [SimplyConnectedSpace Y] : IsEmpty (AddCircle p ≃ₜ Y)

The circle AddCircle p (p ≠ 0) is not homeomorphic to any simply connected space: a homeomorphism is in particular a homotopy equivalence, and simple connectivity transfers along homotopy equivalences, which the circle does not enjoy.

theorem AddCircle.isEmpty_homeomorph_real (p : ℝ) (hp : p ≠ 0) : IsEmpty (AddCircle p ≃ₜ ℝ)

The circle AddCircle p (p ≠ 0) is not homeomorphic to the real line: the circle is not simply connected but ℝ is contractible.

theorem UnitAddCircle.nontrivial_fundamentalGroup_zero : Nontrivial (FundamentalGroup UnitAddCircle 0)

The fundamental group of the unit circle S¹ = ℝ ⧸ ℤ, based at 0, is nontrivial.

theorem UnitAddCircle.infinite_fundamentalGroup_zero : Infinite (FundamentalGroup UnitAddCircle 0)

The fundamental group of the unit circle S¹ = ℝ ⧸ ℤ, based at 0, is infinite.

theorem UnitAddCircle.not_simplyConnectedSpace : ¬SimplyConnectedSpace UnitAddCircle

The unit circle S¹ = ℝ ⧸ ℤ is not simply connected.

theorem UnitAddCircle.not_contractibleSpace : ¬ContractibleSpace UnitAddCircle

The unit circle S¹ = ℝ ⧸ ℤ is not contractible.

theorem UnitAddCircle.isEmpty_homeomorph_real : IsEmpty (UnitAddCircle ≃ₜ ℝ)

The unit circle S¹ = ℝ ⧸ ℤ is not homeomorphic to the real line.

theorem Circle.nontrivial_fundamentalGroup (x : Circle) : Nontrivial (FundamentalGroup Circle x)

The fundamental group of the complex unit circle Circle, based at x, is nontrivial. See fundamentalGroupMulEquiv for the full identification with Multiplicative ℤ.

theorem Circle.infinite_fundamentalGroup (x : Circle) : Infinite (FundamentalGroup Circle x)

The fundamental group of the complex unit circle Circle, based at x, is infinite. See fundamentalGroupMulEquiv for the full identification with Multiplicative ℤ.

theorem Circle.not_simplyConnectedSpace : ¬SimplyConnectedSpace Circle

The complex unit circle Circle is not simply connected: its fundamental group is nontrivial, whereas a simply connected space has a subsingleton fundamental group.

theorem Circle.not_contractibleSpace : ¬ContractibleSpace Circle

The complex unit circle Circle is not contractible: a contractible space is simply connected, and the circle is not.

theorem Circle.isEmpty_homeomorph_of_simplyConnectedSpace (Y : Type u_1) [TopologicalSpace Y] [SimplyConnectedSpace Y] : IsEmpty (Circle ≃ₜ Y)

The complex unit circle Circle is not homeomorphic to any simply connected space: a homeomorphism is a homotopy equivalence, and simple connectivity transfers along homotopy equivalences, which the circle does not enjoy.

theorem Circle.isEmpty_homeomorph_real : IsEmpty (Circle ≃ₜ ℝ)

The complex unit circle Circle is not homeomorphic to the real line: the circle is not simply connected but ℝ is contractible.