32.4. PeriodLattice.JacobiBasePoints🔗

Jacobians.PeriodLattice.JacobiBasePoints — source

formEvalSelf

Evaluation of a holomorphic 1-form at a point, as a ℂ-linear functional: the chart-centre coefficient localRep α a a (the value of α at a on the unit coordinate tangent vector of the chart at a). Its vanishing is the chart-invariant meaning of "α(a) = 0" (the tangent fibre is 1-dimensional).

noncomputable def formEvalSelf (a : X) : HolomorphicOneForms X →ₗ[ℂ] ℂ where

formEvalSelf_apply

@[simp] theorem formEvalSelf_apply (a : X) (α : HolomorphicOneForms X) :
    formEvalSelf a α = Jacobians.Montel.localRep α a a

finrank_inf_ker_formEvalSelf

One-step kernel drop. If some α ∈ V has formEvalSelf a α ≠ 0, then cutting V by the kernel of the evaluation at a drops the dimension by exactly one (rank–nullity for the restricted functional, whose range is all of ℂ).

theorem finrank_inf_ker_formEvalSelf (V : Submodule ℂ (HolomorphicOneForms X))
    {α : HolomorphicOneForms X} (hωV : α ∈ V) {a : X} (hωa : formEvalSelf a α ≠ 0) :
    finrank ℂ ↥(V ⊓ LinearMap.ker (formEvalSelf (X := X) a))
      = finrank ℂ ↥V - 1

exists_finset_formEvalSelf_ker

The induction core: for every k ≤ g there is a k-element set of points whose common evaluation kernel has dimension exactly g − k.

theorem exists_finset_formEvalSelf_ker (k : ℕ) (hk : k ≤ genus X) :
    ∃ s : Finset X, s.card = k ∧
      finrank ℂ ↥(⨅ a ∈ s, LinearMap.ker (formEvalSelf (X := X) a)) = genus X - k

exists_jacobiBasePoints

Forster Lemma 21.3. There are g distinct points a j on X such that the only holomorphic 1-form whose coefficient vanishes at all of them is the zero form.

theorem exists_jacobiBasePoints :
    ∃ a : Fin (genus X) → X, Function.Injective a ∧
      ∀ α : HolomorphicOneForms X,
        (∀ j, Jacobians.Montel.localRep α (a j) (a j) = 0) → α = 0

jacobiEvalMatrix

The g × g evaluation matrix of the period basis forms at a point family: A i j = chart-centre coefficient of periodBasisForm X i at a j. This is the Jacobian matrix of Forster 21.4(a)'s local Jacobi map at the base point.

noncomputable def jacobiEvalMatrix (a : Fin (genus X) → X) :
    Matrix (Fin (genus X)) (Fin (genus X)) ℂ

jacobiEvalMatrix_apply

@[simp] theorem jacobiEvalMatrix_apply (a : Fin (genus X) → X) (i j : Fin (genus X)) :
    jacobiEvalMatrix a i j = Jacobians.Montel.localRep (periodBasisForm X i) (a j) (a j)

jacobiEvalMatrix_det_ne_zero

Rank g of the evaluation matrix (Forster 21.4(a)): at a family of base points with the 21.3 property, the evaluation matrix of the period basis is invertible (det ≠ 0). A nonzero left null vector v would make α = ∑ v i • ω_i = ambientIso X v a nonzero form vanishing at every a j.

theorem jacobiEvalMatrix_det_ne_zero {a : Fin (genus X) → X}
    (ha : ∀ α : HolomorphicOneForms X,
      (∀ j, Jacobians.Montel.localRep α (a j) (a j) = 0) → α = 0) :
    (jacobiEvalMatrix a).det ≠ 0

exists_jacobiBasePoints_det_ne_zero

Forster 21.3 + 21.4(a) rank statement, packaged: a family of g distinct base points at which the period-basis evaluation matrix is invertible.

theorem exists_jacobiBasePoints_det_ne_zero :
    ∃ a : Fin (genus X) → X, Function.Injective a ∧
      (jacobiEvalMatrix (X := X) a).det ≠ 0