2 Roots of Complex Polynomials
2.1 Homotopies through loops
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
This is the direct formalization of the condition that every slice \(t\mapsto H(s,t)\) is a loop.
2.2 The closed unit disk
The closed unit disk in the complex plane.
abbrev Disk : Type := Submonoid.unitClosedBall ℂ
This is the closed unit ball packaged as a bundled subtype, parallel to Mathlib’s definition of the unit circle.
2.3 Circle-valued helper constructions
The canonical inclusion of the unit circle into the closed unit disk.
abbrev toDisk :
Circle → Disk
This is the direct inclusion of the unit circle into the closed unit disk in \(\mathbb {C}\).
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)
The map is continuous by composition, and its endpoints agree because the circle parametrization takes both \(0\) and \(1\) to the point \(1\in S^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)
This is obtained by composing the given homotopy with the standard map from \(I\) to the circle.
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)
For each fixed \(s\), the two endpoints correspond to the same point of the circle because \(\exp (0)=\exp (2\pi i)=1\).
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
This is the defining property of a homotopy at time \(0\), evaluated along the circle parametrization.
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
This is the corresponding defining property of a homotopy at time \(1\).
2.4 Lifts and winding numbers of loops
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, ℂ)
Transport the path to the standard nonzero-complex subtype, where ‘exp‘ is already registered as a covering map in Mathlib, and apply path lifting there.
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
This is exactly the lifting property supplied by the covering-space API, after forgetting the codomain subtype.
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
This is uniqueness of lifts for the covering map \(\exp \), after transporting the path from \(\mathbb {C}^\times \) to the standard nonzero-complex subtype.
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 * π * 𝓲)
At the initial point, the two lifts have the same exponential, so their values differ by an integral multiple of \(2\pi i\). Shifting one lift by that constant does not change its projection, and uniqueness of lifts then shows the two lifts agree everywhere.
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) :
ℤ
Choose the lift beginning at \(\log (z)\). Since the path is a loop, the endpoints of the lift have the same exponential, hence differ by an integral multiple of \(2\pi i\); that integer is the winding number.
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 γ
Any lift differs from the canonical lift by a constant integral multiple of \(2\pi i\), so the endpoint difference and hence the quotient by \(2\pi i\) are unchanged.
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 γ'
Lift the whole free homotopy through the exponential covering map. The two boundary loops of the lift differ by a constant integral multiple of \(2\pi i\) along the side edges, so their endpoint differences agree and hence their winding numbers agree.
The constant loop has winding number zero.
theorem windingNumber_refl
(u : ℂˣ) :
Path.windingNumber (Path.refl u) = 0
The constant loop is lifted by a constant logarithm, whose endpoint difference is zero.
2.5 Winding numbers of circle maps
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, ℂˣ)) :
ℤ
This is the modern ‘Path‘-based version of passing from a circle map to its associated loop and taking the loop winding number.
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
The associated loop of a constant circle map is the constant loop, whose winding number is zero.
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
Precompose the homotopy with the standard parametrization of the circle to obtain a free homotopy between the associated loops, then apply homotopy invariance for loop winding numbers.
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)
Use the straight-line homotopy \((1-t)f+t g\). If this vanished at some point, then \(f=t(f-g)\) there, which would force \(\| f\| \le \| f-g\| \), contradicting the hypothesis.
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
Apply the previous existence theorem for a homotopy and then homotopy invariance of winding number.
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
Radially contract the closed disk to its center. Composing the extension with this contraction produces a homotopy from the boundary map to a constant map, and constant maps have winding number zero.
2.6 Monomials on the circle
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 underlying formula is continuous, and it never vanishes because \(a\), \(c\), and every point of the circle are nonzero.
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 : ℤ)
Choose a logarithm of the nonzero constant \(a c^n\). Then \(t\mapsto \log (ac^n)+n(2\pi t)i\) is a lift of the associated loop, and its endpoint difference is exactly \(2\pi n i\).
2.7 Polynomial maps on the circle and disk
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)‖
Choose \(R\) so large that the sum of the lower-order coefficients is small compared with the leading coefficient. On the circle of radius \(R\), the lower-order terms are then bounded by a strictly smaller quantity than the norm of the leading term.
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)‖
This is the previous threshold statement rewritten in the standard ‘atTop‘ language.
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 : ℤ)
For large radius, the polynomial map is uniformly close on the circle to its leading monomial in the walking-dog sense. The monomial has winding number equal to the degree, so the polynomial map has the same winding number.
Every nonconstant complex polynomial has a complex root.
theorem exists_root_of_natDegree_pos
(p : Polynomial ℂ) (hdeg : 0 < p.natDegree) :
∃ z : ℂ, p.IsRoot z
Assume the polynomial has no complex roots. Then it is nonzero on the whole plane, so the map \(z\mapsto p(Rz)\) extends from the unit circle to the closed unit disk through nonzero values. Hence its winding number must be zero. On the other hand, for sufficiently large \(R\), the previous theorem shows that the same winding number is the positive degree of the polynomial, a contradiction.