22.4. Monodromy.HolomorphicPrimitiveChain🔗

Jacobians.Monodromy.HolomorphicPrimitiveChain — source

IsLocalPrimitiveOn.mono

Restricting a primitive to a smaller set.

theorem IsLocalPrimitiveOn.mono {η : HolomorphicOneForms X} {F : X → ℂ} {U V : Set X}
    (h : IsLocalPrimitiveOn η F U) (hVU : V ⊆ U) : IsLocalPrimitiveOn η F V

exists_isPathConnected_open_mem_nhds

Every neighbourhood contains a path-connected open neighbourhood (the chart-ball preimage — the manifold is locally path-connected in the strong chart sense used throughout).

theorem exists_isPathConnected_open_mem_nhds {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] {x : X} {V : Set X} (hV : V ∈ 𝓝 x) :
    ∃ B : Set X, IsOpen B ∧ IsPathConnected B ∧ x ∈ B ∧ B ⊆ V

PrimitiveChain

A primitive chain along γ: a stabilized monotone partition of [0,1] together with a local primitive of η on an open set containing each sub-arc of γ.

structure PrimitiveChain (η : HolomorphicOneForms X) (γ : ℝ → X) where

t_nonneg

theorem t_nonneg (k : ℕ) : 0 ≤ C.t k

t_le_one

theorem t_le_one (k : ℕ) : C.t k ≤ 1

n_pos

theorem n_pos : 0 < C.n

value

The chain value: the telescoping sum ∑ᵢ Fᵢ(γ(tᵢ₊₁)) − Fᵢ(γ(tᵢ)).

def value : ℂ

partialValue

The capped partial value at time s: each block is capped at s (min-form; for s = 1 this is value, for s = 0 it vanishes).

def partialValue (s : ℝ) : ℂ

partialValue_zero

theorem partialValue_zero : C.partialValue 0 = 0

partialValue_one

theorem partialValue_one : C.partialValue 1 = C.value

partialValue_eq

The block formula: for s in block k, the partial value is the full sum of the first k blocks plus the capped k-th block.

theorem partialValue_eq (k : ℕ) (hk : k < C.n) {s : ℝ} (hs : s ∈ Icc (C.t k) (C.t (k + 1))) :
    C.partialValue s
      = (∑ i ∈ Finset.range k, (C.F i (γ (C.t (i + 1))) - C.F i (γ (C.t i))))
        + (C.F k (γ s) - C.F k (γ (C.t k)))

partialValue_sub

For s, s' in a common block k, the partial values differ by the Fₖ-increment.

theorem partialValue_sub (k : ℕ) (hk : k < C.n) {s s' : ℝ}
    (hs : s ∈ Icc (C.t k) (C.t (k + 1))) (hs' : s' ∈ Icc (C.t k) (C.t (k + 1))) :
    C.partialValue s' - C.partialValue s = C.F k (γ s') - C.F k (γ s)

exists_block_right

Right block: every s ∈ [0,1) lies in a block [tₖ, tₖ₊₁) open on the right.

theorem exists_block_right {s : ℝ} (h0 : 0 ≤ s) (h1 : s < 1) :
    ∃ k < C.n, C.t k ≤ s ∧ s < C.t (k + 1)

exists_block_left

Left block: every s ∈ (0,1] lies in a block (tₖ, tₖ₊₁] open on the left.

theorem exists_block_left {s : ℝ} (h0 : 0 < s) (h1 : s ≤ 1) :
    ∃ k < C.n, C.t k < s ∧ s ≤ C.t (k + 1)

exists_primitiveChain

Primitive chains exist along every continuous path: refine the open cover of [0,1] by preimages of primitive neighbourhoods (Mathlib's monotone-subdivision lemma).

theorem exists_primitiveChain (η : HolomorphicOneForms X) {γ : ℝ → X}
    (hγ : ContinuousOn γ (Icc 0 1)) : Nonempty (PrimitiveChain η γ)

PrimitiveChain.value_eq_of_chains

The chain value is chain-independent (uniqueness of the discrete continuation, Forster §10.4): the difference of the two capped partial values is locally constant on [0,1] (one-sided block arguments + the step-0 rigidity near each path point), hence constant on the preconnected interval; it vanishes at 0 and reads value − value at 1.

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