The degree of a loop in the circle

A loop γ in the unit circle Circle, based at x, lifts along the universal covering Circle.exp : ℝ → Circle, t ↦ e^{it}, to a continuous angle function θ : [0, 1] → ℝ with exp (θ t) = γ t (Mathlib's path lifting, IsCoveringMap.liftPath). Since the loop is closed, θ 1 - θ 0 is an integer multiple of 2π, and since two continuous lifts of the same map differ by a constant, this integer does not depend on the lift. It is the degree (or winding number) Circle.degree γ of the loop: the number of times it runs counterclockwise around the circle.

The degree is characterized by any one continuous lift (Circle.sub_eq_degree_mul and Circle.degree_eq_of_sub_eq), which is how it is computed in practice. It is invariant under homotopies through loops, whose basepoint may move (Circle.degree_eq_of_homotopy), in particular under homotopies of based loops (Circle.degree_eq_of_homotopic). It is additive under the concatenation (Circle.degree_trans) and the pointwise product (Circle.degree_mul) of loops, because angle functions concatenate and add, and reversing a loop negates it (Circle.degree_symm). Raising a loop pointwise to the n-th power multiplies its degree by n (Circle.degree_map_pow).

The degree is the integer that Tau Ceti's identification Circle.fundamentalGroupMulEquiv : π₁(Circle, x) ≃* Multiplicative ℤ assigns to the class of the loop (Circle.fundamentalGroupMulEquiv_fromPath); the lift description is what makes it computable and gives its invariance under free homotopies, changes of basepoint (Circle.degree_symm_trans_trans) and pointwise products. It is the invariant through which the Maslov index of a loop of totally real subspaces is defined.

Main declarations

• Circle.degree: the degree of a loop in the circle.
• Circle.sub_eq_degree_mul: every continuous lift θ of a loop satisfies θ 1 - θ 0 = degree γ * (2 * π).
• Circle.degree_eq_of_homotopy: the degree is invariant under free homotopies of loops.
• Circle.degree_symm_trans_trans: the degree is invariant under change of basepoint.
• Circle.degree_trans, Circle.degree_symm: the degree of a concatenation of loops is the sum of the degrees, and reversing a loop negates its degree.
• Circle.degree_mul: the degree of a pointwise product of loops is the sum of the degrees.
• Circle.degree_map_pow: the pointwise n-th power of a loop has n times its degree.

noncomputable def Circle.degree {x : Circle} (γ : Path x x) : ℤ

The degree of a loop γ in the circle: the integer n such that every continuous angle function θ of the loop, exp (θ t) = γ t, satisfies θ 1 - θ 0 = n * (2 * π). It counts how many times the loop runs counterclockwise around the circle.

Equations

• Circle.degree γ = ⋯.choose

theorem Circle.sub_eq_degree_mul {x : Circle} (γ : Path x x) {θ : ↑unitInterval → ℝ} (hθ : Continuous θ) (hθγ : ∀ (t : ↑unitInterval), exp (θ t) = γ t) : θ 1 - θ 0 = ↑(degree γ) * (2 * Real.pi)

Every continuous lift θ of a loop γ along Circle.exp changes by degree γ full turns: θ 1 - θ 0 = degree γ * (2 * π).

theorem Circle.degree_eq_of_sub_eq {x : Circle} (γ : Path x x) {θ : ↑unitInterval → ℝ} (hθ : Continuous θ) (hθγ : ∀ (t : ↑unitInterval), exp (θ t) = γ t) {n : ℤ} (hn : θ 1 - θ 0 = ↑n * (2 * Real.pi)) : degree γ = n

The degree of a loop can be read off from any one continuous lift.

@[simp]

theorem Circle.degree_refl (x : Circle) : degree (Path.refl x) = 0

The constant loop has degree zero.

theorem Circle.degree_eq_of_homotopy {x y : Circle} (γ₀ : Path x x) (γ₁ : Path y y) (F : C(↑unitInterval × ↑unitInterval, Circle)) (h₀ : ∀ (t : ↑unitInterval), F (0, t) = γ₀ t) (h₁ : ∀ (t : ↑unitInterval), F (1, t) = γ₁ t) (hF : ∀ (s : ↑unitInterval), F (s, 0) = F (s, 1)) : degree γ₀ = degree γ₁

Homotopy invariance of the degree. If F is a homotopy from the loop γ₀ to the loop γ₁ through loops (F (s, 0) = F (s, 1) for every s; the basepoint may move), then the two loops have the same degree.

theorem Circle.degree_eq_of_homotopic {x : Circle} {γ₀ γ₁ : Path x x} (h : γ₀.Homotopic γ₁) : degree γ₀ = degree γ₁

Homotopic loops, relative to their basepoint, have the same degree.

@[simp]

theorem Circle.degree_trans {x : Circle} (γ₁ γ₂ : Path x x) : degree (γ₁.trans γ₂) = degree γ₁ + degree γ₂

The degree of the concatenation of two loops is the sum of their degrees.

@[simp]

theorem Circle.degree_symm {x : Circle} (γ : Path x x) : degree γ.symm = -degree γ

Reversing a loop negates its degree.

theorem Circle.degree_symm_trans_trans {x y : Circle} (γ : Path x x) (p : Path x y) : degree (p.symm.trans (γ.trans p)) = degree γ

Conjugating a loop by a path does not change its degree: p⁻¹ ⬝ γ ⬝ p has the degree of γ. This is the invariance of the degree under change of basepoint.

@[simp]

theorem Circle.degree_mul {x y : Circle} (γ₁ : Path x x) (γ₂ : Path y y) : degree (γ₁.mul γ₂) = degree γ₁ + degree γ₂

The degree of the pointwise product of two loops is the sum of their degrees.

@[simp]

theorem Circle.degree_map_pow {x : Circle} (γ : Path x x) (n : ℕ) : degree (γ.map ⋯) = ↑n * degree γ

The pointwise n-th power of a loop has n times its degree.