27.12. TailDuality.TailMultiplicationH1🔗

Jacobians.TailDuality.TailMultiplicationH1 — source

MulLevelLE

The standing order condition for μ_ψ : 𝒯[A] → 𝒯[B] to be compatible with realization: A − B ≤ ord ψ pointwise.

def MulLevelLE (ψ : MeromorphicFunction X) (A B : Divisor X) : Prop

MulLevelLE.hE

theorem MulLevelLE.hE {ψ : MeromorphicFunction X} {A B : Divisor X} (h : MulLevelLE ψ A B) :
    ∀ p : X, ((-(B p) : ℤ) : WithTop ℤ) ≤ ψ.orderW p + ((-(A p) : ℤ) : WithTop ℤ)

mulLevelLE_of_mem

Membership ψ ∈ L(C) gives the level condition for A := B − C-type shifts: MulLevelLE ψ (B - C) B.

theorem mulLevelLE_of_mem [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {ψ : MeromorphicFunction X} {C : Divisor X}
    (hψ : ψ ∈ linearSystem (X := X) C) (B : Divisor X) :
    MulLevelLE ψ (B - C) B

mulLevelLE_add_div

The exact shift A := B + div ψ satisfies the level condition.

theorem mulLevelLE_add_div [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    [Nonempty X] (ψ : MeromorphicFunction X) (B : Divisor X) :
    MulLevelLE ψ (B + (ψ.div : Divisor X)) B

tailMulCo

μ_ψ co-restricted between tail levels (the target membership is unconditional — the operator truncates at B by construction).

noncomputable def tailMulCo [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (ψ : MeromorphicFunction X) (A B : Divisor X) :
    ↥(tailSubspace (X := X) A) →ₗ[ℂ] ↥(tailSubspace (X := X) B)

tailMulCo_coe

@[simp] theorem tailMulCo_coe [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (ψ : MeromorphicFunction X) (A B : Divisor X)
    (Z : ↥(tailSubspace (X := X) A)) :
    (tailMulCo ψ A B Z : TailSpace X) = tailMul ψ B (Z : TailSpace X)

tailMulH1

The H¹-level multiplication action (Miranda Problem VI.2.J): μ_ψ descends to the Mittag-Leffler quotients under the level condition (realized tails map to realized tails by Miranda (2.2)).

noncomputable def tailMulH1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (ψ : MeromorphicFunction X) {A B : Divisor X}
    (h : MulLevelLE ψ A B) :
    mittagLefflerH1 (X := X) A →ₗ[ℂ] mittagLefflerH1 (X := X) B

tailMulH1_mk

@[simp] theorem tailMulH1_mk [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (ψ : MeromorphicFunction X) {A B : Divisor X}
    (h : MulLevelLE ψ A B) (Z : ↥(tailSubspace (X := X) A)) :
    tailMulH1 ψ h (Submodule.Quotient.mk Z) = Submodule.Quotient.mk (tailMulCo ψ A B Z)

psi_mul_inv_eventually_one

For ψ whose germ survives somewhere (hence everywhere — orderW_ne_top_of_exists), ψ·ψ⁻¹ has germ 1 at every point.

theorem psi_mul_inv_eventually_one [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (ψ : MeromorphicFunction X)
    (hψ : ∃ x, ψ.orderW x ≠ ⊤) (p : X) :
    ∀ᶠ z in 𝓝[≠] ((chartAt (H := ℂ) p) p),
      ψ.toFun ((chartAt (H := ℂ) p).symm z)
        * (ψ⁻¹).toFun ((chartAt (H := ℂ) p).symm z) = 1

tailMul_tailMul_inv

The composite identity μ_ψ(μ_{ψ⁻¹}(W)) = W on 𝒯[B] at the exact shift A = B + div ψ: the coefficients of ψ·(A-tail of ψ⁻¹·(tail of W)) below −B are those of ψ·ψ⁻¹·(tail of W) = tail of W, because the dropped part has order ≥ ord ψ − A ≥ −B.

theorem tailMul_tailMul_inv [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    [Nonempty X] (ψ : MeromorphicFunction X) (hψ : ∃ x, ψ.orderW x ≠ ⊤)
    (B : Divisor X) (W : ↥(tailSubspace (X := X) B)) :
    tailMul ψ B (tailMul ψ⁻¹ (B + (ψ.div : Divisor X)) (W : TailSpace X))
      = (W : TailSpace X)

tailMulH1_surjective

Surjectivity of the H¹ multiplication action (Forster 17.8): for ψ with surviving germ, every class of H¹(B) is hit — the preimage is the ψ⁻¹-image at the exact shift B + div ψ, which lies in the (coarser) 𝒯[A] since A ≤ B + div ψ.

theorem tailMulH1_surjective [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    [Nonempty X] (ψ : MeromorphicFunction X) (hψ : ∃ x, ψ.orderW x ≠ ⊤)
    {A B : Divisor X} (h : MulLevelLE ψ A B) :
    Function.Surjective (tailMulH1 ψ h)

comp_tailMulH1_ne_zero

For λ ≠ 0 and ψ with surviving germ, λ ∘ T̄_ψ ≠ 0 — the dimension input for the Λ-side of the Serre-duality pigeonhole (Forster 17.9).

theorem comp_tailMulH1_ne_zero [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    [Nonempty X] {B : Divisor X}
    (φ : Module.Dual ℂ (mittagLefflerH1 (X := X) B)) (hφ : φ ≠ 0)
    (ψ : MeromorphicFunction X) (hψ : ∃ x, ψ.orderW x ≠ ⊤)
    {A : Divisor X} (h : MulLevelLE ψ A B) :
    φ.comp (tailMulH1 ψ h) ≠ 0