The fundamental group of the circle

For 0 < p, the fundamental group of AddCircle p at any basepoint is isomorphic to ℤ (AddCircle.windingNumberIso). The winding number AddCircle.windingNumber of a loop is (f 1 - f 0) / p for any continuous lift f : I → ℝ of the loop (AddCircle.windingNumber_eq_div); in particular the loop t ↦ n • (t * p) + x has winding number n (AddCircle.windingNumber_zsmulLoop).

def AddCircle.zsmulLoop (p x : ℝ) (n : ℤ) : Path ↑x ↑x

The loop in AddCircle p based at x that winds n times, defined as t ↦ n • (t * p) + x.

Equations

• AddCircle.zsmulLoop p x n = { toFun := fun (t : ↑unitInterval) => n • ↑(↑t * p) + ↑x, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }

@[simp]

theorem AddCircle.zsmulLoop_apply (p x : ℝ) (n : ℤ) (t : ↑unitInterval) : (zsmulLoop p x n) t = n • ↑(↑t * p) + ↑x

noncomputable def AddCircle.windingNumberIso {p : ℝ} [hp : Fact (0 < p)] (x : AddCircle p) : FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ

The fundamental group of the circle is ℤ: the isomorphism sends the class of a loop to its winding number (windingNumber_eq_div). It does not depend on the choice of a lift of the basepoint (IsAddQuotientCoveringMap.fundamentalGroupEquiv_eq).

Equations

• x.windingNumberIso = (⋯.fundamentalGroupEquiv ⟨↑((AddCircle.equivIco p 0) x), ⋯⟩).trans (MulOpposite.opMulEquiv.symm.trans (AddEquiv.toMultiplicative (AddSubgroup.zmultiplesEquivInt ⋯)))

noncomputable def AddCircle.windingNumber {p : ℝ} [hp : Fact (0 < p)] {x : AddCircle p} (γ : FundamentalGroup (AddCircle p) x) : ℤ

The winding number of a loop in AddCircle p, defined as its image under windingNumberIso.

Equations

• AddCircle.windingNumber γ = Multiplicative.toAdd (x.windingNumberIso γ)

theorem AddCircle.windingNumber_eq_div {p : ℝ} [hp : Fact (0 < p)] {x : AddCircle p} (γ : Path x x) (f : C(↑unitInterval, ℝ)) (hf : QuotientAddGroup.mk ∘ ⇑f = ⇑γ) : ↑(windingNumber (Path.Homotopic.Quotient.mk γ)) = (f 1 - f 0) / p

The winding number of a loop in AddCircle p is (f 1 - f 0) / p, for any continuous lift f of the loop to ℝ.

theorem AddCircle.windingNumber_zsmulLoop {p : ℝ} [hp : Fact (0 < p)] (x : ℝ) (n : ℤ) : windingNumber (Path.Homotopic.Quotient.mk (zsmulLoop p x n)) = n

The loop t ↦ n • (t * p) + x has winding number n.