32.9. PeriodLattice.PeriodLatticeNondegenerate🔗

Jacobians.PeriodLattice.PeriodLatticeNondegenerate — source

eventually_const_of_re_le

Local maximum of Re forces local constancy (the open-mapping dichotomy): an analytic function whose real part has a local maximum at z₀ is locally constant at z₀.

theorem eventually_const_of_re_le {H : ℂ → ℂ} {z₀ : ℂ} (hH : AnalyticAt ℂ H z₀)
    (hmax : ∀ᶠ z in 𝓝 z₀, (H z).re ≤ (H z₀).re) :
    ∀ᶠ z in 𝓝 z₀, H z = H z₀

exists_re_dotProduct_repr

Every ℝ-linear functional on ℂ^g is v ↦ Re (∑ⱼ dⱼ·vⱼ) for some d : ℂ^g (dⱼ = λ(eⱼ) − λ(i·eⱼ)·i).

theorem exists_re_dotProduct_repr {n : ℕ} (l : (Fin n → ℂ) →ₗ[ℝ] ℝ) :
    ∃ d : Fin n → ℂ, ∀ v : Fin n → ℂ, (∑ j, d j * v j).re = l v

span_real_truePeriodLattice_eq_top

Forster 21.4(c): the period lattice is non-degenerate — its real span is all of ℂ^g. A nonzero killing functional Re ⟨d, ·⟩ would make u = Re ⟨d, periodVec (smoothPath x₀ ·)⟩ a global continuous function that is locally the real part of an analytic chart primitive; the maximum principle (open-mapping dichotomy) forces u constant, all chart coefficients of ∑ dⱼωⱼ vanish, and d = 0 — contradiction.

theorem span_real_truePeriodLattice_eq_top :
    Submodule.span ℝ ((truePeriodLattice X : Set (Fin (genus X) → ℂ))) = ⊤