21.10. LaurentTail.TailSpace🔗

Jacobians.LaurentTail.TailSpace — source

TailSpace

The ambient space of Laurent tails on X: finitely supported families of coefficients, the entry at (p, n) being the coefficient of (z − c_p)^n in the tail at p.

abbrev TailSpace (X : Type*) : Type _

tailDegreeSet

The degree window of a divisor D: the index pairs (p, n) with n < −D(p).

def tailDegreeSet (D : Divisor X) : Set (X × ℤ)

mem_tailDegreeSet

theorem mem_tailDegreeSet {D : Divisor X} {q : X × ℤ} :
    q ∈ tailDegreeSet D ↔ q.2 < -(D q.1)

tailSubspace

Miranda's 𝒯[D](X) — the space of Laurent tail divisors for D: tails whose terms all have degree < −D(p). A ℂ-submodule of TailSpace X (Finsupp.supported).

noncomputable def tailSubspace (D : Divisor X) : Submodule ℂ (TailSpace X)

mem_tailSubspace_iff

theorem mem_tailSubspace_iff {D : Divisor X} {Z : TailSpace X} :
    Z ∈ tailSubspace D ↔ ∀ q : X × ℤ, ¬ q.2 < -(D q.1) → Z q = 0

tailSubspace_anti

The tail spaces are antitone in the divisor: a deeper cutoff (larger D) allows fewer terms.

theorem tailSubspace_anti {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    tailSubspace (X := X) D₂ ≤ tailSubspace D₁

truncateRaw

Truncation at depth D on the ambient tail space: kill all entries of degree ≥ −D(p) (Finsupp.filter, which is ℂ-linear).

noncomputable def truncateRaw (D : Divisor X) : TailSpace X →ₗ[ℂ] TailSpace X where

truncateRaw_apply

@[simp] theorem truncateRaw_apply (D : Divisor X) (Z : TailSpace X) (q : X × ℤ) :
    truncateRaw D Z q = if q.2 < -(D q.1) then Z q else 0

truncateRaw_mem_tailSubspace

theorem truncateRaw_mem_tailSubspace (D : Divisor X) (Z : TailSpace X) :
    truncateRaw D Z ∈ tailSubspace D

truncateRaw_eq_self_of_mem

A tail already supported in the window of D is unchanged by truncation at D.

theorem truncateRaw_eq_self_of_mem {D : Divisor X} {Z : TailSpace X} (hZ : Z ∈ tailSubspace D) :
    truncateRaw D Z = Z

tailTruncate

Miranda's truncation map t^{D₁}_{D₂} : 𝒯[D₁] → 𝒯[D₂] — keep only the terms of degree < −D₂(p). (Defined for any pair of divisors; it is surjective when D₁ ≤ D₂.)

noncomputable def tailTruncate (D₁ D₂ : Divisor X) :
    ↥(tailSubspace (X := X) D₁) →ₗ[ℂ] ↥(tailSubspace (X := X) D₂)

tailTruncate_coe

@[simp] theorem tailTruncate_coe (D₁ D₂ : Divisor X) (Z : ↥(tailSubspace (X := X) D₁)) :
    (tailTruncate D₁ D₂ Z : TailSpace X) = truncateRaw D₂ (Z : TailSpace X)

tailTruncate_surjective

Truncation is surjective for D₁ ≤ D₂ (a D₂-tail is in particular a D₁-tail, and is fixed by the truncation).

theorem tailTruncate_surjective {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    Function.Surjective (tailTruncate (X := X) D₁ D₂)

windowFinset

The (finite) window of degrees killed by t^{D₁}_{D₂}: pairs (p, n) with −D₂(p) ≤ n < −D₁(p). Nonempty windows force p into supp D₁ ∪ supp D₂.

noncomputable def windowFinset (D₁ D₂ : Divisor X) : Finset (X × ℤ)

mem_windowFinset

theorem mem_windowFinset {D₁ D₂ : Divisor X} {q : X × ℤ} :
    q ∈ windowFinset D₁ D₂ ↔ -(D₂ q.1) ≤ q.2 ∧ q.2 < -(D₁ q.1)

card_windowFinset

The monomial count: #window = ∑_{p ∈ supp D₁ ∪ supp D₂} (D₂(p) − D₁(p))⁺.

theorem card_windowFinset (D₁ D₂ : Divisor X) :
    (windowFinset D₁ D₂).card
      = ∑ p ∈ D₁.support ∪ D₂.support, (-(D₁ p) - -(D₂ p)).toNat

finrank_supported_finset

finrank of Finsupp.supported over (the coercion of) a Finset: the cardinality.

theorem finrank_supported_finset {α : Type*} (s : Finset α) :
    finrank ℂ ↥(Finsupp.supported ℂ ℂ (↑s : Set α)) = s.card

finiteDimensional_supported_finset

instance finiteDimensional_supported_finset {α : Type*} (s : Finset α) :
    FiniteDimensional ℂ ↥(Finsupp.supported ℂ ℂ (↑s : Set α))

ker_tailTruncate_eq

The kernel of t^{D₁}_{D₂} is exactly the window-supported tails, read inside 𝒯[D₁].

theorem ker_tailTruncate_eq (D₁ D₂ : Divisor X) :
    LinearMap.ker (tailTruncate (X := X) D₁ D₂)
      = (Finsupp.supported ℂ ℂ (↑(windowFinset D₁ D₂) : Set (X × ℤ))).comap
          (tailSubspace (X := X) D₁).subtype

kerTailTruncateEquiv

The kernel of t^{D₁}_{D₂} is linearly equivalent to the window-supported tail space.

noncomputable def kerTailTruncateEquiv [DecidableEq X] (D₁ D₂ : Divisor X) :
    ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂))
      ≃ₗ[ℂ] ↥(Finsupp.supported ℂ ℂ (↑(windowFinset D₁ D₂) : Set (X × ℤ)))

finiteDimensional_ker_tailTruncate

instance finiteDimensional_ker_tailTruncate (D₁ D₂ : Divisor X) :
    FiniteDimensional ℂ ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂))

finrank_ker_tailTruncate

The monomial count (Miranda Ch. VI, proof of Lemma 2.3, p. 181): for D₁ ≤ D₂,

dim ker t^{D₁}_{D₂} = deg D₂ − deg D₁.

theorem finrank_ker_tailTruncate {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    (finrank ℂ ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂)) : ℤ)
      = Divisor.deg X D₂ - Divisor.deg X D₁

tailCutoff

A divisor B ≥ A deep enough that t^{A}_{B} Z = 0: add to A the (effective) divisor ∑_{(p,n) ∈ supp Z} (−n − A(p))⁺ · p.

noncomputable def tailCutoff (A : Divisor X) (Z : TailSpace X) : Divisor X

le_tailCutoff

theorem le_tailCutoff (A : Divisor X) (Z : TailSpace X) : A ≤ tailCutoff A Z

neg_tailCutoff_le_of_mem_support

Every entry of Z has degree ≥ −(tailCutoff A Z)(p): the cutoff is deep enough.

theorem neg_tailCutoff_le_of_mem_support (A : Divisor X) (Z : TailSpace X) {q : X × ℤ}
    (hq : q ∈ Z.support) : -(tailCutoff A Z q.1) ≤ q.2

truncateRaw_tailCutoff

Deep truncation kills the tail: t^{A}_{tailCutoff A Z} Z = 0.

theorem truncateRaw_tailCutoff (A : Divisor X) (Z : TailSpace X) :
    truncateRaw (tailCutoff A Z) Z = 0