32.8. PeriodLattice.PeriodLatticeDiscrete🔗

Jacobians.PeriodLattice.PeriodLatticeDiscrete — source

exists_pairwise_disjoint_opens

Pairwise-disjoint open neighbourhoods of an injective finite family (T2 separation, intersected over the off-diagonal pairs).

theorem exists_pairwise_disjoint_opens {X : Type*} [TopologicalSpace X] [T2Space X] {n : ℕ}
    {a : Fin n → X} (ha : Function.Injective a) :
    ∃ O : Fin n → Set X, (∀ j, IsOpen (O j)) ∧ (∀ j, a j ∈ O j) ∧
      ∀ j k, j ≠ k → Disjoint (O j) (O k)

resAt_analyticAt_mul_sub_inv

Res_c (Φ·(z−c)⁻¹) = Φ(c) for Φ analytic at c (split off the constant term via dslope).

theorem resAt_analyticAt_mul_sub_inv {Φ : ℂ → ℂ} {c : ℂ} (hΦ : AnalyticAt ℂ Φ c) :
    Dolbeault.resAt (fun w => Φ w * (w - c)⁻¹) c = Φ c

pathPrimValue_congr_curve

pathPrimValue only depends on the curve (any continuity witness).

theorem pathPrimValue_congr_curve {η : HolomorphicOneForms X} {γ₁ γ₂ : ℝ → X} (h : γ₁ = γ₂)
    (h₁ : ContinuousOn γ₁ (Icc 0 1)) :
    pathPrimValue η γ₁ h₁ = pathPrimValue η γ₂ (h ▸ h₁)

truePeriodLattice_isolated_zero

Forster 21.4(b): the period lattice is isolated at 0. There is a neighbourhood of 0 ∈ ℂ^g meeting the period lattice only in 0.

theorem truePeriodLattice_isolated_zero :
    ∃ U ∈ 𝓝 (0 : Fin (genus X) → ℂ),
      ∀ v ∈ truePeriodLattice X, v ∈ U → v = 0