Dependencies

If a map \(\rho \colon S^1\to \Cstar \) extends to a map from the closed disk to \(\Cstar \), then its winding number is zero.

Let \(\rho \colon S^1\to \mathbb {C}\) be a map with \(\rho (z)\in Cstar\) for all \(z\in S^1\). Suppose there is a map \(\hat f\colon D^2\to \mathbb {C}\) with \(\hat f|_{S^1}=\rho \) and with the image of \(\hat f\) contained in \(Cstar\). Then the winding \(w(\rho )=0\).

The associated loop evaluates at \(t\in I\) as \(\psi (\exp (2\pi i t))\).

theorem circleLoop_apply
    [TopologicalSpace X] (f : C(Circle, X))
    (t : I) :
    (ContinuousMap.circleLoop f) t =
    f (Circle.exp (2 * Real.pi * (t : ℝ)))

The induced homotopy evaluates by the expected formula \(\widehat H(s,t)=H(s,\exp (2\pi i t))\).

theorem circleLoopHomotopy_apply
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : ContinuousMap.Homotopy f g) (x : I × I) :
    circleLoopHomotopy H x =
    H (x.1, Circle.exp (2 * Real.pi * (x.2 : ℝ)))

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

theorem circleLoopHomotopy_isLoopHomotopy
    [TopologicalSpace X] {f g : C(Circle, X)}
    (H : ContinuousMap.Homotopy f 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 : ContinuousMap.Homotopy f 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 : ContinuousMap.Homotopy f g) (t : I) :
    circleLoopHomotopy H (0, t) =
    (ContinuousMap.circleLoop f) t

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 : ContinuousMap.Homotopy f g) :
    C(I × I, X)

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)

For \(R{\gt}0\), the winding number of the map \(z\mapsto a\, (Rz)^n\) on the unit circle is \(n\).

theorem circleMonomial_windingNumber
    (a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R) :
    ContinuousMap.windingNumber (circleMonomial a
    n R hR) = (n : ℤ)

For \(R{\gt}0\), the map \(z\mapsto a\, (Rz)^n\) is obtained by specializing the previous construction to the nonzero scalar \(R\).

noncomputable def circleMonomial
    (a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R) :
    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 : ℤ)

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 canonical inclusion of the unit circle into the closed unit disk.

abbrev toClosedUnitDisk :
    Circle → Metric.closedBall (0 : ℂ) 1

The canonical inclusion \(S^1\hookrightarrow D^2\) sends a point of the unit circle to the same complex number, now viewed as a point of the closed disk.

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

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 : ContinuousMap.Homotopy f 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(Metric.closedBall (0 : ℂ) 1, ℂˣ)}
    (hF :
      ∀ z : Circle,
        F (Circle.toClosedUnitDisk z) = f z) :
    windingNumber f = 0

The same vanishing result holds for extensions valued in the nonzero-complex subtype, after transporting through the units/nonzero bridge.

theorem windingNumber_eq_zero_of_exists_extension'
    {f : C(Circle, ℂˣ)}
    {F : C(Metric.closedBall (0 : ℂ) 1,
      {z : ℂ // z ≠ 0})}
    (hF :
      ∀ z : Circle,
        F (Circle.toClosedUnitDisk z) =
          ContinuousMap.toNonzeroSubtype f z) :
    windingNumber f = 0

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, ℂˣ)) :
    ℤ

After coercing to \(\mathbb {C}\), the circle monomial evaluates as \(a\, (Rz)^n\).

theorem coe_circleMonomial_apply
    (a : ℂˣ) (n : ℕ) (R : ℝ) (hR : 0 < R)
    (z : Circle) :
    ((circleMonomial a n R hR z : ℂˣ) : ℂ) =
    a * (((R : ℂ) * z) ^ n)

After coercing to \(\mathbb {C}\), the scaled monomial has the expected pointwise formula \(a\, (cz)^n\).

theorem coe_circleScaledMonomial_apply
    (a c : ℂˣ) (n : ℕ) (z : Circle) :
    ((circleScaledMonomial a c n z : ℂˣ) : ℂ) =
    a * (((c : ℂ) * z) ^ n)

After coercing to \(\mathbb {C}\), the map obtained by passing from the nonzero subtype to units has the same values as the original map.

theorem coe_fromNonzeroSubtype_apply
    [TopologicalSpace α] (f : C(α, Cstar)) (x : α)
    :
    ((ContinuousMap.fromNonzeroSubtype f x : ℂˣ) :
    ℂ) = (f x : ℂ)

After coercing to \(\mathbb {C}\), the circle-valued units map evaluates as \(p(Rz)\).

theorem coe_mapCircleUnits_apply
    (p : Polynomial ℂ) (R : ℝ)
    (hR : ∀ z : Circle, p.eval ((R : ℂ) * z) ≠ 0)
    (z : Circle) :
    ((Polynomial.mapCircleUnits p R hR z : ℂˣ) :
    ℂ) = p.eval ((R : ℂ) * z)

After coercing to \(\mathbb {C}\), the disk-valued units map evaluates as \(p(Rz)\).

theorem coe_mapClosedUnitDiskUnits_apply
    (p : Polynomial ℂ) (R : ℝ)
    (hR :
      ∀ z : Metric.closedBall (0 : ℂ) 1,
        p.eval ((R : ℂ) * z) ≠ 0)
    (z : Metric.closedBall (0 : ℂ) 1) :
    ((Polynomial.mapClosedUnitDiskUnits p R hR z :
    ℂˣ) : ℂ) = p.eval ((R : ℂ) * z)

After forgetting the subtype, the sphere-to-ball inclusion is the identity on points.

theorem coe_sphereToClosedBall
    [PseudoMetricSpace α]
    (x : α) (r : ℝ) (y : Metric.sphere x r) :
    sphereToClosedBall x r y = y

After forgetting the subtype, the inclusion of the circle into the closed disk does not change the underlying complex number.

theorem coe_toClosedUnitDisk (z : Circle) :
    ((toClosedUnitDisk z :
      Metric.closedBall (0 : ℂ) 1) : ℂ) = z

After coercing to \(\mathbb {C}\), the map obtained by passing from units to the nonzero subtype has the same values as the original map.

theorem coe_toNonzeroSubtype_apply
    [TopologicalSpace α] (f : C(α, ℂˣ)) (x : α) :
    (ContinuousMap.toNonzeroSubtype f x : ℂ) =
    (f x : ℂ)

Suppose \(f\colon E\to X\) is a map between topological spaces and \(\varphi \colon X\to X\), \(\tilde\varphi \colon E\to E\) are homeomorphisms such that \(f\circ \tilde\varphi =\varphi \circ f\). Then also \(f\circ \tilde\varphi ^{-1}=\varphi ^{-1}\circ f\).

Internally, we identify \(\mathbb {C}^\times \) (as the group of units in \(\mathbb {C}\)) with the subtype of nonzero complex numbers.

def complexUnitsHomeomorphNeZero :
    ℂˣ ≃ₜ Cstar

Suppose that \(\omega \colon [ a, b ]\to \mathbb {C}\) is a loop and \(\omega (t)\in Cstar\) for all \(t\in [ a, b ]\). Suppose that \(H\colon [ a, b ]\times [ 0, 1 ]\to \mathbb {C}\) is a homotopy of loops from \(\omega \) to a constant loop and \(H(t,s)\in Cstar\) for all \((t,s)\in [ a, b ]\times [ 0, 1 ]\). Then the winding number of \(\omega \) is zero.

If \(f\colon S^1\to \mathbb {C}\) is a constant map to a point \(z\in Cstar\), then \(w(f)=0\).

If \(f\colon S^1\to \Cstar \) is constant, then its winding number is zero.

Let \(\omega \colon [ a, b]\to \mathbb {C}\) be a loop with \(\omega (t)\in Cstar\) for all \(t\in [ a, b]\). There is a lift \(\tilde\omega \colon [ a, b]\to \mathbb {C}\) of \(\omega \) through \(CSexp\). There is a constant \(w(\omega )\in \mathbb {Z}\) such that for every lift \(\tilde\omega \colon [ a, b]\to \mathbb {C}\) the winding number of \(\tilde\omega \) is \(w(\omega )\).

\(CSexp\colon \mathbb {C}\to \mathbb {C}\) is continuous.

The map \(w\mapsto \left\lfloor \frac{\Im (w)+\pi }{2\pi }\right\rfloor \) is continuous on \(\tilde S\).

If a map into \(\mathbb Z\) is continuous after coercion to \(\mathbb {C}\), then it is continuous.

\(PBlog\) is continuous on \(T\) and if \(z\in T\) then \(PBlog(z)\in \{ z\in \mathbb {C}|-\pi {\lt} Im(z) {\lt} \pi \} \).

\(CSexp\colon \mathbb {C}\to \mathbb {C}\) defined by the usual power series.

For every \(x\in \mathbb {C}\), one has \(CSexp(\tilde\varphi ^{-1}_{\mathbb {C}}(x))=CSexp(x)\).

Let

be the map obtained from \(CSexp\) by regarding \(CSexp(z)\) as an element of \(Cstar\).

For every \(z\in \mathbb {C}\), forgetting that \(CSexpCstar(z)\) lies in \(Cstar\) gives back \(CSexp(z)\).

The map \(CSexpCstar\colon \mathbb {C}\to Cstar\) is a covering map.

For \(w\in S\), \(CSexp(w)\in T\).

\(Cstar=\{ z\in \mathbb {C}| z\not= 0\} \)

We use the local notation ‘Cstar‘ to refer to the subtype of nonzero complex numbers.

local notation "Cstar" => {z : ℂ // z ≠ 0}

Let \(D^2=\{ z\in \mathbb {C}: |z|\le 1\} \) be the closed unit disk.

The closed unit disk in \(\mathbb {C}\).

Let \(f\colon X\to Y\) be a continuous map between topological spaces and \(\alpha \colon A\to Y\) a continuous map. A lift of \(\alpha \) through \(f\) is a continuous map \(\tilde\alpha \colon A\to X\) such that \(f\circ \tilde\alpha = \alpha \).

There is a map \(PBlog\colon \mathbb {C}\to \mathbb {C}\).

Given a map of the circle \(\psi \colon S^1\to X\) the associated loop is \(\omega \colon [ 0, 2\pi ]\to X\) defined by \(\omega (t)=\psi (CSexp(it))\).

Given a map of the circle \(\psi \colon S^1\to X\) the associated loop is \(\omega \colon [ 0, 2\pi ]\to X\) defined by \(\omega (t)=\psi (CSexp(it))\).

For every circle map \(\psi \), the associated path begins and ends at the same point, so it is a loop.

The path associated with a circle map is a loop.

For any \(a, b\in \mathbb {R}\) (in practice, we assume \(a {\lt} b\)), we define \(S(a,b)=\{ z\in \mathbb {C}| a {\lt} Im{z} {\lt} b\} \).

\(\tilde S\subset \mathbb {C}\) is the subset \(\{ r+\theta * I|r,\theta \in \mathbb {R}\text{\ and\ } \theta \not= (2k+1)\pi \text{ for any } k\in \mathbb {Z}\} \).

Let \(\widetilde{PBlog}\colon T\times \mathbb {Z}\to S\times \mathbb {Z}\) be defined by \(\widetilde{PBlog}(z,n)=(PBlog(z),n)\) for all \(z\in T\) and \(n\in \mathbb {Z}\).

Suppose given a loop \(\omega \colon a\colon [a, b]\to \mathbb {C}\) with \(\omega (t)\in Cstar\) for all \(t\in [a, b]\), and given a lift \(\tilde\omega \) of \(\omega \) through \(CSexp\) the winding number of the lift \(\tilde\omega \), denoted \(w(\tilde\omega )\), is \((\tilde\omega _x(b)-\tilde\omega _x(a))/2\pi *I\).

The winding number of a map \(\rho \colon S^1\to \mathbb {C}\) with \(\rho (z)\in Cstar\) for all \(z\in S^1\) is the winding number of the associated loop.

The winding number of a map \(\rho \colon S^1\to \Cstar \) is the winding number of the associated loop.

Let \(\omega \colon [a, b]\to \mathbb {C}\) be continuous with \(\omega (t)\in Cstar\) for all \(t\in [a ,b]\). Suppose that \(\tilde\omega \) and \(\tilde\omega '\) are lifts of \(\omega \) through \(CSexp\). Then DefWNlift\((\tilde\omega )\in \mathbb {Z}\) and DefWNlift\((\tilde\omega ')=\)DefWNlift\((\tilde\omega )\).

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
    {z₀ z₁ : Cstar} (γ : Path z₀ z₁)
    (Γ₀ Γ₁ : C(I, ℂ))
    (hΓ₀ : ∀ t, Complex.exp (Γ₀ t) = (γ t : ℂ))
    (hΓ₁ : ∀ t, Complex.exp (Γ₁ t) = (γ t : ℂ)) :
    ∃ n : ℤ, ∀ t, Γ₁ t =
    Γ₀ t + n * (2 * Real.pi * Complex.I)

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

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

If \(\omega \colon [ a, b ]\to \mathbb {C}\) and \(\omega '\colon [ a, b ]\to \mathbb {C}\) are loops with \(\omega (t) , \omega '(t) \in Cstar\) for all \(t\in [ a, b ]\) and if \(H\colon [ a, b ]\times [ 0, 1 ]\to \mathbb {C}\) is a homotopy of loops from \(\omega \) to \(\omega '\) with \(H(t,s)\in Cstar\) for all \(t\in [ a, b ]\) and \(s\in [ 0, 1 ]\), then \(w(\omega )=w(\omega ')\)

for \(r,\theta \in \mathbb {R}\).

For 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) :
    ∃ R0 : ℝ, 0 < R0 ∧ ∀ R : ℝ, R0 ≤ R →
    ∃ f : C(Circle, ℂˣ), (∀ z, (f z : ℂ) = p.eval
    ((R : ℂ) * z)) ∧ ContinuousMap.windingNumber f
    = (p.natDegree : ℤ)

Let \(\omega \colon [a, b]\to \mathbb {C}\) be a loop. Assume that \(\omega (t)\in Cstar\) for all \(t\in [a, b]\). There is a lift of \(\omega \) through \(exp\).

Every nonconstant complex polynomial has a complex root.

Every complex polynomial of degree \(k{\gt}0\) has a complex root.

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 (ContinuousMap.Homotopy f 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

Adding an integral multiple of \(2\pi i\) does not change the exponential.

theorem exp_add_int_mul_two_pi_I_eq
    (z : ℂ) (n : ℤ) :
    Complex.exp (z + n * (2 * Real.pi *
    Complex.I)) = Complex.exp z

\(CSexp\colon \mathbb {C}\to \mathbb {C}\) is a covering projection over \(Cstar\) with source \(\mathbb {C}\). The image of \(CSexp\) is \(Cstar\).

Let \(A\) be a topological space, let \(H\colon [0,1]\times A\to Cstar\) be continuous, and let \(f\colon A\to \mathbb {C}\) be continuous. Assume that

for all \(a\in A\). Then there is a unique continuous map

such that \(\tilde H(0,a)=f(a)\) for all \(a\in A\) and \(CSexp(\tilde H(t,a))=H(t,a)\) for all \((t,a)\in [0,1]\times A\).

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

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

The lifted path starts at the prescribed basepoint.

theorem expLift_zero
    {z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
    (hw0 : Complex.exp w0 = (z₀ : ℂ)) :
    Path.expLift γ w0 hw0 0 = w0

Given a path in \(\mathbb {C}\setminus \{ 0\} \) and a chosen logarithm of its starting point, lift the path through the covering map \(\exp \colon \mathbb {C}\to \mathbb {C}\setminus \{ 0\} \).

noncomputable def expLift
    {z₀ z₁ : Cstar} (γ : Path z₀ z₁) (w0 : ℂ)
    (hw0 : Complex.exp w0 = (z₀ : ℂ)) :
    C(I, ℂ)

Given \(a,b\in \mathbb {R}\) with \(a {\lt} b\), a path \(\omega \colon [ a , b]\to \mathbb {C}\) with \(\omega (t)\not=0\) for all \(t\in [ a, b]\), and \(\tilde a_0\in CSexp^{-1}(\omega (a))\), there is a unique map \(\tilde\omega \colon [ a, b ]\to \mathbb {C}\) with \(\tilde\omega (a)=\tilde a_0\) and \(exp(\tilde\omega )=\omega \).

For each \(w\in \tilde S\), the number \(\frac{\Im (w)+\pi }{2\pi }\) is not an integer.

For \(z\in T\) and \(n\in \mathbb {Z}\),

Passing from units to the nonzero subtype and back again does not change a continuous map.

theorem fromNonzeroSubtype_toNonzeroSubtype
    [TopologicalSpace α] (f : C(α, ℂˣ)) :
    ContinuousMap.fromNonzeroSubtype
    (ContinuousMap.toNonzeroSubtype f) = f

A continuous map to nonzero complex numbers can be viewed as a units-valued continuous map.

noncomputable def fromNonzeroSubtype
    [TopologicalSpace α] (f : C(α, Cstar)) :
    C(α, ℂˣ)

Suppose \(f\colon E\to X\) is a map between topological spaces and \(U\subset X\) is an open subset and there is a trivialization for \(f\) on \(U\). Suppose also that there are homeomorphisms \(\varphi \colon X\to X\) and \(\tilde\varphi \colon E\to E\) with \(f\circ \tilde\varphi =\varphi \circ f\). Then there is a trivialization for \(f\) on \(\varphi (U)\).

A homotopy of loops is a one parameter family \(\Omega \colon [a, b]\times [0, 1]\to X\) with \(\Omega |_{[a, b]\times \{ s\} }\) a loop for all \(s\in [0, 1]\). A homotopy of loops based at \(x_0\) is a one parameter family indexed by \([0, 1]\) of loops based at \(x_0\).

The image of \(PBlog\) is contained in \(\{ z\in \mathbb {C}|-\pi {\lt} Im(z)\le \pi \} \) and for all \(\{ z\in \mathbb {C}| z\not=0\} \) \(CSexp(PBlog(z))=z\).

Then \(CSexp\colon S\to T\) and \(PBlog\colon T\to S\) are inverse homeomorphisms.

The image of a connected set under a continuous map is connected.

Let \(f\colon X\to Y\) be a continuous map and \(A\subset Y\). Then \(f\) is an even cover on \(A\subset X\) if every \(a\in A\) has a neighborhood which is contained in the target of a trivialization

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, the leading term eventually dominates the sum of the lower terms on circles of large 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)‖

Let \(X\) be a topological space and \(a, b ∈ ℝ\) with \(b {\gt} a\). A loop in \(X\) is a map \(\omega \colon [ a, b]\to X\) with \(\omega (b)=\omega (a)\). A loop is based at \(x_0\in X\) if \(\omega (a)=x_0\).

If a polynomial has no zeros on the circle of radius \(R\), then \(z\mapsto p(Rz)\) defines a map from the unit circle to \(\mathbb {C}^\times \).

noncomputable def mapCircleUnits
    (p : Polynomial ℂ) (R : ℝ)
    (hR : ∀ z : Circle, p.eval ((R : ℂ) * z) ≠ 0)
    :
    C(Circle, ℂˣ)

If a polynomial has no zeros on the closed unit disk of radius \(R\), then \(z\mapsto p(Rz)\) defines a map from that disk to \(\mathbb {C}^\times \).

noncomputable def mapClosedUnitDiskUnits
    (p : Polynomial ℂ) (R : ℝ)
    (hR :
      ∀ z : Metric.closedBall (0 : ℂ) 1,
        p.eval ((R : ℂ) * z) ≠ 0) :
    C(Metric.closedBall (0 : ℂ) 1, ℂˣ)

If \(x\in CSexp^{-1}(T)\), then \(x\in \widetilde S\).

Given \(\alpha _0\in \mathbb {C}^\times \), a natural number \(k\), and \(R{\gt}0\), let \(\psi _{\alpha _0,k,R}\colon S^1\to Cstar\) be the map \(\psi _{\alpha _0,k,R}(z)=\alpha _0(Rz)^k\).

The map \(z \mapsto \alpha _0 (Rz)^k\) from the unit circle to \(\Cstar \).

\(CSexp(z+w)=CSexp(z)* CSexp(w)\).

After coercing to \(\mathbb {C}\), the converted path has the same pointwise values as the original path.

theorem coe_toNonzeroSubtype_apply
    {u v : ℂˣ} (γ : Path u v) (t : I) :
    ((Path.toNonzeroSubtype γ t : Cstar) : ℂ) =
    (γ t : ℂ)

A units-valued path can be viewed as a path in the nonzero-complex subtype.

noncomputable def toNonzeroSubtype
    {u v : ℂˣ} (γ : Path u v) :
    Path (complexUnitsHomeomorphNeZero u)
    (complexUnitsHomeomorphNeZero v)

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

theorem windingNumber_eq_of_homotopy
    {z z' : Cstar} (γ : Path z z)
    (γ' : Path z' z') (H : C(I × I, Cstar))
    (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}\setminus \{ 0\} \), then the endpoint quotient \((\Gamma (1)-\Gamma (0))/(2\pi i)\) computes the winding number.

theorem windingNumber_eq_of_lift
    {z : Cstar} (γ : Path z z) (Γ : C(I, ℂ))
    (hlift : ∀ t, Complex.exp (Γ t) = (γ t : ℂ)) :
    (Γ 1 - Γ 0) / (2 * Real.pi * Complex.I) =
    Path.windingNumber γ

The constant loop has winding number zero.

theorem windingNumber_refl
    (z : Cstar) :
    Path.windingNumber (Path.refl z) = 0

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

noncomputable def windingNumber
    {z : Cstar} (γ : Path z z) :
    ℤ

If \(x\in CSexp^{-1}(T)\), then \(PBlog(CSexp(x))=\tilde\varphi ^{-1}_{\mathbb {C}}(x)\).

\(CSexp\colon \mathbb {C}\to \mathbb {C}\) is periodic of period \(2\pi i\) and with no smaller period.

The polynomial map \(z \mapsto p(Rz)\) from the unit circle to \(\Cstar \) when it avoids zero.

If a polynomial \(p\) has no zeros on the circle of radius \(R\), let \(f_{p,R}\colon S^1\to Cstar\) be the map \(f_{p,R}(z)=p(Rz)\).

If a polynomial \(p\) has no zeros on the closed disk of radius \(R\), let \(F_{p,R}\colon D^2\to Cstar\) be the map \(F_{p,R}(z)=p(Rz)\).

The polynomial map \(z \mapsto p(Rz)\) from the closed unit disk to \(\Cstar \) when it avoids zero.

Let \(\psi , \psi '\colon S^1\to \mathbb {C}\) be maps and let \(H : S^1\times I\to \mathbb {C}\) be a homotopy between them whose image lies in \(Cstar\). Then the winding numbers of \(\psi \) and \(\psi '\) are equal.

If two maps \(S^1\to \Cstar \) are homotopic through maps into \(\Cstar \), then they have equal winding numbers.

If \(\rho \colon S^1\to \Cstar \), then the image of the associated loop is contained in \(\Cstar \).

Let \(ρ : S^1→ \mathbb {C}\) be a map with \(ρ(z)∈ Cstar\) for all \(z∈ S^1\). Let \(ω\) be the loop associated with \(ρ\). Then the image of \(ω\) is contained in \(Cstar\).

Maps satisfying the walking-dog hypothesis have the same winding number.

Suppose that \(\psi ,\psi '\colon S^1\to \mathbb {C}\) satisfy \(|\psi (z)-\psi '(z)|{\lt}|\psi (z)|\) for all \(z\in S^1\). Then \(\psi \) and \(\psi '\) have the same winding number.

Any nonempty connected subset of \(\mathbb Z\) is a singleton.

The canonical inclusion of a sphere into the corresponding closed ball.

def sphereToClosedBall [PseudoMetricSpace α]
    (x : α) (r : ℝ) :
    Metric.sphere x r → Metric.closedBall x r

\(T=\{ z\in \mathbb {C}|Re(z){\gt}0 \cup Im(z)\not= 0\} \)

The set \(T=\{ z\in \mathbb {C}\mid \Re (z){\gt}0 \text{ or } \Im (z)\neq 0\} \) is open.

We have \(T\subset Cstar\).

Define \(S\subset \mathbb {C}\) by \(S=S(-\pi ,\pi )\).

\(T\cup T'=\{ z\in \mathbb {C}| z∈ Cstar\} \).

Define \(\varphi \colon S\times \mathbb {Z}\to \mathbb {C}\) by \(\varphi (z,k)=z+2k\pi *I\). Then \(\varphi \colon S\times \mathbb {Z}\to \tilde S\) is a homeomorphism.

The inverse map \(\tilde S\to S\times \mathbb {Z}\) is continuous.

The forward map \(S\times \mathbb {Z}\to \tilde S\) is continuous.

Define \(N(w)=\left\lfloor \frac{\Im (w)+\pi }{2\pi }\right\rfloor \).

Define \(\tilde\varphi ^{-1}(w)=(\tilde\varphi ^{-1}_{\mathbb {C}}(w),N(w))\in \mathbb {C}\times \mathbb {Z}\).

Define \(\tilde\varphi ^{-1}_{\mathbb {C}}(w)=w-2N(w)\pi i\).

Restrict \(\tilde\varphi ^{-1}\) to a map \(\tilde S\to S\times \mathbb {Z}\).

If \(w\in \tilde S\), then \(\tilde\varphi ^{-1}_{\mathbb {C}}(w)\in S\).

The maps \(\tilde\varphi \) and \(\tilde\varphi ^{-1}\) are left inverses on \(S\times \mathbb {Z}\).

The maps \(\tilde\varphi \) and \(\tilde\varphi ^{-1}\) are right inverses on \(\tilde S\).

Define \(\varphi \colon \mathbb {C}\times \mathbb {Z}\to \mathbb {C}\) by \(\varphi (z,n)=z+2n\pi i\).

If \(z\in S\), then \(\varphi (z,n)\in \tilde S\).

Passing from the nonzero subtype to units and back again does not change a continuous map.

theorem toNonzeroSubtype_fromNonzeroSubtype
    [TopologicalSpace α] (f : C(α, Cstar)) :
    ContinuousMap.toNonzeroSubtype
    (ContinuousMap.fromNonzeroSubtype f) = f

A units-valued continuous map can be viewed as a continuous map to nonzero complex numbers.

noncomputable def toNonzeroSubtype
    [TopologicalSpace α] (f : C(α, ℂˣ)) :
    C(α, Cstar)

Let

We have \(T'\subset Cstar\).

\(f\colon X\to Y\) a local trivialization for \(f\) on \(U\) is:

• an open subset \(U\subset Y\)

• a discrete space set \(I\)

• a homeomorphism \(\varphi \colon f^{-1}(U)\to U\times I\)

such that letting \(p_1\colon U\times I\to U\) be the projection onto the first factor, we have \(p_1\circ \varphi (x)=f(x)\) for all \(x\in f^{-1}(U)\)

If \(e\) is a trivialization of \(CSexp\colon \mathbb {C}\to \mathbb {C}\) over a set \(U\), then the same formulas define a trivialization of \(CSexpCstar\colon \mathbb {C}\to Cstar\) over \(U\cap Cstar\).

The composition \(\psi =\varphi \circ \widetilde{PBlog}\colon T\times \mathbb {Z}\to \tilde S\) defines a trivialization of \(CSexp\) on \(T\)

There is a trivialization of \(CSexpCstar\) over \(T\), viewed as a subset of \(Cstar\).

The base of the trivialization of Corollary 5 is exactly \(T\), viewed as a subset of \(Cstar\).

\(T'\) is the base of a trivialization for \(CSexp\colon \mathbb {C}\to \mathbb {C}\) with non-empty fiber.

There is a trivialization of \(CSexpCstar\) over \(T'\), viewed as a subset of \(Cstar\).

The base of the trivialization of Corollary 6 is exactly \(T'\), viewed as a subset of \(Cstar\).

Freely homotopic loops in \(\mathbb {C}^\times \) have the same winding number.

theorem unitsWindingNumber_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.unitsWindingNumber γ =
    Path.unitsWindingNumber γ'

Any exponential lift of a loop in \(\mathbb {C}^\times \) computes its winding number by the same endpoint quotient formula.

theorem unitsWindingNumber_eq_of_lift
    {u : ℂˣ} (γ : Path u u) (Γ : C(I, ℂ))
    (hlift : ∀ t, Complex.exp (Γ t) = (γ t : ℂ)) :
    (Γ 1 - Γ 0) / (2 * Real.pi * Complex.I) =
    Path.unitsWindingNumber γ

The constant loop in \(\mathbb {C}^\times \) has winding number zero.

theorem unitsWindingNumber_refl
    (u : ℂˣ) :
    Path.unitsWindingNumber (Path.refl u) = 0

The winding number of a loop in \(\mathbb {C}^\times \) is defined by transporting the loop to \(\mathbb {C}\setminus \{ 0\} \) and using the previous definition.

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

If two maps of the circle satisfy \(|\psi (z)-\psi '(z)|{\lt}|\psi (z)|\) for every \(z\), then the straight line homotopy between them stays inside \(\Cstar \).

Suppose that \(\psi \colon S^1\to \mathbb {C}\) and \(\psi '\colon S^1\to \mathbb {C}\) are maps and for each \(z\in S^1\), we have \(|\psi (z)-\psi '(z)|{\lt}|\psi (z)|\). Then there is a homotopy \(H\) from \(\psi \) to \(\psi '\) whose image lies in \(Cstar\).

\(\widetilde{PBlog}\colon T\times \mathbb {Z}\to S\times \mathbb {Z}\) is a homeomorphism.

Suppose that \(\omega \colon [ a, b ]\to \mathbb {C}\) is a loop with \(\omega (t)\in Cstar\) for all \(t\in [ a, b ]\). Then the constant \(w(\omega )\) given in Corollary 9 is the winding number of \(\omega \).

If \(\tilde\omega \) is any lift of the loop \(\omega \) through \(CSexp\), then its winding number is \(w(\omega )\).

If \(\omega \) is a loop in \(Cstar\), then it admits a lift through \(CSexp\).

Let \(p(z)\) be a complex polynomial of degree \(k{\gt}0\) given by \(p(z)=\sum _{i=0}^k\alpha _iz^{k-i}\) with \(α_i∈ℂ\) for all \(i\) and \(α_0\not= 0\). Then for \(R\) sufficiently large, the map \(f : S^1\to \mathbb {C}\) given by \(f(z)= p(R* z)\) for \(z\in S^1\) has winding number \(k\).

On a sufficiently large circle, a complex polynomial has winding number equal to its degree.

For \(x\in \mathbb {C}\) with \(x\not= 0\), either \(x\in T\) or \(x\in T'\).

Let \(0_{D^2}\) denote the center of the closed unit disk.

The center of the closed unit disk.

For a nonconstant complex polynomial, the leading term dominates the lower-order terms on sufficiently large circles.

Let \(p(z)\) be a complex polynomial of degree \(k\); \(p(z)=\sum _{i=0}^k\alpha _iz^{k-i}\) with \(\alpha _i\in \mathbb {C}\) and \(\alpha _0\not= 0\). For all \(R\) sufficiently large \(|\alpha _0|R^k{\gt}|\alpha _0z^k - p(z)|\) for any \(z\) with \(|z|=R\).

For any \(\alpha _0\in \mathbb {C}\) and any \(k\in \mathbb N\), define \(\psi _{\alpha _0,k}\colon \mathbb {C}\to \mathbb {C}\) by \(\psi _{\alpha _0,k}(z)=\alpha _0 z^k\). Then for any \(R{\gt}0\), if \(\alpha _0\not=0\), the winding number of the restriction of \(\psi _{\alpha _0,k}\) to the circle of radius \(R\) is \(k\).

The map \(z \mapsto \alpha _0 (Rz)^k\) on the unit circle has winding number \(k\).