22.5. Monodromy.HolomorphicPrimitiveLocal🔗

Jacobians.Monodromy.HolomorphicPrimitiveLocal — source

IsLocalPrimitiveOn

F is a holomorphic primitive of η on U: at every point of U the function F is manifold-differentiable and its intrinsic differential reads η on every tangent vector (the value-wise dF = η of HasHolomorphicPrimitives).

def IsLocalPrimitiveOn (η : HolomorphicOneForms X) (F : X → ℂ) (U : Set X) : Prop

oneForm_eq_mfderiv_of_frame_eq

The frame lemma. For y in the chart source at x₀ where F is differentiable, if the chart-pullback derivative of F matches the local representative of η (a single scalar equation), then dF = η holds at y on every tangent vector: both sides are ℂ-linear on the 1-dimensional T_y X, and they agree on the spanning vector symmL ℂ y 1 — η.toFun y (symmL 1) = localRep η x₀ y by definition, mfderiv F y (symmL 1) = (F ∘ chart⁻¹)′(chart y) by mfderiv_apply_symmL_eq_deriv.

theorem oneForm_eq_mfderiv_of_frame_eq (η : HolomorphicOneForms X) (F : X → ℂ) {x₀ y : X}
    (hy : y ∈ (chartAt ℂ x₀).source) (hF : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) F y)
    (hfr : Montel.localRep η x₀ y = deriv (F ∘ (chartAt ℂ x₀).symm) ((chartAt ℂ x₀) y)) :
    ∀ v : TangentSpace 𝓘(ℂ) y, η.toFun y v = mfderiv 𝓘(ℂ) 𝓘(ℂ) F y v

exists_isLocalPrimitiveOn

Chart-local existence of holomorphic primitives (the holomorphic Poincaré lemma on a Riemann surface): every point has a path-connected open neighbourhood carrying a primitive of η. The chart coefficient of η is analytic on the chart target, hence has a primitive G on a ball around the chart centre (exists_primitive_of_convex); F := G ∘ chart works on the preimage of the ball.

theorem exists_isLocalPrimitiveOn (η : HolomorphicOneForms X) (x₀ : X) :
    ∃ (U : Set X) (F : X → ℂ), IsOpen U ∧ x₀ ∈ U ∧ IsPathConnected U ∧
      IsLocalPrimitiveOn η F U

differentiableAt_comp_chart_symm

Chart-pullback differentiability from manifold differentiability (the converse of mdifferentiableAt_of_differentiableAt_comp): if f is MDifferentiableAt y for y in the chart source at x, then f ∘ chart⁻¹ is DifferentiableAt (chart y).

theorem differentiableAt_comp_chart_symm {X : Type*} [TopologicalSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {f : X → ℂ} {x y : X}
    (hy : y ∈ (chartAt ℂ x).source) (hf : MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f y) :
    DifferentiableAt ℂ (f ∘ (chartAt ℂ x).symm) ((chartAt ℂ x) y)

isLocalPrimitiveOn_sub_locally_const

On an open set, the difference of two primitives of the same form is locally constant: near every point it is constant on a chart ball (its chart pullback is differentiable with vanishing derivative on a convex set).

theorem isLocalPrimitiveOn_sub_locally_const {η : HolomorphicOneForms X} {F F' : X → ℂ}
    {U : Set X} (hU : IsOpen U) (hF : IsLocalPrimitiveOn η F U)
    (hF' : IsLocalPrimitiveOn η F' U) {y : X} (hy : y ∈ U) :
    ∀ᶠ w in 𝓝 y, F w - F' w = F y - F' y

isLocalPrimitiveOn_sub_const

Rigidity: two primitives of η on a preconnected open set differ by a constant — their difference is locally constant (isLocalPrimitiveOn_sub_locally_const), and a locally constant function on a preconnected set takes one value (clopen argument).

theorem isLocalPrimitiveOn_sub_const {η : HolomorphicOneForms X} {F F' : X → ℂ}
    {U : Set X} (hU : IsOpen U) (hUc : IsPreconnected U) (hF : IsLocalPrimitiveOn η F U)
    (hF' : IsLocalPrimitiveOn η F' U) {a b : X} (ha : a ∈ U) (hb : b ∈ U) :
    F a - F' a = F b - F' b