Dependencies

Given a continuous map \(\psi \colon S^1\to X\), its associated loop is obtained by precomposing with the standard parametrization \(t\mapsto \exp (2\pi i t)\) of the circle on \(I\).

def circleLoop
    [TopologicalSpace X] (f : C(Circle, X)) :
    Path (f 1) (f 1)

A homotopy of circle maps induces a homotopy of the associated loops by precomposing with the standard circle parametrization.

def circleLoopHomotopy
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : f.Homotopy g) :
    C(I × I, X)

The induced homotopy of associated loops is a homotopy through loops.

theorem circleLoopHomotopy_isLoopHomotopy
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : f.Homotopy g) :
    ContinuousMap.IsLoopHomotopy
    (circleLoopHomotopy H)

At the right endpoint of the homotopy parameter, the induced loop homotopy recovers the associated loop of the terminal map.

theorem circleLoopHomotopy_one_left
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : f.Homotopy g) (t : I) :
    circleLoopHomotopy H (1, t) =
    (ContinuousMap.circleLoop g) t

At the left endpoint of the homotopy parameter, the induced loop homotopy recovers the associated loop of the initial map.

theorem circleLoopHomotopy_zero_left
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : f.Homotopy g) (t : I) :
    circleLoopHomotopy H (0, t) =
    (ContinuousMap.circleLoop f) t

Given \(a,c\in \mathbb {C}^\times \) and \(n\in \mathbb N\), define the circle map \(z\mapsto a\, (cz)^n\) with values in \(\mathbb {C}^\times \).

noncomputable def circleScaledMonomial
    (a c : ℂˣ) (n : ℕ) :
    C(Circle, ℂˣ)

The winding number of the map \(z\mapsto a\, (cz)^n\) on the unit circle is \(n\).

theorem circleScaledMonomial_windingNumber
    (a c : ℂˣ) (n : ℕ) :
    ContinuousMap.windingNumber
    (circleScaledMonomial a c n) = (n : ℤ)

The canonical inclusion of the unit circle into the closed unit disk.

abbrev toDisk :
    Circle → Disk

The winding number of a continuous map from the circle to \(\mathbb {C}^\times \) is the winding number of its associated loop.

noncomputable def windingNumber
    (f : C(Circle, ℂˣ)) :
    ℤ

A constant map from the circle to \(\mathbb {C}^\times \) has winding number zero.

theorem windingNumber_const
    (c : ℂˣ) :
    windingNumber (ContinuousMap.const _ c :
    C(Circle, ℂˣ)) = 0

Homotopic circle maps into \(\mathbb {C}^\times \) have the same winding number.

theorem windingNumber_eq_of_homotopy
    {f g : C(Circle, ℂˣ)}
    (H : f.Homotopy g) :
    windingNumber f = windingNumber g

Circle maps satisfying the walking-dog inequality have the same winding number.

theorem windingNumber_eq_of_norm_sub_lt
    {f g : C(Circle, ℂˣ)}
    (hclose :
      ∀ z : Circle, ‖(f z : ℂ) - g z‖ <
        ‖(f z : ℂ)‖) :
    windingNumber f = windingNumber g

If a map from the unit circle to \(\mathbb {C}^\times \) extends to the closed unit disk through maps into \(\mathbb {C}^\times \), then its winding number is zero.

theorem windingNumber_eq_zero_of_exists_extension
    {f : C(Circle, ℂˣ)}
    {F : C(Disk, ℂˣ)}
    (hF :
      ∀ z : Circle,
        F z = f z) :
    windingNumber f = 0

The closed unit disk in the complex plane.

abbrev Disk : Type := Submonoid.unitClosedBall ℂ

Two lifts of the same path differ by a constant integral multiple of \(2\pi i\).

theorem eq_add_int_mul_two_pi_I_of_lifts
    {u₀ u₁ : ℂˣ} (γ : Path u₀ u₁)
    (Γ₀ Γ₁ : C(I, ℂ))
    (hΓ₀ : ∀ t, exp (Γ₀ t) = γ t)
    (hΓ₁ : ∀ t, exp (Γ₁ t) = γ t) :
    ∃ n : ℤ, ∀ t, Γ₁ t =
    Γ₀ t + n * (2 * π * 𝓲)

Any other lift of the same path with the same starting point agrees with the canonical lifted path.

theorem eq_expLift
    {u₀ u₁ : ℂˣ} (γ : Path u₀ u₁) (w0 : ℂ)
    (hw0 : exp w0 = u₀)
    (Γ : C(I, ℂ))
    (hlift : ∀ t, exp (Γ t) = γ t)
    (h0 : Γ 0 = w0) :
    Γ = Path.expLift γ w0 hw0

Equivalently, the leading-term domination estimate holds eventually along the filter \(R\to +\infty \).

theorem eventually_leadingTerm_dominates_on_circle
    (p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
    ∀ᶠ R : ℝ in Filter.atTop, ∀ z : Circle,
      ‖p.eval ((R : ℂ) * z) -
        p.leadingCoeff * (((R : ℂ) * z) ^
          p.natDegree)‖ <
        ‖p.leadingCoeff * (((R : ℂ) * z) ^
          p.natDegree)‖

For all sufficiently large \(R\), the restriction of a nonconstant polynomial to the circle of radius \(R\) has winding number equal to the degree of the polynomial.

theorem eventually_windingNumber_eq_natDegree
    (p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
    ∀ᶠ R : ℝ in Filter.atTop,
      ∃ f : C(Circle, ℂˣ), (∀ z, f z = p.eval
      ((R : ℂ) * z)) ∧ ContinuousMap.windingNumber f
      = (p.natDegree : ℤ)

If two maps into \(\Bbbk ^\times \) satisfy the walking-dog inequality \(\lVert f(x)-g(x)\rVert {\lt} \lVert f(x)\rVert \) pointwise, then they are homotopic through maps into \(\Bbbk ^\times \).

theorem exists_homotopy_of_norm_sub_lt
    [TopologicalSpace α] [RCLike 𝕜]
    {f g : C(α, 𝕜ˣ)}
    (hclose :
      ∀ z : α, ‖(f z : 𝕜) - g z‖ <
        ‖(f z : 𝕜)‖) :
    Nonempty (f.Homotopy g)

Every nonconstant complex polynomial has a complex root.

theorem exists_root_of_natDegree_pos
    (p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
    ∃ z : ℂ, p.IsRoot z

Given a path in \(\mathbb {C}^\times \) and a chosen logarithm of its starting point, lift the path through the exponential covering map.

noncomputable def expLift
    {u₀ u₁ : ℂˣ} (γ : Path u₀ u₁) (w0 : ℂ)
    (hw0 : exp w0 = u₀) :
    C(I, ℂ)

The lifted path projects back to the original path under the exponential map.

theorem expLift_apply
    {u₀ u₁ : ℂˣ} (γ : Path u₀ u₁) (w0 : ℂ)
    (hw0 : exp w0 = u₀) (t : I) :
    exp (Path.expLift γ w0 hw0 t) =
    γ t

A homotopy \(H\colon I\times I\to X\) is a homotopy through loops if each horizontal slice has the same initial and terminal point.

def IsLoopHomotopy
    [TopologicalSpace X] (H : C(I × I, X)) :
    Prop

For a nonconstant complex polynomial, there is a radius beyond which the leading term dominates the sum of the lower terms on every circle of larger radius.

theorem leadingTerm_dominates_on_circle
    (p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
    ∃ R0 : ℝ, 0 < R0 ∧ ∀ R : ℝ, R0 ≤ R →
    ∀ z : Circle, ‖p.eval ((R : ℂ) * z) -
    p.leadingCoeff * (((R : ℂ) * z) ^
    p.natDegree)‖ < ‖p.leadingCoeff * (((R : ℂ) *
    z) ^ p.natDegree)‖

The winding number of a loop in \(\mathbb {C}^\times \) is defined from the endpoint difference of a lift through the exponential covering map.

noncomputable def windingNumber
    {u : ℂˣ} (γ : Path u u) :
    ℤ

Loops in \(\mathbb {C}^\times \) that are freely homotopic through loops have the same winding number.

theorem windingNumber_eq_of_homotopy
    {u u' : ℂˣ} (γ : Path u u)
    (γ' : Path u' u') (H : C(I × I, ℂˣ))
    (hhom : ContinuousMap.IsLoopHomotopy H)
    (hzero : ∀ t, H (0, t) = γ t)
    (hone : ∀ t, H (1, t) = γ' t) :
    Path.windingNumber γ = Path.windingNumber γ'

If \(\Gamma \) is any lift of a loop in \(\mathbb {C}^\times \), then the endpoint quotient \((\Gamma (1)-\Gamma (0))/(2\pi i)\) computes the winding number.

theorem windingNumber_eq_of_lift
    {u : ℂˣ} (γ : Path u u) (Γ : C(I, ℂ))
    (hlift : ∀ t, exp (Γ t) = γ t) :
    (Γ 1 - Γ 0) / (2 * π * 𝓲) =
    Path.windingNumber γ

The constant loop has winding number zero.

theorem windingNumber_refl
    (u : ℂˣ) :
    Path.windingNumber (Path.refl u) = 0