The crossing angles of a closed immersion, modulo an integer

Hungerbühler–Wasem Proposition 2.2 decomposes a closed piecewise-C¹ immersion Λ meeting a point s at the finitely many parameters t₁, …, tₙ as Λ = \tilde{\Lambda} + Γ₁ + ⋯ + Γₙ, with \tilde{\Lambda} avoiding s and each Γ_ℓ a model sector of opening angle α_ℓ, and concludes

n_s(Λ) = n_s(\tilde{\Lambda}) + ∑_ℓ α_ℓ / 2π.

Since \tilde{\Lambda} avoids s, its winding number is an integer (TauCeti.Contour.IsPiecewiseC1On.exists_int_windingNumber). This file proves the identity in the form that does not name the surgered curve:

n_s(Λ) - ∑_ℓ α_ℓ / 2π ∈ ℤ,

where α_ℓ = crossingAngle Λ t_ℓ is read off the one-sided tangents at the crossing. Nothing here builds \tilde{\Lambda}, so the integer is produced abstractly rather than identified with n_s(\tilde{\Lambda}); that identification, which needs the excise-and-cap construction, is what remains of HW Proposition 2.2.

The proof does not decompose the curve either. It exponentiates. The principal value 2πi · n_s(Λ) is aggregated out of plain pieces and crossing windows exactly as the existence proof aggregates it (TauCeti.Contour.IsPwC1ImmersionOn.cauchyPVExistsAt_inv_sub), and both kinds of contribution exponentiate to a chord ratio: a plain piece to (Λ u - s)/(Λ l - s) (TauCeti.Contour.IsPiecewiseC1On.exp_two_pi_I_mul_windingNumber), and a crossing window to that same ratio times exp (i α_ℓ) (TauCeti.Contour.exp_log_norm_add_arg_eq_mul_exp_crossingAngle below, which is where the crossing angle enters). The ratios telescope along the curve and cancel at the closed-up basepoint, leaving exp (2πi · n_s(Λ)) = exp (i ∑_ℓ α_ℓ). Reading that off is the whole content: with no crossings it is the classical integrality statement, and each crossing shifts the winding number by its angle over 2π.

Main results

• TauCeti.Contour.exp_log_norm_add_arg_eq_mul_exp_crossingAngle — the per-window principal value of the Cauchy kernel exponentiates to the window's chord ratio times exp (i · crossingAngle).
• TauCeti.Contour.IsPwC1ImmersionOn.exp_two_pi_I_mul_windingNumber_eq_exp_sum_crossingAngle — exp (2πi · n_s(γ)) = exp (i ∑ α) for a closed piecewise-C¹ immersion based off s.
• TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_sum_crossingAngle — HW Proposition 2.2, modulo the integer: n_s(γ) = k + (∑ α) / 2π for some k : ℤ, and …_toFinset, the same against the canonical crossing set of the immersion.
• TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_card_div_two — the smooth case: if every crossing is smooth, each contributes ½.

Provenance

No formal source is vendored for the exponential argument. Its two inputs are migrated material: the per-window principal value of the Cauchy kernel (TauCeti.Analysis.Contour.PerWindow.CPV, from LocalCutoffs.lean of the AINTLIB LeanModularForms development) and the crossing-angle reading of its boundary arguments (TauCeti.Analysis.Contour.RegularityConditions).

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Proposition 2.2.

theorem TauCeti.Contour.exp_log_norm_add_arg_eq_mul_exp_crossingAngle {γ : ℝ → ℂ} {t₀ : ℝ} {L_R L_L w_L w_R : ℂ} (hL_L : L_L ≠ 0) (hL_R : L_R ≠ 0) (hw_L : w_L ≠ 0) (hw_R : w_R ≠ 0) (h_R : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Ioi t₀)) (nhds L_R)) (h_L : Filter.Tendsto (deriv γ) (nhdsWithin t₀ (Set.Iio t₀)) (nhds L_L)) : Complex.exp (↑(Real.log ‖w_R‖ - Real.log ‖w_L‖) + ↑((-L_L / w_L).arg + (w_R / L_R).arg) * Complex.I) = w_R / w_L * Complex.exp (↑(crossingAngle γ t₀) * Complex.I)

The per-window principal value exponentiates to the chord ratio times the crossing angle. TauCeti.Contour.perWindow_truncated_integral_tendsto evaluates the ε-truncated integral of the Cauchy kernel over a crossing window to (log ‖w_R‖ - log ‖w_L‖) + i · (arg (-L_L / w_L) + arg (w_R / L_R)), where w_L, w_R are the chords to the two window endpoints and L_L, L_R the one-sided tangents at the crossing. This identity says its exponential is w_R / w_L · exp (i · crossingAngle γ t₀): the log-norm part supplies the modulus of the chord ratio, and the two boundary arguments supply its argument plus exactly the crossing angle, by TauCeti.Contour.coe_crossingAngle_eq_arg_neg_div_add_arg_div_sub_arg_div.

The chords w_L, w_R are left free, as they are there; the intended reading takes them to be γ (t₀ - ρ) - s and γ (t₀ + ρ) - s.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exp_two_pi_I_mul_windingNumber_eq_exp_sum_crossingAngle {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {T : Finset ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) (hT : ∀ (t : ℝ), t ∈ T ↔ t ∈ Set.Icc a b ∧ γ t = s) : Complex.exp (2 * ↑Real.pi * Complex.I * windingNumber γ a b s) = Complex.exp (↑(∑ t ∈ T, crossingAngle γ t) * Complex.I)

The winding number of a closed immersion exponentiates to its crossing angles. For a closed piecewise-C¹ immersion γ on [a, b] whose basepoint avoids s, and a finset T listing exactly the parameters where γ meets s,

exp (2πi · n_s(γ)) = exp (i · ∑_{t ∈ T} crossingAngle γ t).

The principal value on the left is aggregated by cutting [a, b] into plain pieces, on which γ keeps a positive distance from s, and one window around each crossing. Exponentiated, a plain piece contributes the chord ratio of its endpoints, and a crossing window contributes that ratio times exp (i · crossingAngle) (TauCeti.Contour.exp_log_norm_add_arg_eq_mul_exp_crossingAngle); the ratios telescope, and closedness cancels the two ends. With T = ∅ this is the endpoint-ratio proof of integrality.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_sum_crossingAngle {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {T : Finset ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) (hT : ∀ (t : ℝ), t ∈ T ↔ t ∈ Set.Icc a b ∧ γ t = s) : ∃ (k : ℤ), windingNumber γ a b s = ↑k + ↑(∑ t ∈ T, crossingAngle γ t) / (2 * ↑Real.pi)

Hungerbühler–Wasem Proposition 2.2, modulo the integer. For a closed piecewise-C¹ immersion γ on [a, b] whose basepoint avoids s, and a finset T listing exactly the parameters where γ meets s, the generalized winding number is an integer plus the crossing angles over 2π:

n_s(γ) = k + (∑_{t ∈ T} crossingAngle γ t) / 2π.

In HW's decomposition Λ = \tilde{\Lambda} + Γ₁ + ⋯ + Γₙ the integer is n_s(\tilde{\Lambda}), the winding number of the curve obtained by excising the crossings and capping them off; that surgery is not performed here, so k is produced abstractly. Everything else is: the crossings' contribution is exactly their model-sector value α_ℓ / 2π.

With no crossings this is TauCeti.Contour.IsPiecewiseC1On.exists_int_windingNumber, and with a single smooth crossing it gives the half-integral winding number of the half-residue regime (exists_int_windingNumber_eq_add_card_div_two).

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_sum_crossingAngle_toFinset {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) : ∃ (k : ℤ), windingNumber γ a b s = ↑k + ↑(∑ t ∈ ⋯.toFinset, crossingAngle γ t) / (2 * ↑Real.pi)

Hungerbühler–Wasem Proposition 2.2 against the canonical crossing set. The form of exists_int_windingNumber_eq_add_sum_crossingAngle that takes its crossing finset from the finiteness of the crossing set of an immersion (TauCeti.Contour.IsPwC1ImmersionOn.finite_crossings) rather than from the caller.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_card_div_two {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} {T : Finset ℝ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a ≤ b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) (hT : ∀ (t : ℝ), t ∈ T ↔ t ∈ Set.Icc a b ∧ γ t = s) (hsmooth : ∀ t ∈ T, crossingAngle γ t = Real.pi) : ∃ (k : ℤ), windingNumber γ a b s = ↑k + ↑T.card / 2

Every smooth crossing contributes ½. A crossing where the two one-sided tangents agree has angle π (TauCeti.Contour.crossingAngle_eq_pi), hence winding weight π / 2π = ½. So a closed immersion running smoothly through s exactly n times has winding number n / 2 modulo an integer — in particular a single smooth crossing gives the ½ of the half-residue regime and of the valence formula's elliptic point i.