22.6. Monodromy.HolomorphicPrimitiveMonodromy🔗

Jacobians.Monodromy.HolomorphicPrimitiveMonodromy — source

sum_telescope_abel

Abel summation: a telescoping sum with block-dependent summands equals the boundary terms minus the interior-node defects.

theorem sum_telescope_abel {n : ℕ} (hn : 0 < n) (G : ℕ → ℕ → ℂ) :
    ∑ k ∈ Finset.range n, (G k (k + 1) - G k k)
      = G (n - 1) n - G 0 0 - ∑ k ∈ Finset.Ico 1 n, (G k k - G (k - 1) k)

pathPrimValue

The path value ∫_γ η in its discrete incarnation: the value of any primitive chain along γ (chain-independent by value_eq_of_chains).

def pathPrimValue (η : HolomorphicOneForms X) (γ : ℝ → X)
    (hγ : ContinuousOn γ (Icc 0 1)) : ℂ

pathPrimValue_eq

theorem pathPrimValue_eq (η : HolomorphicOneForms X) {γ : ℝ → X}
    (hγ : ContinuousOn γ (Icc 0 1)) (C : PrimitiveChain η γ) :
    pathPrimValue η γ hγ = C.value

pathPrimValue_eq_of_homotopy

The monodromy theorem: the path value is invariant under endpoint-fixed continuous homotopies (stated over all of ℝ — the homotopy is totalized, e.g. via projIcc).

theorem pathPrimValue_eq_of_homotopy (η : HolomorphicOneForms X) {H : ℝ → ℝ → X}
    (hH : Continuous (uncurry H)) {x₀ x₁ : X}
    (h0 : ∀ s, H s 0 = x₀) (h1 : ∀ s, H s 1 = x₁) :
    pathPrimValue η (H 0) ((hH.comp (continuous_const.prodMk continuous_id)).continuousOn)
      = pathPrimValue η (H 1)
        ((hH.comp (continuous_const.prodMk continuous_id)).continuousOn)