The fundamental group of the circle

Category: 1-Mathlib (CSD-free).

Mathlib has the whole covering-space apparatus — path lifting, the monodromy theorem, the monodromy permutation representation, and IsAddQuotientCoveringMap.fundamentalGroupEquiv, which identifies the fundamental group of the base of a simply-connected quotient covering with the (opposite of the) deck group. It also has Circle.isAddQuotientCoveringMap_exp, exhibiting Circle.exp : ℝ → Circle as exactly such a covering with deck group 2πℤ. What it does not state anywhere is the classical consequence, that the circle's fundamental group is ℤ and in particular is nontrivial.

This module supplies it. Everything here is a short application of the two results above; the mathematical work was already done upstream.

• Circle.fundamentalGroupEquivZMultiples — π₁(S¹) ≃* (2πℤ)ᵐᵒᵖ, written multiplicatively.
• ★ Circle.fundamentalGroup_nontrivial — the circle's fundamental group is nontrivial. This is the form downstream obstruction arguments consume: a loop-exchange acting nontrivially on π₁ cannot be joined to the identity.
• Circle.not_simplyConnectedSpace — the circle is not simply connected.

Why this is here

It is the first brick of the relocation-generation obstruction (specs/BACKLOG.md): a time-one map of a flow is homotopic to the identity, so it acts trivially on π₁, whereas exchanging two identical factors of a product arena does not. That argument needs one nontrivial fundamental group to run against, and the record arenas' torus factors supply it.

References

Mathlib/Topology/Homotopy/Lifting.lean (fundamentalGroupEquiv, monodromy_theorem); Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean (isAddQuotientCoveringMap_exp); specs/future-work.md; MATHLIB-GAPS.md.

def Circle.expFibreZero : ↑(⇑exp ⁻¹' {1})

The basepoint 0 : ℝ lies in the fibre of Circle.exp over 1.

Equations

• Circle.expFibreZero = ⟨0, Circle.expFibreZero._proof_1⟩

@[simp]

theorem Circle.expFibreZero_val : ↑expFibreZero = 0

noncomputable def Circle.fundamentalGroupEquivZMultiples : FundamentalGroup Circle 1 ≃* (Multiplicative ↥(AddSubgroup.zmultiples (2 * Real.pi)))ᵐᵒᵖ

The fundamental group of the circle is its deck group. Circle.exp is a quotient covering with deck group 2πℤ and simply-connected total space ℝ, so the upstream fundamentalGroupEquiv applies verbatim.

Equations

• Circle.fundamentalGroupEquivZMultiples = Circle.isAddQuotientCoveringMap_exp.fundamentalGroupEquiv Circle.expFibreZero

theorem Circle.nontrivial_zmultiples_two_pi : Nontrivial ↥(AddSubgroup.zmultiples (2 * Real.pi))

The deck group 2πℤ is nontrivial, since 2π ≠ 0.

theorem Circle.fundamentalGroup_nontrivial : Nontrivial (FundamentalGroup Circle 1)

★ The circle's fundamental group is nontrivial. The classical fact, here a transport of nontrivial_zmultiples_two_pi along the deck-group equivalence.

This is the form the obstruction arguments consume: any self-map joined to the identity by a flow induces the identity on π₁, so a map inducing a nonidentity automorphism is not a time-one flow map.

theorem Circle.not_simplyConnectedSpace : ¬SimplyConnectedSpace Circle

The circle is not simply connected. A simply connected space has subsingleton fundamental group, which contradicts fundamentalGroup_nontrivial.

theorem Circle.not_contractibleSpace : ¬ContractibleSpace Circle

★ The circle is not contractible. A contractible space is simply connected (SimplyConnectedSpace.ofContractible).

theorem AddCircle.not_contractibleSpace {T : ℝ} (hT : T ≠ 0) : ¬ContractibleSpace (AddCircle T)

★ The additive circle is not contractible, for any nonzero period, transported from Circle.not_contractibleSpace along AddCircle.homeomorphCircle. This is the form the record arenas consume, since LF4.KTorus is a product of copies of AddCircle 1.