30.8. Abel.AbelFormRead🔗

Jacobians.Abel.AbelFormRead — source

extChartAt_real_eq_chartAt

The boundaryless identity-model extChartAt is the bare chart, as a function.

theorem extChartAt_real_eq_chartAt (y : X) :
    ((extChartAt 𝓘(ℝ, ℂ) y) : X → ℂ) = (chartAt (H := ℂ) y)

mem_extChartAt_real_source_iff

Source transfer between the two chart spellings.

theorem mem_extChartAt_real_source_iff (y x : X) :
    x ∈ (extChartAt 𝓘(ℝ, ℂ) y).source ↔ x ∈ (chartAt (H := ℂ) y).source

deriv_transition_ext_eq_chart

The transition derivative in extChartAt 𝓘(ℝ,ℂ) spelling equals the chartAt (λ-form) spelling.

theorem deriv_transition_ext_eq_chart (y x : X) :
    deriv ((extChartAt 𝓘(ℝ, ℂ) x) ∘ (extChartAt 𝓘(ℝ, ℂ) y).symm) ((extChartAt 𝓘(ℝ, ℂ) y) x)
      = deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y).symm w))
          ((chartAt (H := ℂ) y) x)

deriv_transition_self

The self-chart transition has derivative 1 at the centre image.

theorem deriv_transition_self (x : X) {z : ℂ} (hz : z ∈ (chartAt (H := ℂ) x).target) :
    deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) x).symm w)) z = 1

differentiableAt_pullback_of_mdifferentiableAt

MDifferentiableAt over the real model gives plain real differentiability of the own-chart pullback at the chart coordinate.

theorem differentiableAt_pullback_of_mdifferentiableAt {w : X → ℂ} {x : X}
    (hw : MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) :
    DifferentiableAt ℝ (fun z => w ((extChartAt 𝓘(ℝ, ℂ) x).symm z))
      (extChartAt 𝓘(ℝ, ℂ) x x)

frameVector_eq_deriv_chart

The frame vector in chart spelling: symmL (trivAt y) x 1 is the transition derivative (chart_x ∘ chart_y⁻¹)′(chart_y x).

theorem frameVector_eq_deriv_chart [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {y x : X} (hx : x ∈ (chartAt (H := ℂ) y).source) :
    ((Bundle.Trivialization.symmL ℝ
        (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) y) x) (1 : ℂ) : ℂ)
      = deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y).symm w))
          ((chartAt (H := ℂ) y) x)

transition_eventuallyEq_comp

On the germ window at chart_y x, the x-transition through y factors through the y → y' transition.

theorem transition_eventuallyEq_comp [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y).symm w))
        =ᶠ[𝓝 ((chartAt (H := ℂ) y) x)]
      (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y').symm w))
        ∘ (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))

deriv_transition_cocycle

The transition-derivative cocycle: for x in both chart sources, (chart\_x ∘ chart\_y⁻¹)′(chart\_y x) = (chart\_x ∘ chart\_\{y'\}⁻¹)′(chart\_\{y'\} x) · (chart\_\{y'\} ∘ chart\_y⁻¹)′(chart\_y x).

theorem deriv_transition_cocycle [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y).symm w))
        ((chartAt (H := ℂ) y) x)
      = deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y').symm w))
          ((chartAt (H := ℂ) y') x)
        * deriv (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))
            ((chartAt (H := ℂ) y) x)

read01

The chart-y read of a smooth (0,1)-form: the value of g at x on the constant y-frame tangent vector (the symmL of the fixed y-trivialization at 1).

def read01 [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (g : SmoothCOneForms X) (y : X) : X → ℂ

contMDiffAt_read01

The read is smooth at every point of the chart source (contMDiffAt_chartRead_datum).

theorem contMDiffAt_read01 [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (g : SmoothCOneForms X) {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) :
    ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) (⊤ : ℕ∞) (read01 g y) x

read01_eq_conj_mul

The conjugate-frame formula: for g ∈ A^{0,1} and x in the chart source of y, read01 g y x = conj((chart_x ∘ chart_y⁻¹)′(chart_y x)) · (g x) 1.

theorem read01_eq_conj_mul [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {g : SmoothCOneForms X} (hg : g ∈ OneFormsZeroOne X) {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) :
    read01 g y x = (starRingEnd ℂ)
      (deriv (fun w => (chartAt (H := ℂ) x) ((chartAt (H := ℂ) y).symm w))
        ((chartAt (H := ℂ) y) x))
        * (g x) (1 : ℂ)

read01_transform

The (0,1)-transformation law: read_y = conj(T′)·read_{y'} along the chart transition T = chart_{y'} ∘ chart_y⁻¹.

theorem read01_transform [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {g : SmoothCOneForms X} (hg : g ∈ OneFormsZeroOne X) {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    read01 g y x = (starRingEnd ℂ)
      (deriv (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))
        ((chartAt (H := ℂ) y) x))
        * read01 g y' x

localRep_transform

The (1,0)-transformation law for the holomorphic coefficient: localRep_y = T′ · localRep_{y'} along the chart transition T = chart_{y'} ∘ chart_y⁻¹.

theorem localRep_transform [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) {x y y' : X}
    (hxy : x ∈ (chartAt (H := ℂ) y).source) (hxy' : x ∈ (chartAt (H := ℂ) y').source) :
    Jacobians.Montel.localRep η y x
      = deriv (fun w => (chartAt (H := ℂ) y') ((chartAt (H := ℂ) y).symm w))
          ((chartAt (H := ℂ) y) x)
        * Jacobians.Montel.localRep η y' x

read01_proj01_mfderiv

The ∂̄-bridge in any chart. For w real-differentiable at x ∈ source_y, the y-frame read of the (0,1)-part of mfderiv w x is the planar Wirtinger derivative of the chart-y pullback of w:

proj01 (mfderiv w x) (frame_y) = ∂̄(w ∘ chart_y⁻¹)(chart_y x).

theorem read01_proj01_mfderiv [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {w : X → ℂ} {x y : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source)
    (hw : MDifferentiableAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) :
    proj01 (mfderiv 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) w x) ((Bundle.Trivialization.symmL ℝ
        (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) y) x) (1 : ℂ))
      = DbarDisk.dbar (w ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x)

read01_dbarL

The read of ∂̄u in the chart at y: read01 (∂̄u) y = ∂̄(u ∘ chart_y⁻¹) ∘ chart_y on the chart source.

theorem read01_dbarL [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (u : SmoothCFunctions X) {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) :
    read01 (dbarL u) y x
      = DbarDisk.dbar (⇑u ∘ (chartAt (H := ℂ) y).symm) ((chartAt (H := ℂ) y) x)

read01_add

theorem read01_add [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (g₁ g₂ : SmoothCOneForms X) (y x : X) :
    read01 (g₁ + g₂) y x = read01 g₁ y x + read01 g₂ y x

read01_smul

theorem read01_smul [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (r : ℝ)
    (g : SmoothCOneForms X) (y x : X) :
    read01 (r • g) y x = r • read01 g y x

read01_zero

theorem read01_zero [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (y x : X)
    : read01 (0 : SmoothCOneForms X) y x = 0

read01_zsmul

theorem read01_zsmul [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X] (n : ℤ)
    (g : SmoothCOneForms X) (y x : X) :
    read01 (n • g) y x = n • read01 g y x

read01_cSmulForm

theorem read01_cSmulForm [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (c : SmoothCFunctions X) (g : SmoothCOneForms X) (y x : X) :
    read01 (cSmulForm c g) y x = c x * read01 g y x

read01_eq_zero_of_apply_eq_zero

Reads vanish wherever the fiber value vanishes.

theorem read01_eq_zero_of_apply_eq_zero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {g : SmoothCOneForms X} {x : X}
    (h : (g x) = (0 : ℂ →L[ℝ] ℂ)) (y : X) : read01 g y x = 0

proj01_eq_self_of_conjLinear

A conjugate-linear fiber form is fixed by proj01 (it IS (0,1)).

theorem proj01_eq_self_of_conjLinear {α : ℂ →L[ℝ] ℂ}
    (h : ∀ v, α (Complex.I * v) = -(Complex.I * α v)) : proj01 α = α

conjFiber

The fiberwise conjugate of a holomorphic form: v ↦ conj (η x v), an ℝ-CLM.

def conjFiber [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) (x : X) : ℂ →L[ℝ] ℂ

conjFiber_apply

theorem conjFiber_apply [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) (x : X) (v : ℂ) :
    conjFiber η x v = (starRingEnd ℂ) (η.toFun x v)

conjFiber_conjLinear

The conjugate fiber is conjugate-linear.

theorem conjFiber_conjLinear [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) (x : X) (v : ℂ) :
    conjFiber η x (Complex.I * v) = -(Complex.I * conjFiber η x v)

conjFiber_frame

The conjugate fiber against the y-frame vector is conj (localRep η y x).

theorem conjFiber_frame [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) :
    conjFiber η x ((Bundle.Trivialization.symmL ℝ
        (trivializationAt ℂ (TangentSpace (𝓘(ℝ, ℂ))) y) x) (1 : ℂ))
      = (starRingEnd ℂ) (Jacobians.Montel.localRep η y x)

contMDiff_conjFiber

Smoothness of the conjugate-fiber section (hom-bundle reduction: near y the in-coordinates read is (mul (conj (localRep η y ·))).comp conj, with conj (localRep η y ·) real-smooth since localRep η y is chart-analytic).

theorem contMDiff_conjFiber [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) :
    ContMDiff (𝓘(ℝ, ℂ)) (𝓘(ℝ, ℂ).prod 𝓘(ℝ, ℂ →L[ℝ] ℂ)) (⊤ : ℕ∞)
      (fun x => (⟨x, conjFiber η x⟩ : Bundle.TotalSpace (ℂ →L[ℝ] ℂ)
        (fun x : X => TangentSpace (𝓘(ℝ, ℂ)) x →L[ℝ] (Bundle.Trivial X ℂ) x)))

conjForm

The conjugate form ω̄ of a holomorphic 1-form, as a smooth ℂ-valued 1-form.

def conjForm [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) : SmoothCOneForms X where

conjForm_apply

theorem conjForm_apply [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) (x : X) :
    (conjForm η) x = conjFiber η x

conjForm_mem_zeroOne

ω̄ is a (0,1)-form.

theorem conjForm_mem_zeroOne [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) :
    conjForm η ∈ OneFormsZeroOne X

read01_conjForm

The chart-y read of ω̄ is the conjugate of the holomorphic coefficient: read01 (conjForm η) y = conj ∘ localRep η y on the chart source.

theorem read01_conjForm [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (η : HolomorphicOneForms X) {y x : X}
    (hx : x ∈ (chartAt (H := ℂ) y).source) :
    read01 (conjForm η) y x = (starRingEnd ℂ) (Jacobians.Montel.localRep η y x)