21.4. LaurentTail.DimensionBookkeeping🔗

Jacobians.LaurentTail.DimensionBookkeeping — source

linearSystem_mono

L(D) is monotone in D: a deeper allowed pole set is a weaker constraint.

theorem linearSystem_mono {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    linearSystem (X := X) D₁ ≤ linearSystem (X := X) D₂

lSysInclusion

The inclusion L(D₁)/germZero → L(D₂)/germZero (first map of the chain).

noncomputable def lSysInclusion {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    lSysModule (X := X) D₁ →ₗ[ℂ] lSysModule (X := X) D₂

lSysInclusion_mk

@[simp] theorem lSysInclusion_mk {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂)
    (f : ↥(linearSystem (X := X) D₁)) :
    lSysInclusion h (Submodule.Quotient.mk f)
      = Submodule.Quotient.mk (Submodule.inclusion (linearSystem_mono h) f)

lSysInclusion_injective

Exactness at L(D₁): the inclusion of junk-free linear systems is injective.

theorem lSysInclusion_injective {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    Function.Injective (lSysInclusion (X := X) h)

tailMapCo_eq_zero_iff

α_D vanishes on an element iff it lies in L(D) (subtype form of ker_tailMap).

theorem tailMapCo_eq_zero_iff (D : Divisor X) (f : MeromorphicFunction X) :
    tailMapCo (X := X) D f = 0 ↔ f ∈ linearSystem (X := X) D

lSysToTailKernelAux

α_{D₁} restricted to L(D₂) lands in ker t^{D₁}_{D₂} (since t ∘ α_{D₁} = α_{D₂} kills L(D₂)).

noncomputable def lSysToTailKernelAux {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    ↥(linearSystem (X := X) D₂) →ₗ[ℂ] ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂))

lSysToTailKernelAux_coe

@[simp] theorem lSysToTailKernelAux_coe {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂)
    (f : ↥(linearSystem (X := X) D₂)) :
    ((lSysToTailKernelAux h f : ↥(tailSubspace (X := X) D₁)) : TailSpace X)
      = tailMap D₁ (f : MeromorphicFunction X)

lSysToTailKernel

The second map of the chain: α_{D₁} : L(D₂)/germZero → ker t^{D₁}_{D₂} (well defined on the junk-free quotient because germ-zero functions have no tail).

noncomputable def lSysToTailKernel {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    lSysModule (X := X) D₂ →ₗ[ℂ] ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂))

lSysToTailKernel_mk

@[simp] theorem lSysToTailKernel_mk {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂)
    (f : ↥(linearSystem (X := X) D₂)) :
    lSysToTailKernel h (Submodule.Quotient.mk f) = lSysToTailKernelAux h f

tailKernelToH1

The third map of the chain: ker t^{D₁}_{D₂} → H¹(D₁), the class-of map.

noncomputable def tailKernelToH1 (D₁ D₂ : Divisor X) :
    ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂)) →ₗ[ℂ] mittagLefflerH1 (X := X) D₁

tailKernelToH1_apply

@[simp] theorem tailKernelToH1_apply (D₁ D₂ : Divisor X)
    (Z : ↥(LinearMap.ker (tailTruncate (X := X) D₁ D₂))) :
    tailKernelToH1 D₁ D₂ Z
      = Submodule.Quotient.mk (Z : ↥(tailSubspace (X := X) D₁))

ker_lSysToTailKernel

Exactness at L(D₂): ker (α_{D₁}|_{L(D₂)}) = range (L(D₁) → L(D₂)) — a function in L(D₂) has vanishing D₁-tail iff it already lies in L(D₁).

theorem ker_lSysToTailKernel {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    LinearMap.ker (lSysToTailKernel (X := X) h)
      = LinearMap.range (lSysInclusion (X := X) h)

ker_tailKernelToH1

Exactness at ker t^{D₁}_{D₂}: a window tail maps to 0 in H¹(D₁) iff it is the D₁-tail of a global meromorphic function — which then automatically lies in L(D₂).

theorem ker_tailKernelToH1 {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    LinearMap.ker (tailKernelToH1 (X := X) D₁ D₂)
      = LinearMap.range (lSysToTailKernel (X := X) h)

ker_mittagLefflerTruncate_eq

Exactness at H¹(D₁): a class dies under the truncation H¹(D₁) → H¹(D₂) iff it is represented by a window tail (correct the representative by a global function).

theorem ker_mittagLefflerTruncate_eq {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    LinearMap.ker (mittagLefflerTruncate (X := X) h)
      = LinearMap.range (tailKernelToH1 (X := X) D₁ D₂)

finiteDimensional_ker_mittagLefflerTruncate

The relative kernel ker (H¹(D₁) → H¹(D₂)) is finite-dimensional — it is the image of the finite monomial window, with no finiteness assumption on the H¹s themselves.

theorem finiteDimensional_ker_mittagLefflerTruncate {D₁ D₂ : Divisor X} (h : D₁ ≤ D₂) :
    FiniteDimensional ℂ ↥(LinearMap.ker (mittagLefflerTruncate (X := X) h))

finrank_ker_mittagLefflerTruncate

Miranda Lemma 2.3 (Ch. VI §2, p. 181): for D₁ ≤ D₂,

dim ker (H¹(D₁) → H¹(D₂)) = (deg D₂ − l(D₂)) − (deg D₁ − l(D₁)).

Rank–nullity walked down the explicit chain: dim ker t = deg D₂ − deg D₁ monomials, of which α_{D₁}(L(D₂)) (dimension l(D₂) − l(D₁)) are realized; the rest is the relative kernel.

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