Generic points (Forster §21.3)

Unit: period-lattice-rank (docs/design/period-lattice-rank.md §6.2). There are genus X distinct points a₁,…,a_g ∈ X such that any ω ∈ Form1 X vanishing at all aⱼ is identically zero: Forster's proof is a strict descending induction on dim ⋂ⱼ ker (evalAt aⱼ), using that a nonzero holomorphic form is nonzero off any finite set (openness of the nonvanishing locus + RS.nonempty_open_diff_finite).

Main declarations: RS.isOpen_coeffAt_ne_zero, RS.exists_coeffAt_ne_zero_notMem, RS.exists_genericPoints, RS.det_genericMatrix_ne_zero.

noncomputable def RS.evalAtₗ {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) : Form1 X →ₗ[ℂ] ℂ

coeffAt x bundled as a ℂ-linear functional.

Equations

• RS.evalAtₗ x = { toFun := fun (η : RS.Form1 X) => RS.coeffAt x η, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem RS.evalAtₗ_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (x : X) (η : Form1 X) : (evalAtₗ x) η = coeffAt x η

theorem RS.isOpen_coeffAt_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (η : Form1 X) : IsOpen {x : X | coeffAt x η ≠ 0}

The nonvanishing locus of a form's coefficient is open.

theorem RS.exists_coeffAt_ne_zero_notMem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {η : Form1 X} (hη : η ≠ 0) (S : Finset X) : ∃ x ∉ S, coeffAt x η ≠ 0

A nonzero form is nonzero somewhere off any finite set (openness + avoidance).

def RS.genericKernel (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (s : Finset X) : Submodule ℂ (Form1 X)

The submodule of forms vanishing at every point of s.

Equations

• RS.genericKernel X s = { carrier := {η : RS.Form1 X | ∀ x ∈ s, RS.coeffAt x η = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem RS.mem_genericKernel {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {s : Finset X} {η : Form1 X} : η ∈ genericKernel X s ↔ ∀ x ∈ s, coeffAt x η = 0

theorem RS.genericKernel_anti {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {s t : Finset X} (h : s ⊆ t) : genericKernel X t ≤ genericKernel X s

theorem RS.genericKernel_empty {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : genericKernel X ∅ = ⊤

theorem RS.exists_finset_card_finrank_le {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (k : ℕ) : ∃ (s : Finset X), s.card = k ∧ Module.finrank ℂ ↥(genericKernel X s) ≤ genus X - k

Descending induction: after choosing k points, the kernel's finrank has dropped by (at least) k, saturating at ⊥ once k ≥ genus X.

theorem RS.exists_genericPoints {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (_hg : 1 ≤ genus X) : ∃ (a : Fin (genus X) → X), Function.Injective a ∧ ∀ (η : Form1 X), (∀ (j : Fin (genus X)), coeffAt (a j) η = 0) → η = 0

Forster 21.3: genus X distinct points such that any form vanishing at all of them is identically zero.

theorem RS.det_genericMatrix_ne_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {a : Fin (genus X) → X} (ha : ∀ (η : Form1 X), (∀ (j : Fin (genus X)), coeffAt (a j) η = 0) → η = 0) : (Matrix.of fun (i j : Fin (genus X)) => coeffAt (a j) ((basis X) i)).det ≠ 0

The generic-point evaluation matrix A i j := coeffAt (a j) (basis X i) is invertible (transpose of the natural evaluation map; §21.4(a)).