32.5. PeriodLattice.JacobiLocalMap🔗

Jacobians.PeriodLattice.JacobiLocalMap — source

chartFormCoeff_center

chartFormCoeff at the chart center is the localRep self-evaluation (the jacobiEvalMatrix entry).

theorem chartFormCoeff_center (Q₀ : X) (i : Fin (genus X)) :
    chartFormCoeff (X := X) Q₀ i ((chartAt (H := ℂ) Q₀) Q₀)
      = Jacobians.Montel.localRep (periodBasisForm X i) Q₀ Q₀

localLiftChart_center

The chart primitive at the chart center takes its constant value (the segment degenerates).

theorem localLiftChart_center (Q₀ : X) (constants : Fin (genus X) → ℂ) (i : Fin (genus X)) :
    localLiftChart (X := X) Q₀ constants i ((chartAt (H := ℂ) Q₀) Q₀) = constants i

localLiftChart_hasDerivAt_center

HasDerivAt of the chart primitive at the chart center, with derivative the chart form coefficient: rewrite localLiftChart on a chart ball as constants i + g z − g z₀ for an analytic primitive g of chartFormCoeff (the localLiftChart_analyticAt mechanism), and read the derivative off g.

theorem localLiftChart_hasDerivAt_center (Q₀ : X) (constants : Fin (genus X) → ℂ)
    (i : Fin (genus X)) :
    HasDerivAt (localLiftChart (X := X) Q₀ constants i)
      (chartFormCoeff (X := X) Q₀ i ((chartAt (H := ℂ) Q₀) Q₀))
      ((chartAt (H := ℂ) Q₀) Q₀)

localLiftChart_hasStrictDerivAt_center

Strict differentiability of the chart primitive at the chart center (analytic ⟹ strict), with the derivative identified by localLiftChart_hasDerivAt_center.

theorem localLiftChart_hasStrictDerivAt_center (Q₀ : X) (constants : Fin (genus X) → ℂ)
    (i : Fin (genus X)) :
    HasStrictDerivAt (localLiftChart (X := X) Q₀ constants i)
      (chartFormCoeff (X := X) Q₀ i ((chartAt (H := ℂ) Q₀) Q₀))
      ((chartAt (H := ℂ) Q₀) Q₀)

jacobiMap

The local Jacobi map at a base-point family a : Fin g → X (Forster 21.4(a)): G(z)ᵢ = ∑ⱼ Φ̃_{a j, i}(z j), the sum of the chart primitives of ω_i at the a j, each read in its own chart coordinate z j.

noncomputable def jacobiMap (a : Fin (genus X) → X) (z : Fin (genus X) → ℂ) :
    Fin (genus X) → ℂ

jacobiCenter

The chart-coordinate center of the local Jacobi map.

noncomputable def jacobiCenter (a : Fin (genus X) → X) : Fin (genus X) → ℂ

jacobiMap_center

The local Jacobi map vanishes at the center (Φ̃ is normalized by constants = 0).

theorem jacobiMap_center (a : Fin (genus X) → X) :
    jacobiMap a (jacobiCenter a) = 0

jacobiDeriv

The Fréchet derivative of the local Jacobi map at the center: the continuous linear map v ↦ A.mulVec v with A = jacobiEvalMatrix a (assembled as a Pi of summed projections).

noncomputable def jacobiDeriv (a : Fin (genus X) → X) :
    (Fin (genus X) → ℂ) →L[ℂ] (Fin (genus X) → ℂ)

jacobiDeriv_apply

@[simp] theorem jacobiDeriv_apply (a : Fin (genus X) → X) (v : Fin (genus X) → ℂ)
    (i : Fin (genus X)) :
    jacobiDeriv a v i = ∑ j, jacobiEvalMatrix a i j * v j

jacobiMap_hasStrictFDerivAt

Strict differentiability of the local Jacobi map at the center, with derivative the evaluation matrix: assemble per-summand strict derivatives (HasStrictDerivAt.comp with the coordinate projections) through Finset.sum and Pi.

theorem jacobiMap_hasStrictFDerivAt (a : Fin (genus X) → X) :
    HasStrictFDerivAt (jacobiMap a) (jacobiDeriv a) (jacobiCenter a)

jacobiDerivEquiv

At a base-point family with invertible evaluation matrix, jacobiDeriv is (the coercion of) a continuous linear equivalence.

noncomputable def jacobiDerivEquiv (a : Fin (genus X) → X)
    (ha : (jacobiEvalMatrix (X := X) a).det ≠ 0) :
    (Fin (genus X) → ℂ) ≃L[ℂ] (Fin (genus X) → ℂ)

coe_jacobiDerivEquiv

theorem coe_jacobiDerivEquiv (a : Fin (genus X) → X)
    (ha : (jacobiEvalMatrix (X := X) a).det ≠ 0) :
    (jacobiDerivEquiv a ha : (Fin (genus X) → ℂ) →L[ℂ] (Fin (genus X) → ℂ))
      = jacobiDeriv a

jacobiMap_map_nhds

Forster 21.4(a), the open-image conclusion. At a base-point family with det A ≠ 0, the local Jacobi map sends neighbourhoods of the center to neighbourhoods of 0 (the inverse function theorem HasStrictFDerivAt.map_nhds_eq_of_equiv).

theorem jacobiMap_map_nhds (a : Fin (genus X) → X)
    (ha : (jacobiEvalMatrix (X := X) a).det ≠ 0) :
    Filter.map (jacobiMap a) (nhds (jacobiCenter a)) = nhds 0

exists_jacobiMap_map_nhds

The packaged 21.4(a) statement: a base-point family a (injective, rank-g evaluation matrix) at which the local Jacobi map G has G(center) = 0 and maps every neighbourhood of the center onto a neighbourhood of 0 ∈ ℂ^g.

theorem exists_jacobiMap_map_nhds :
    ∃ a : Fin (genus X) → X, Function.Injective a ∧
      (jacobiEvalMatrix (X := X) a).det ≠ 0 ∧
      jacobiMap a (jacobiCenter a) = 0 ∧
      ∀ V ∈ nhds (jacobiCenter a), jacobiMap a '' V ∈ nhds (0 : Fin (genus X) → ℂ)