22.7. Monodromy.HolomorphicPrimitives🔗

Jacobians.Monodromy.HolomorphicPrimitives — source

pathPrimValue_congr

theorem pathPrimValue_congr (η : HolomorphicOneForms X) {γ₁ γ₂ : ℝ → X}
    (h₁ : ContinuousOn γ₁ (Icc 0 1)) (h₂ : ContinuousOn γ₂ (Icc 0 1)) (h : γ₁ = γ₂) :
    pathPrimValue η γ₁ h₁ = pathPrimValue η γ₂ h₂

pathPrimValue_eq_of_homotopic

Homotopic paths have equal path values (monodromy + projIcc-totalization of the Path.Homotopy).

theorem pathPrimValue_eq_of_homotopic (η : HolomorphicOneForms X) {x y : X}
    {p q : Path x y} (h : p.Homotopic q) :
    pathPrimValue η p.extend p.continuous_extend.continuousOn
      = pathPrimValue η q.extend q.continuous_extend.continuousOn

trans_extend_left

Evaluating the extension of a concatenation, left half.

theorem trans_extend_left {X : Type*} [TopologicalSpace X] {x₀ x y : X}
    (p : Path x₀ x) (q : Path x y) {s : ℝ}
    (h0 : 0 ≤ s) (h2 : s ≤ 1 / 2) :
    (p.trans q).extend s = p.extend (2 * s)

trans_extend_right

Evaluating the extension of a concatenation, right half.

theorem trans_extend_right {X : Type*} [TopologicalSpace X] {x₀ x y : X}
    (p : Path x₀ x) (q : Path x y) {s : ℝ}
    (h2 : 1 / 2 < s) (h1 : s ≤ 1) :
    (p.trans q).extend s = q.extend (2 * s - 1)

pathPrimValue_trans_primitive_block

The in-disk concatenation identity: appending a path that stays inside a primitive disk (B, G) adds exactly the primitive increment G y − G x to the path value. (The chain for the concatenation is the half-scaled chain of p plus the single block (B, G).)

theorem pathPrimValue_trans_primitive_block (η : HolomorphicOneForms X) {x₀ x y : X}
    (p : Path x₀ x) {B : Set X} {G : X → ℂ} (hBo : IsOpen B)
    (hG : IsLocalPrimitiveOn η G B) (q : Path x y) (hq : ∀ τ : I, q τ ∈ B) :
    pathPrimValue η (p.trans q).extend (p.trans q).continuous_extend.continuousOn
      = pathPrimValue η p.extend p.continuous_extend.continuousOn + (G y - G x)

hasHolomorphicPrimitives

HasHolomorphicPrimitives holds (the monodromy theorem / holomorphic Poincaré lemma): on a simply connected compact Riemann surface, every holomorphic 1-form has a global holomorphic primitive.

theorem hasHolomorphicPrimitives : HasHolomorphicPrimitives X