27.11. TailDuality.TailMultiplication🔗

Jacobians.TailDuality.TailMultiplication — source

finite_setOf_laurentCoeff_ne_zero_lt

For a meromorphic germ, only finitely many Laurent coefficients below any level are nonzero.

theorem finite_setOf_laurentCoeff_ne_zero_lt {g : ℂ → ℂ} {c : ℂ} (hg : MeromorphicAt g c)
    (b : ℤ) : {n : ℤ | n < b ∧ laurentCoeff g c n ≠ 0}.Finite

tailFnAt

The tail polynomial of Z at p, as an actual function: tailFnAt Z p (z) = ∑_{(p,n) ∈ supp Z} Z(p,n)·(z − c_p)^n.

noncomputable def tailFnAt (Z : TailSpace X) (p : X) : ℂ → ℂ

tailFnAt_def

theorem tailFnAt_def (Z : TailSpace X) (p : X) :
    tailFnAt Z p = fun z => ∑ q ∈ Z.support,
      (if q.1 = p then Z q * (z - (chartAt (H := ℂ) p) p) ^ q.2 else 0)

meromorphicAt_tailFnAt

theorem meromorphicAt_tailFnAt (Z : TailSpace X) (p : X) :
    MeromorphicAt (tailFnAt Z p) ((chartAt (H := ℂ) p) p)

laurentCoeff_tailFnAt

The coefficients of the tail polynomial are the tail entries.

theorem laurentCoeff_tailFnAt (Z : TailSpace X) (p : X) (n : ℤ) :
    laurentCoeff (tailFnAt Z p) ((chartAt (H := ℂ) p) p) n = Z (p, n)

tailFnAt_add

The tail polynomial is additive in Z.

theorem tailFnAt_add (Z₁ Z₂ : TailSpace X) (p : X) (z : ℂ) :
    tailFnAt (Z₁ + Z₂) p z = tailFnAt Z₁ p z + tailFnAt Z₂ p z

tailFnAt_smul

The tail polynomial is homogeneous in Z.

theorem tailFnAt_smul (c : ℂ) (Z : TailSpace X) (p : X) (z : ℂ) :
    tailFnAt (c • Z) p z = c * tailFnAt Z p z

tailFnAt_eq_zero_of_notMem

For p outside the base points of Z, the tail polynomial vanishes.

theorem tailFnAt_eq_zero_of_notMem (Z : TailSpace X) (p : X)
    (hp : p ∉ Z.support.image Prod.fst) (z : ℂ) : tailFnAt Z p z = 0

tailMulFun

The entries of μ_ψ(Z) at target level E: the coefficients of ψ·(tail polynomial), truncated below −E.

noncomputable def tailMulFun (ψ : MeromorphicFunction X) (E : Divisor X) (Z : TailSpace X) :
    (X × ℤ) → ℂ

meromorphicAt_psi_mul_tailFnAt

theorem meromorphicAt_psi_mul_tailFnAt (ψ : MeromorphicFunction X) (Z : TailSpace X) (p : X) :
    MeromorphicAt (fun z => ψ.toFun ((chartAt (H := ℂ) p).symm z) * tailFnAt Z p z)
      ((chartAt (H := ℂ) p) p)

finite_support_tailMulFun

theorem finite_support_tailMulFun (ψ : MeromorphicFunction X) (E : Divisor X)
    (Z : TailSpace X) : (Function.support (tailMulFun ψ E Z)).Finite

tailMulRaw

μ_ψ(Z) as a tail divisor.

noncomputable def tailMulRaw (ψ : MeromorphicFunction X) (E : Divisor X) (Z : TailSpace X) :
    TailSpace X

tailMulRaw_apply

theorem tailMulRaw_apply (ψ : MeromorphicFunction X) (E : Divisor X) (Z : TailSpace X)
    (q : X × ℤ) : tailMulRaw ψ E Z q = tailMulFun ψ E Z q

tailMulRaw_mem

theorem tailMulRaw_mem (ψ : MeromorphicFunction X) (E : Divisor X) (Z : TailSpace X) :
    tailMulRaw ψ E Z ∈ tailSubspace (X := X) E

tailMul

Miranda's multiplication operator μ_ψ (Ch. VI p. 179) at target level E, as a linear endomorphism of the ambient tail space (range in 𝒯[E] by tailMulRaw_mem).

noncomputable def tailMul (ψ : MeromorphicFunction X) (E : Divisor X) :
    TailSpace X →ₗ[ℂ] TailSpace X where

tailMul_apply

theorem tailMul_apply (ψ : MeromorphicFunction X) (E : Divisor X) (Z : TailSpace X)
    (q : X × ℤ) :
    tailMul ψ E Z q = if q.2 < -(E q.1)
      then laurentCoeff
        (fun z => ψ.toFun ((chartAt (H := ℂ) q.1).symm z) * tailFnAt Z q.1 z)
        ((chartAt (H := ℂ) q.1) q.1) q.2
      else 0

tailMul_tailMap

Miranda (2.2): μ_ψ(α_D f) = α_E(ψ·f) whenever −E ≤ ord ψ + (−D) pointwise — the re-truncated coefficients of ψ·(D-tail of f) and of ψ·f agree below −E, because ψ times the complementary part of f has order ≥ ord ψ − D ≥ −E.

theorem tailMul_tailMap [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (ψ f : MeromorphicFunction X) (D E : Divisor X)
    (hE : ∀ p : X, ((-(E p) : ℤ) : WithTop ℤ) ≤ ψ.orderW p + ((-(D p) : ℤ) : WithTop ℤ)) :
    tailMul ψ E (tailMap (X := X) D f) = tailMap (X := X) E (ψ * f)