21.9. LaurentTail.TailMap🔗

Jacobians.LaurentTail.TailMap — source

laurentCoeffAt

The n-th Laurent coefficient of f at p, read in the canonical chart at p (centre c_p = chartAt ℂ p p): the coefficient of (z − c_p)^n of the chart pullback f ∘ (chartAt ℂ p).symm.

noncomputable def laurentCoeffAt (f : X → ℂ) (p : X) (n : ℤ) : ℂ

laurentCoeffAt_eq_zero_of_lt_orderW

Coefficients below the order vanish (orderW *is* the chart-pullback meromorphic order).

theorem laurentCoeffAt_eq_zero_of_lt_orderW (f : MeromorphicFunction X) {p : X} {n : ℤ}
    (hn : (n : WithTop ℤ) < f.orderW p) : laurentCoeffAt f.toFun p n = 0

le_orderW_iff_laurentCoeffAt

The order↔coefficients bridge at a point (Miranda p. 181): orderW f p ≥ k iff all Laurent coefficients of f at p below k vanish.

theorem le_orderW_iff_laurentCoeffAt (f : MeromorphicFunction X) (p : X) (k : ℤ) :
    (k : WithTop ℤ) ≤ f.orderW p ↔ ∀ n : ℤ, n < k → laurentCoeffAt f.toFun p n = 0

laurentCoeffAt_add

theorem laurentCoeffAt_add (f g : MeromorphicFunction X) (p : X) (n : ℤ) :
    laurentCoeffAt (f + g).toFun p n
      = laurentCoeffAt f.toFun p n + laurentCoeffAt g.toFun p n

laurentCoeffAt_smul

theorem laurentCoeffAt_smul (a : ℂ) (f : MeromorphicFunction X) (p : X) (n : ℤ) :
    laurentCoeffAt (a • f).toFun p n = a * laurentCoeffAt f.toFun p n

laurentCoeffAt_eq_zero_of_germZero

Germ-zero functions have vanishing Laurent coefficients in every degree.

theorem laurentCoeffAt_eq_zero_of_germZero [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {f : MeromorphicFunction X}
    (hf : f ∈ germZeroSubmodule (X := X)) (p : X) (n : ℤ) :
    laurentCoeffAt f.toFun p n = 0

div_apply

The divisor of f evaluates to the (untop₀-read) order: div f p = (orderW f p)⁰. (NB div takes X explicitly *first*, so f.div must be type-ascribed before application — f.div p would feed p into the X slot.)

theorem div_apply [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (f : MeromorphicFunction X) (p : X) :
    (f.div : Divisor X) p = (f.orderW p).untop₀

tailEntries_support_finite

Finite support of the truncated tail: a nonzero entry at (p, n) with n < −D(p) forces div f p ≤ n < −D(p), confining (p, n) to finitely many pairs.

theorem tailEntries_support_finite [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (f : MeromorphicFunction X) :
    (Function.support fun q : X × ℤ =>
      if q.2 < -(D q.1) then laurentCoeffAt f.toFun q.1 q.2 else 0).Finite

tailEntries

The underlying tail of α_D f: the Laurent coefficients of f in degrees < −D(p).

noncomputable def tailEntries [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) (f : MeromorphicFunction X) : TailSpace X

tailEntries_apply

@[simp] theorem tailEntries_apply [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (f : MeromorphicFunction X) (q : X × ℤ) :
    tailEntries D f q = if q.2 < -(D q.1) then laurentCoeffAt f.toFun q.1 q.2 else 0

tailMap

Miranda's truncation map α_D : ℳ(X) → 𝒯[D](X) (Ch. VI p. 180), as a ℂ-linear map into the ambient tail space: truncate the full Laurent series of f to the degrees < −D(p).

noncomputable def tailMap [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) : MeromorphicFunction X →ₗ[ℂ] TailSpace X where

tailMap_apply

@[simp] theorem tailMap_apply [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) (f : MeromorphicFunction X) (q : X × ℤ) :
    tailMap D f q = if q.2 < -(D q.1) then laurentCoeffAt f.toFun q.1 q.2 else 0

tailMap_mem_tailSubspace

theorem tailMap_mem_tailSubspace [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) (f : MeromorphicFunction X) :
    tailMap D f ∈ tailSubspace D

tailMapCo

α_D co-restricted to its natural target 𝒯[D](X).

noncomputable def tailMapCo [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) :
    MeromorphicFunction X →ₗ[ℂ] ↥(tailSubspace (X := X) D)

tailMapCo_coe

@[simp] theorem tailMapCo_coe [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) (f : MeromorphicFunction X) :
    (tailMapCo D f : TailSpace X) = tailMap D f

ker_tailMap

L(D) = ker α_D (Miranda Ch. VI, p. 181): a meromorphic function lies in the complete linear system L(D) iff its D-truncated Laurent tail vanishes. This is the central bridge between the order-theoretic linearSystem and the Laurent-tail calculus.

theorem ker_tailMap [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) :
    LinearMap.ker (tailMap (X := X) D) = linearSystem (X := X) D

germZeroSubmodule_le_ker_tailMap

The germ-zero junk submodule is contained in ker α_D for every D (so α_D descends to the junk-free quotient lSysModule).

theorem germZeroSubmodule_le_ker_tailMap [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] (D : Divisor X) :
    germZeroSubmodule (X := X) ≤ LinearMap.ker (tailMap (X := X) D)

truncateRaw_tailMap

theorem truncateRaw_tailMap [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (f : MeromorphicFunction X) :
    truncateRaw D₂ (tailMap D₁ f) = tailMap D₂ f

tailTruncate_tailMapCo

theorem tailTruncate_tailMapCo [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) (f : MeromorphicFunction X) :
    tailTruncate D₁ D₂ (tailMapCo D₁ f) = tailMapCo D₂ f

mittagLefflerH1

Miranda's H¹(D) (Ch. VI Def. 2.4, p. 182): the cokernel of the truncation map, 𝒯[D](X) ⧸ range α_D — the space of Laurent tail divisors modulo those realized by global meromorphic functions.

abbrev mittagLefflerH1 [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) : Type _

h1TailDim

h¹(D) := dim_ℂ H¹(D) (finite for every D — Miranda Prop. 2.7, proved in Finiteness).

noncomputable def h1TailDim [T2Space X] [CompactSpace X] [ConnectedSpace X] [IsManifold 𝓘(ℂ) ω X]
    (D : Divisor X) : ℕ

mittagLefflerTruncate

The truncation t^{D₁}_{D₂} descends to the Mittag-Leffler quotients H¹(D₁) → H¹(D₂) (it maps realized tails to realized tails).

noncomputable def mittagLefflerTruncate [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    mittagLefflerH1 (X := X) D₁ →ₗ[ℂ] mittagLefflerH1 (X := X) D₂

mittagLefflerTruncate_mk

@[simp] theorem mittagLefflerTruncate_mk [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂)
    (Z : ↥(tailSubspace (X := X) D₁)) :
    mittagLefflerTruncate h (Submodule.Quotient.mk Z)
      = Submodule.Quotient.mk (tailTruncate D₁ D₂ Z)

mittagLefflerTruncate_surjective

The induced truncation H¹(D₁) → H¹(D₂) is surjective (Miranda p. 182).

theorem mittagLefflerTruncate_surjective [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [IsManifold 𝓘(ℂ) ω X] {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    Function.Surjective (mittagLefflerTruncate (X := X) h)