32.7. PeriodLattice.PeriodLatticeBasis🔗

Jacobians.PeriodLattice.PeriodLatticeBasis — source

exists_periodLattice_realBasis

Existence of a period ℝ-basis — the *single* classical input behind the Jacobian-as-complex-torus structure. The period lattice is generated, as a ℤ-module, by a real basis of ℂ^(genus X) ≅ ℝ^(2·genus X).

Dissection-free proof (Forster 21.4): discreteness + non-degeneracy make the lattice a ZLattice, and Mathlib's ZLattice theory produces the basis.

theorem exists_periodLattice_realBasis :
    ∃ b : Module.Basis (Fin (2 * genus X)) ℝ (Fin (genus X) → ℂ),
      truePeriodLattice X = Submodule.span ℤ (Set.range ⇑b)