30.10. Abel.AbelPairing🔗

Jacobians.Abel.AbelPairing — source

pairingIntegrand

The pairing integrand in the chart at y, over the window V ⊆ X: 𝟙_{chart''V} · (P∘chart⁻¹) · (read01 g y ∘ chart⁻¹) · (localRep η y ∘ chart⁻¹). The indicator makes the formula globally defined (junk chart-inverse values are cut off).

def pairingIntegrand {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) (V : Set X) : ℂ → ℂ

KillsAt

The vanishing kill condition: at x either the scalar field or the (0,1)-fiber dies.

def KillsAt {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (P : X → ℂ) (g : SmoothCOneForms X) (x : X) : Prop

pairingIntegrand_eq_zero_of_killsAt

theorem pairingIntegrand_eq_zero_of_killsAt {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {g : SmoothCOneForms X}
    {η : HolomorphicOneForms X} {P : X → ℂ} {y : X} {V : Set X}
    (_hV : V ⊆ (chartAt (H := ℂ) y).source) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) y) '' V → KillsAt P g ((chartAt (H := ℂ) y).symm z)) :
    pairingIntegrand g η P y V z = 0

pairingIntegrand_congr_window

Window change: the indicator window may be enlarged as long as the kill condition holds on the difference.

theorem pairingIntegrand_congr_window {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) {V W : Set X} (hVW : V ⊆ W)
    (hW : W ⊆ (chartAt (H := ℂ) y).source)
    (hkill : ∀ x ∈ W, x ∉ V → KillsAt P g x) :
    pairingIntegrand g η P y V = pairingIntegrand g η P y W

continuous_pairingIntegrand

Continuity of the pairing integrand: honest continuity at window points (all three factors are smooth/analytic reads on the chart source), local vanishing outside the compact core image (the kill condition).

theorem continuous_pairingIntegrand {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    {P : X → ℂ} (hP : Continuous P)
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → KillsAt P g x) :
    Continuous (pairingIntegrand g η P y V)

hasCompactSupport_pairingIntegrand

Compact support of the pairing integrand (inside the chart image of the core).

theorem hasCompactSupport_pairingIntegrand {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X) (P : X → ℂ)
    {y : X} {V : Set X} (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → KillsAt P g x) :
    HasCompactSupport (pairingIntegrand g η P y V)

integrable_pairingIntegrand

Integrability of the pairing integrand (continuity + compact support).

theorem integrable_pairingIntegrand {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    {P : X → ℂ} (hP : Continuous P)
    {y : X} {V : Set X} (hVopen : IsOpen V) (hVsub : V ⊆ (chartAt (H := ℂ) y).source)
    {K : Set X} (hK : IsCompact K) (hKV : K ⊆ V)
    (hsupp : ∀ x ∈ V, x ∉ K → KillsAt P g x) :
    Integrable (pairingIntegrand g η P y V) volume

integral_pairingIntegrand_transport

Chart-change invariance of the pairing integral: for g ∈ A^{0,1} and an open window inside both chart sources, the plane integral of the pairing integrand does not depend on the chart it is read in. Holomorphic change of variables along the transition: the (0,1)-factor transforms by conj T′ (read01_transform), the (1,0)-factor by T′ (localRep_transform), and conj T′ · T′ = |T′|² is the real Jacobian.

theorem integral_pairingIntegrand_transport {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X) (η : HolomorphicOneForms X) (P : X → ℂ)
    {y y' : X} {V : Set X} (hVopen : IsOpen V)
    (hVy : V ⊆ (chartAt (H := ℂ) y).source) (hVy' : V ⊆ (chartAt (H := ℂ) y').source) :
    ∫ z, pairingIntegrand g η P y V z = ∫ w, pairingIntegrand g η P y' V w

coverWindow

The j-th cover window: the outer open shrinkage at the j-th cover centre.

def coverWindow {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X]
    (j : Fin ((chartCover : Finset X).card)) : Set X

coverWindow_isOpen

theorem coverWindow_isOpen {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ChartedSpace ℂ X] (j : Fin ((chartCover : Finset X).card)) :
    IsOpen (coverWindow (X := X) j)

coverWindow_subset_source

theorem coverWindow_subset_source {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (j : Fin ((chartCover : Finset X).card)) :
    coverWindow (X := X) j ⊆ (chartAt (H := ℂ) (coverCenter j)).source

tsupport_coverPoU_subset_window

theorem tsupport_coverPoU_subset_window {X : Type*} [TopologicalSpace X] [T2Space X]
    [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X]
    (j : Fin ((chartCover : Finset X).card)) :
    tsupport (coverPoU (X := X) j) ⊆ coverWindow (X := X) j

killsAt_coverRhoC

The kill condition for the PoU scalar field: ρ̂ⱼ vanishes off its compact support.

theorem killsAt_coverRhoC {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (j : Fin ((chartCover : Finset X).card)) :
    ∀ x ∈ coverWindow (X := X) j, x ∉ tsupport (coverPoU (X := X) j) →
      KillsAt (coverRhoC j) g x

integrable_pairForm_piece

The j-th piece of the pairing is integrable.

theorem integrable_pairForm_piece {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) :
    Integrable (pairingIntegrand g η (coverRhoC j) (coverCenter j)
      (coverWindow (X := X) j)) volume

pairForm

The pairing ⟨η, g⟩ = ∬_X g∧η (up to the fixed constant 2i), as the PoU-weighted sum of planar chart integrals over the fixed Montel chart cover.

def pairForm {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X) (g : SmoothCOneForms X) :
    ℂ

pairingIntegrand_add

theorem pairingIntegrand_add {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (g₁ g₂ : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) (V : Set X) (z : ℂ) :
    pairingIntegrand (g₁ + g₂) η P y V z
      = pairingIntegrand g₁ η P y V z + pairingIntegrand g₂ η P y V z

pairingIntegrand_zsmul

theorem pairingIntegrand_zsmul {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (n : ℤ) (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) (V : Set X) (z : ℂ) :
    pairingIntegrand (n • g) η P y V z = n • pairingIntegrand g η P y V z

pairingIntegrand_smul

theorem pairingIntegrand_smul {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (r : ℝ) (g : SmoothCOneForms X)
    (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) (V : Set X) (z : ℂ) :
    pairingIntegrand (r • g) η P y V z = r • pairingIntegrand g η P y V z

pairingIntegrand_zero

theorem pairingIntegrand_zero {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X)
    (P : X → ℂ) (y : X) (V : Set X) (z : ℂ) :
    pairingIntegrand (0 : SmoothCOneForms X) η P y V z = 0

pairForm_add

theorem pairForm_add {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X)
    (g₁ g₂ : SmoothCOneForms X) :
    pairForm η (g₁ + g₂) = pairForm η g₁ + pairForm η g₂

pairForm_zero

theorem pairForm_zero {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X) :
    pairForm η (0 : SmoothCOneForms X) = 0

pairForm_zsmul

theorem pairForm_zsmul {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η : HolomorphicOneForms X) (n : ℤ)
    (g : SmoothCOneForms X) :
    pairForm η (n • g) = n • pairForm η g

pairForm_sum

theorem pairForm_sum {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {ι : Type*}
    (η : HolomorphicOneForms X) (s : Finset ι)
    (g : ι → SmoothCOneForms X) :
    pairForm η (∑ k ∈ s, g k) = ∑ k ∈ s, pairForm η (g k)

pairForm_eta_add

theorem pairForm_eta_add {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (η₁ η₂ : HolomorphicOneForms X)
    (g : SmoothCOneForms X) :
    pairForm (η₁ + η₂) g = pairForm η₁ g + pairForm η₂ g

pairForm_eta_smul

theorem pairForm_eta_smul {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] (c : ℂ) (η : HolomorphicOneForms X)
    (g : SmoothCOneForms X) :
    pairForm (c • η) g = c * pairForm η g

pairForm_eq_singleChart

The collapse lemma: if the (0,1)-form g is fiber-supported in a compact K inside an open window W of a single chart (centre c), the PoU pairing collapses to the single un-weighted chart-c integral:

pairForm η g = ∫_ℂ 𝟙_{chart_c''W}·(read01 g)_c·(localRep η)_c dA.

Per cover chart j: shrink the window to Vⱼ ∩ W (the kill condition holds on the difference since g dies off K ⊆ W), transport to the chart at c, and sum the PoU weights to 1.

theorem pairForm_eq_singleChart {X : Type*} [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] {g : SmoothCOneForms X}
    (hg : g ∈ OneFormsZeroOne X)
    (η : HolomorphicOneForms X) {c : X} {W K : Set X} (hWopen : IsOpen W)
    (hWsub : W ⊆ (chartAt (H := ℂ) c).source) (hK : IsCompact K) (hKW : K ⊆ W)
    (hgsupp : ∀ x, x ∉ K → (g x) = (0 : ℂ →L[ℝ] ℂ)) :
    pairForm η g = ∫ z, pairingIntegrand g η (fun _ => 1) c W z