A machine-checked solution to the Jacobians challenge

9.4. JacobianConstruction.PeriodLattice🔗

Jacobians.JacobianConstruction.PeriodLattice — source

exists_nbhd_cover

Generic neighborhood cover of a path: given an open-neighborhood assignment W y ∋ y, a continuous γ is covered segment-by-segment, each segment landing in some W (x k). (Generalizes exists_chartCover from chart sources to W.)

theorem exists_nbhd_cover (γ : ℝ → X) (hγ : Continuous γ)
    (W : X → Set X) (hW_open : ∀ y, IsOpen (W y)) (hW_mem : ∀ y, y ∈ W y) :
    ∃ (n : ℕ) (_hn : 0 < n) (x : Fin n → X),
      ∀ (k : Fin n) (s : ℝ),
        (k : ℝ) / n ≤ s → s ≤ ((k : ℝ) + 1) / n → γ s ∈ W (x k)

locConst

f is locally constant at x: eventually equal to f x.

def locConst (f : X → Y) (x : X) : Prop

isOpen_locConst

The set of points where f is locally constant is open.

theorem isOpen_locConst (f : X → Y) : IsOpen {x | locConst f x}

properNbhd

Proper preimage-neighborhood lemma (Forster 4.21b): for a proper f, an open V containing the fibre f⁻¹{x} has an open neighborhood U ∋ x with f⁻¹U ⊆ V. (From f being a closed map.) Used to shrink the disjoint local-homeo sheets over a fibre to a common base neighborhood — the key step in the covering structure off the branch locus (Forster 4.22).

theorem properNbhd [TopologicalSpace Y] {f : X → Y} (hf : IsProperMap f) (x : Y) {V : Set X}
    (hV : IsOpen V) (hsub : f ⁻¹' {x} ⊆ V) :
    ∃ U : Set Y, IsOpen U ∧ x ∈ U ∧ f ⁻¹' U ⊆ V

HopValid

A valid chart-ball hop Q₀ → Q: Q is in Q₀'s chart source and the affine segment between their chart images stays in the chart target. Exactly the hypotheses ChartBallPathSmooth needs.

def HopValid [ChartedSpace ℂ X] (Q₀ Q : X) : Prop

hopNbhd

The HopValid-validity neighborhood of y (open, contains y).

def hopNbhd [ChartedSpace ℂ X] (y : X) : Set X

isOpen_hopNbhd

theorem isOpen_hopNbhd [ChartedSpace ℂ X] (y : X) : IsOpen (hopNbhd y)

self_mem_hopNbhd

theorem self_mem_hopNbhd [ChartedSpace ℂ X] (y : X) : y ∈ hopNbhd y

hopValid_of_mem_hopNbhd

theorem hopValid_of_mem_hopNbhd [ChartedSpace ℂ X] {y Q : X} (h : Q ∈ hopNbhd y) : HopValid y Q

chartPullback

Chart pullback of f at x.

noncomputable def chartPullback [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    (f : X → Y) (x : X) : ℂ → ℂ

analyticAt_chartPullback

theorem analyticAt_chartPullback [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x : X) :
    AnalyticAt ℂ (chartPullback f x) ((chartAt ℂ x) x)

chartPullback_eventuallyConst_iff_locConst

theorem chartPullback_eventuallyConst_iff_locConst [TopologicalSpace Y] [ChartedSpace ℂ X]
    [ChartedSpace ℂ Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x : X) :
    (∀ᶠ z in 𝓝 ((chartAt ℂ x) x),
      chartPullback f x z = chartPullback f x ((chartAt ℂ x) x))
    ↔ locConst f x

locConst_iff_pullback_const_fixedChart

Bridge with a fixed target chart. For x in the source chart of x₀ whose image f x lies in the *fixed* target chart of x₀, local constancy of f at x is equivalent to the (single, x₀-based) chart pullback being eventually constant at φ₀ x.

theorem locConst_iff_pullback_const_fixedChart [TopologicalSpace Y] [ChartedSpace ℂ X]
    [ChartedSpace ℂ Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x₀ x : X)
    (hxφ : x ∈ (chartAt ℂ x₀).source)
    (hfxψ : f x ∈ (chartAt ℂ (f x₀)).source) :
    locConst f x ↔
      ∀ᶠ z in 𝓝 ((chartAt ℂ x₀) x),
        chartPullback f x₀ z = chartPullback f x₀ ((chartAt ℂ x₀) x)

criticalSet

Critical set of a holomorphic map between complex 1-manifolds.

Defined as Jacobians.Discharge.Manifold.criticalSetGeneral f — the set of points at which f is not locally injective. Classically equivalent to {x | mfderiv f x = 0} for analytic maps between complex 1-manifolds (criticalSet_iff_chart_pullback_deriv_zero / Forster §I.7); the local-injectivity definition is the one supported by the imported infrastructure, which gives closedness, ne-univ, and finiteness directly.

def criticalSet (f : X → Y) : Set X

branchLocus

Branch locus: the image of the critical set.

def branchLocus (f : X → Y) : Set Y

isClosed_criticalSet

Critical set is closed. The not-locally-injective set is closed via isClosed_criticalSetGeneral.

theorem isClosed_criticalSet [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y] (f : X → Y)
    (_hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    IsClosed (criticalSet f)

isProperMap_of_contMDiff

A holomorphic map from a compact Riemann surface is proper (Forster §4.20): a continuous map from a compact space to a T2 space is proper. This is what makes the branched-cover theory (§4.22–4.25) available: a proper local homeomorphism is a covering map.

theorem isProperMap_of_contMDiff [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [CompactSpace X] [T2Space Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    IsProperMap f

nhds_le_map_of_chartPullback_not_eventuallyConst

Local open mapping at x (provided the chart pullback is not locally constant there): f sends neighborhoods of x to neighborhoods of f x. This is the heart of the open mapping theorem, transferred through the charts.

theorem nhds_le_map_of_chartPullback_not_eventuallyConst [TopologicalSpace Y] [ChartedSpace ℂ X]
    [ChartedSpace ℂ Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (x : X)
    (hnc : ¬ ∀ᶠ z in 𝓝 ((chartAt ℂ x) x),
      chartPullback f x z = chartPullback f x ((chartAt ℂ x) x)) :
    𝓝 (f x) ≤ Filter.map f (𝓝 x)

isClosed_locConst

The set of points where f is locally constant is closed (equivalently, its complement is open), via the identity theorem.

theorem isClosed_locConst [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y] (f : X → Y)
    (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    IsClosed {x | locConst f x}

chartPullback_not_eventuallyConst

Globalized identity theorem. The chart pullback of a non-constant holomorphic map is not locally constant at any chart image.

theorem chartPullback_not_eventuallyConst [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [Nonempty Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (x : X) :
    ¬ ∀ᶠ z in 𝓝 ((chartAt ℂ x) x),
      chartPullback f x z = chartPullback f x ((chartAt ℂ x) x)

isOpenMap_of_nonconstant

A non-constant holomorphic map between Riemann surfaces is an open map. Assembled from the open-mapping transfer nhds_le_map_of_chartPullback_not_eventuallyConst and the non-constancy lemma chartPullback_not_eventuallyConst.

theorem isOpenMap_of_nonconstant [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [Nonempty Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    IsOpenMap f

surjective_of_nonconstant

A non-constant holomorphic map between compact connected Riemann surfaces is surjective: its range is open (open mapping), closed (continuous image of compact in a T2 space), and nonempty, hence clopen, hence all of the connected target Y.

theorem surjective_of_nonconstant [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [CompactSpace X] [T2Space Y] [ConnectedSpace Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    Function.Surjective f

isLocalHomeoOffCritical

Local homeomorphism off the critical set (Forster §4.4): where f is locally injective (x ∉ criticalSet f, i.e. by definition ∃ U ∈ 𝓝 x, InjOn f U), it restricts to an open injection on a neighborhood — open via the open-mapping theorem, injective by hypothesis. Together with isProperMap_of_contMDiff this is the input to the covering structure off the branch locus.

theorem isLocalHomeoOffCritical [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [Nonempty Y] (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {x : X} (hx : x ∉ criticalSet f) :
    ∃ U : Set X, IsOpen U ∧ x ∈ U ∧ Set.InjOn f U ∧ IsOpen (f '' U)

isCoveringMapOn_compl_branchLocus

Covering off the branch locus (Forster 4.22): a non-constant holomorphic map restricts to a covering map on the complement of its (finite) branch locus. Via Mathlib's IsCoveringMapOn.of_openPartialHomeomorph (the proper-local-homeo ⇒ covering theorem — Mathlib already has it, so no hand-built f⁻¹U ≃ₜ U × fibre): off the branch locus every fibre point is off criticalSet, so isLocalHomeoOffCritical gives an open injective neighborhood, packaged as an OpenPartialHomeomorph whose toFun is f.

theorem isCoveringMapOn_compl_branchLocus [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [T2Space X] [CompactSpace X]
    [T2Space Y] [ConnectedSpace Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    IsCoveringMapOn f (Set.univ \ branchLocus f)

isCoveringMap_restrictPreimage_compl_branchLocus

Subtype corestriction of the off-branch covering. Bridges isCoveringMapOn_compl_branchLocus (an IsCoveringMapOn on the *set* univ ∖ branchLocus f) to a genuine IsCoveringMap of the corestricted map ↥(f ⁻¹' (univ ∖ branchLocus f)) → ↥(univ ∖ branchLocus f), via Mathlib's IsCoveringMapOn.isCoveringMap_restrictPreimage.

This is the form Mathlib.Topology.Homotopy.Lifting consumes: it unlocks IsCoveringMap.liftPath (path lifting, Forster §4.14) and IsCoveringMap.liftPath_apply_one_eq_of_homotopicRel (monodromy / homotopy invariance of lift endpoints) — the toolkit for assembling the lifted loops in exists_preimageCycle_of_off_branchLocus (relocated to Jacobians/MeromorphicTrace/TracePullback.lean, where the genuine ambientPullbackJac lives).

theorem isCoveringMap_restrictPreimage_compl_branchLocus [TopologicalSpace Y] [ChartedSpace ℂ X]
    [ChartedSpace ℂ Y] [ConnectedSpace X] [T2Space X] [CompactSpace X]
    [T2Space Y] [ConnectedSpace Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    IsCoveringMap ((Set.univ \ branchLocus f).restrictPreimage f)

fiber_finite_off_branchLocus

Fibres off the branch locus are finite. For y ∉ branchLocus f every preimage x is a non-critical point, where f is locally injective (isLocalHomeoOffCritical), so x is isolated in the fibre ⟹ the fibre is IsDiscrete; it is also closed in compact X ⟹ compact, hence finite. This is the sheet count of the cover over y (classically = deg f) — the foundation of the §3 preimage-cycle lift. Note: unlike fibres_finite_of_connectivity_hypothesis (which assumes the global identity theorem), this is unconditional off the branch locus, since isLocalHomeoOffCritical holds there.

theorem fiber_finite_off_branchLocus [TopologicalSpace Y] [ChartedSpace ℂ X] [ChartedSpace ℂ Y]
    [ConnectedSpace X] [T2Space X] [CompactSpace X]
    [T2Space Y] [ConnectedSpace Y]
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {y : Y} (hy : y ∉ branchLocus f) :
    (f ⁻¹' {y}).Finite

truePeriodLattice

True period lattice: ℤ-span of period vectors of closed loops.

noncomputable def truePeriodLattice (X : Type*) [TopologicalSpace X]
    [T2Space X] [CompactSpace X] [ConnectedSpace X] [Nonempty X]
    [ChartedSpace ℂ X] [IsManifold 𝓘(ℂ) ω X] :
    Submodule ℤ (Fin (genus X) → ℂ)

periodVec_mem_truePeriodLattice_of_closed

Any closed-smooth-loop period vector is in the period lattice.

theorem periodVec_mem_truePeriodLattice_of_closed (γ : ℝ → X)
    (hγ : IsClosedSmoothLoop γ) :
    periodVec γ ∈ truePeriodLattice X

periodVec_reverse

Period vector reverses sign under path reversal. Classical fact: ∫_{reverse γ} ω = -∫_γ ω. Applied componentwise to the basis forms. The α-independent differentiability hypothesis is inherited from lineIntegral_reverse.

theorem periodVec_reverse (γ : ℝ → X)
    (hdiff : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ (1 - t))).toFun ∘ γ) (1 - t)) :
    periodVec (reverse γ) = -periodVec γ

periodVec_concat

Period vector is additive under path concatenation. Classical fact: ∫_{γ ∗ γ'} ω = ∫_γ ω + ∫_{γ'} ω. Applied componentwise to basis forms. Hypotheses (integrability per basis form + pointwise a.e. identities from the pathSpeed chain rule on each half) are per-i quantified versions of lineIntegral_concat's hypotheses.

theorem periodVec_concat (γ γ' : ℝ → X)
    (hint_γ : ∀ i : Fin (genus X), IntervalIntegrable
      (fun u => (periodBasisForm X i).toFun (γ u) (pathSpeed γ u)) volume 0 1)
    (hint_γ' : ∀ i : Fin (genus X), IntervalIntegrable
      (fun u => (periodBasisForm X i).toFun (γ' u) (pathSpeed γ' u)) volume 0 1)
    (hint_concat_left : ∀ i : Fin (genus X), IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun ((concat γ γ') t)
        (pathSpeed (concat γ γ') t)) volume 0 (1/2))
    (hint_concat_right : ∀ i : Fin (genus X), IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun ((concat γ γ') t)
        (pathSpeed (concat γ γ') t)) volume (1/2) 1)
    (h_ae_left : ∀ i : Fin (genus X), ∀ᵐ t ∂(volume.restrict (Set.uIoc (0 : ℝ) (1/2))),
      (periodBasisForm X i).toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t) =
        (2 : ℂ) * (periodBasisForm X i).toFun (γ (2 * t)) (pathSpeed γ (2 * t)))
    (h_ae_right : ∀ i : Fin (genus X), ∀ᵐ t ∂(volume.restrict (Set.uIoc ((1 : ℝ)/2) 1)),
      (periodBasisForm X i).toFun ((concat γ γ') t) (pathSpeed (concat γ γ') t) =
        (2 : ℂ) * (periodBasisForm X i).toFun (γ' (2 * t - 1)) (pathSpeed γ' (2 * t - 1))) :
    periodVec (concat γ γ') = periodVec γ + periodVec γ'

mk_periodVec_concat_eq_add

Abel-Jacobi additivity under concatenation. Classical fact: concatenating a path P → Q with a path Q → R corresponds to adding their Jacobian-valued classes. Takes the same per-basis-form hypotheses as periodVec_concat.

theorem mk_periodVec_concat_eq_add
    (γ γ' : ℝ → X) (hperiod : periodVec (concat γ γ') = periodVec γ + periodVec γ') :
    (QuotientAddGroup.mk (periodVec (concat γ γ')) :
      (Fin (genus X) → ℂ) ⧸ (truePeriodLattice X).toAddSubgroup) =
      QuotientAddGroup.mk (periodVec γ) + QuotientAddGroup.mk (periodVec γ')

periodVec_sub_mem_truePeriodLattice

Abel–Jacobi well-definedness (lattice form). If two smooth paths share endpoints, their period vectors differ by a lattice element. The concatenation γ₁ ∗ reverse γ₂ must itself be a closed smooth loop (passed in as hsmooth).

theorem periodVec_sub_mem_truePeriodLattice
    (γ₁ γ₂ : ℝ → X) (_h0 : γ₁ 0 = γ₂ 0)
    (hsmooth : IsClosedSmoothLoop (concat γ₁ (reverse γ₂)))
    (hconcat : periodVec (concat γ₁ (reverse γ₂)) =
      periodVec γ₁ - periodVec γ₂) :
    periodVec γ₁ - periodVec γ₂ ∈ truePeriodLattice X

mk_periodVec_eq_of_endpoints

Abel–Jacobi well-definedness (quotient form). Two smooth paths sharing both endpoints map to the same element of (Fin (genus X) → ℂ) ⧸ truePeriodLattice X.

theorem mk_periodVec_eq_of_endpoints
    (γ₁ γ₂ : ℝ → X) (h0 : γ₁ 0 = γ₂ 0)
    (hsmooth : IsClosedSmoothLoop (concat γ₁ (reverse γ₂)))
    (hconcat : periodVec (concat γ₁ (reverse γ₂)) =
      periodVec γ₁ - periodVec γ₂) :
    (QuotientAddGroup.mk (periodVec γ₁) :
      (Fin (genus X) → ℂ) ⧸ (truePeriodLattice X).toAddSubgroup) =
      QuotientAddGroup.mk (periodVec γ₂)

periodVec_concat_of_smooth

Period vector is additive under concatenation of two smooth paths. Packages the 6 hypotheses of periodVec_concat for smooth paths sharing an endpoint (no zero-velocity needed — additivity holds for any smooth paths).

theorem periodVec_concat_of_smooth {P Q R : X} {g₁ g₂ : ℝ → X}
    (h₁ : IsSmoothPath P Q g₁) (h₂ : IsSmoothPath Q R g₂) :
    periodVec (Jacobians.concat g₁ g₂) = periodVec g₁ + periodVec g₂

zeroVelHop

A valid hop yields a smooth path with zero velocity at both endpoints (ChartBallPathSmooth is smoothstep-reparametrized).

theorem zeroVelHop {Q₀ Q : X} (h : HopValid Q₀ Q) :
    IsSmoothPath Q₀ Q (ChartBallPathSmooth Q₀ Q) ∧
    pathSpeed (ChartBallPathSmooth Q₀ Q) 0 = 0 ∧
    pathSpeed (ChartBallPathSmooth Q₀ Q) 1 = 0

exists_zeroVelPath_of_common_anchor

Common-anchor segment: if a point w validly hops to both u and v, then there is a zero-endpoint-velocity smooth path u → v (go u → w via the reversed hop, then w → v via the forward hop).

theorem exists_zeroVelPath_of_common_anchor {w u v : X}
    (hu : HopValid w u) (hv : HopValid w v) :
    ∃ γ, IsSmoothPath u v γ ∧ pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0

exists_smoothChain

Chart-ball cover: a chain of zero-velocity smooth-path hops from P to Q. Lebesgue-number cover of continuousPath P Q; each segment's endpoints are reached from a common Lebesgue anchor via exists_zeroVelPath_of_common_anchor.

theorem exists_smoothChain (P Q : X) :
    ∃ (n : ℕ) (a : ℕ → X), a 0 = P ∧ a n = Q ∧
      ∀ k, k < n → ∃ γ, IsSmoothPath (a k) (a (k+1)) γ ∧
        pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0

exists_zeroVel_smoothPath_aux

Generalized n-piece glue: a chain of zero-velocity smooth-path hops glues to a single zero-velocity smooth path, by induction on the chain length.

theorem exists_zeroVel_smoothPath_aux (a : ℕ → X) :
    ∀ n, (∀ k, k < n → ∃ γ, IsSmoothPath (a k) (a (k+1)) γ ∧
          pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0) →
      ∃ γ, IsSmoothPath (a 0) (a n) γ ∧ pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0

exists_zeroVel_smoothPath

A zero-endpoint-velocity smooth path exists between any two points (chart-ball cover glued by the n-piece induction).

theorem exists_zeroVel_smoothPath (P Q : X) :
    ∃ γ, IsSmoothPath P Q γ ∧ pathSpeed γ 0 = 0 ∧ pathSpeed γ 1 = 0

exists_smoothPath_family

theorem exists_smoothPath_family
    (X : Type*) [TopologicalSpace X] [T2Space X] [CompactSpace X]
    [ConnectedSpace X] [Nonempty X] [ChartedSpace ℂ X]
    [IsManifold 𝓘(ℂ) ω X] :
    ∃ sp : X → X → ℝ → X,
      (∀ P Q, IsSmoothPath P Q (sp P Q)) ∧
      (∀ P P₀ A,
        (QuotientAddGroup.mk (periodVec (sp P₀ A)) :
          (Fin (genus X) → ℂ) ⧸ (truePeriodLattice X).toAddSubgroup) =
        QuotientAddGroup.mk (periodVec (sp P A)) +
        QuotientAddGroup.mk (periodVec (sp P₀ P)))

smoothPath

The smooth path between P and Q, extracted via Classical.choice from exists_smoothPath_family.

noncomputable def smoothPath (P Q : X) : ℝ → X

isSmoothPath_smoothPath

The chosen smooth path satisfies IsSmoothPath.

theorem isSmoothPath_smoothPath (P Q : X) : IsSmoothPath P Q (smoothPath P Q)

smoothPath_zero

Boundary value: smoothPath P Q 0 = P.

@[simp] lemma smoothPath_zero (P Q : X) : smoothPath P Q 0 = P

smoothPath_one

Boundary value: smoothPath P Q 1 = Q.

@[simp] lemma smoothPath_one (P Q : X) : smoothPath P Q 1 = Q

periodVec_smoothPath_self_mem_lattice

The periodVec of the smooth path from P to P is in the period lattice (it's a closed smooth loop).

theorem periodVec_smoothPath_self_mem_lattice (P : X) :
    periodVec (smoothPath P P) ∈ truePeriodLattice X

smoothPath_basepoint_change

Basepoint change for smoothPath modulo the period lattice (classical, Forster §21). Extracted from the second conjunct of exists_smoothPath_family.

theorem smoothPath_basepoint_change (P P₀ A : X) :
    (QuotientAddGroup.mk (periodVec (smoothPath P₀ A)) :
      (Fin (genus X) → ℂ) ⧸ (truePeriodLattice X).toAddSubgroup) =
    QuotientAddGroup.mk (periodVec (smoothPath P A)) +
    QuotientAddGroup.mk (periodVec (smoothPath P₀ P))

pullbackForm_periodBasisForm_eq

Pullback of a Y-basis form via f, expressed in the X basis coordinates. Classical linear-algebra identity tying pullbackForm to ambientPsi. Pure manipulation of the ambientIso-based definitions; no analytic content.

theorem pullbackForm_periodBasisForm_eq (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (j : Fin (genus Y)) :
    pullbackForm f hf (periodBasisForm Y j) =
      ambientIso X (ambientPsi (gX := genus X) (gY := genus Y) f hf
        (Pi.basisFun ℂ (Fin (genus Y)) j))

IsClosedSmoothLoop.comp

Smooth loops compose with smooth maps. If γ : ℝ → X is a closed smooth loop and f : X → Y is smooth, then f ∘ γ is a closed smooth loop in Y. Sub-lemmas:

  1. Closedness: from γ 0 = γ 1.

  2. Continuity: from continuity of f and γ.

  3. Chart-pullback differentiability of chart_Y ∘ (f ∘ γ) at t: via the chart chain rule f_loc ∘ (chart_X ∘ γ) (proved inside pathSpeed_comp_eq_mfderiv).

  4. Integrability of each Y-basis form along f ∘ γ: via lineIntegral_pullback, the integrand equals (pullbackForm f hf (periodBasisForm Y j)).toFun (γ t) (pathSpeed γ t) (at least a.e.), which is a ℂ-linear combination of X-basis integrands — each integrable by hypothesis.

Remaining content: the sub-lemmas 3 and 4 require replaying the chart chain rule + linear-algebra arguments from elsewhere in the file. Bounded but ~100 lines.

theorem IsClosedSmoothLoop.comp (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    {γ : ℝ → X} (hγ : IsClosedSmoothLoop γ) :
    IsClosedSmoothLoop (f ∘ γ) where

periodVec_pushforward

Key identity: the period vector of the image loop equals ambientPhi applied to the period vector of the source loop.

With periodBasisForm Y j = ambientIso Y e_j^Y, the pullback pullbackForm f hf (periodBasisForm Y j) expanded in the X-basis has coefficients (ambientPsi f hf e_j^Y) i = M_ij. Then:

(ambientPhi f hf v)_j = ∑_i M_ij v_i

matches:

periodVec Y (f∘γ) j = ∫\_γ pullbackForm f hf (basis\_j^Y) = ∑\_i M\_ij (periodVec X γ)\_i.

Uses lineIntegral_pullback + linearity of lineIntegral via basis expansion. Requires path regularity (the hypotheses of IsClosedSmoothLoop).

theorem periodVec_pushforward
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) (γ : ℝ → X)
    (hγ_cont : Continuous γ)
    (hγ_diff : ∀ t ∈ Set.uIcc (0 : ℝ) 1,
      DifferentiableAt ℝ ((chartAt (H := ℂ) (γ t)).toFun ∘ γ) t)
    (hint_X : ∀ i : Fin (genus X), IntervalIntegrable
      (fun t => (periodBasisForm X i).toFun (γ t) (pathSpeed γ t))
        MeasureTheory.volume 0 1) :
    periodVec (f ∘ γ) =
      ambientPhi (gX := genus X) (gY := genus Y) f hf (periodVec γ)

ambientPhi_preserves_truePeriodLattice

theorem ambientPhi_preserves_truePeriodLattice
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f) :
    (truePeriodLattice X).toAddSubgroup ≤
      (truePeriodLattice Y).toAddSubgroup.comap
        (ambientPhi (gX := genus X) (gY := genus Y) f hf).toAddMonoidHom

criticalSet_ne_univ_of_nonconstant

Critical set of a non-constant map is not everything. (criticalSet f).Finite holds; X is infinite (a compact connected complex 1-manifold has an open chart into ℂ which contains an open ball, hence infinitely many points); so criticalSet f ≠ univ.

theorem criticalSet_ne_univ_of_nonconstant
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    criticalSet f ≠ Set.univ

finite_criticalSet_of_nonconstant

Critical set is finite (Forster §4 / isolated-zeros). For non-constant holomorphic f, criticalSet f is finite. Direct forward to criticalSet_finite_general.

theorem finite_criticalSet_of_nonconstant
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    (criticalSet f).Finite

finite_branchLocus_of_nonconstant

Branch locus is finite. Image of a finite set is finite.

theorem finite_branchLocus_of_nonconstant
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) :
    (branchLocus f).Finite

chartBridgePackage_of_nonconstant

Chart-bridge package at a single point. For non-constant analytic f : X → Y and any x : X, assembles the ChartBridgePackage f x consumed by the bridge criticalSet_iff_chart_pullback_deriv_zero. The chart pullback F := (chartAt ℂ (f x)) ∘ f ∘ (chartAt ℂ x).symm is analytic at z₀ := chartAt ℂ x x has finite local order k ≥ 1 of F - F z₀ (finiteness = F not eventually constant, via the clopenness/chart-overlap discharge applied to the non-constant f; positivity because (F - F z₀)(z₀) = 0), and the manifold ↔ chart-pullback non-injectivity transfer holds through the chart homeomorphism. This is the single-point specialization of criticalChartPullbackData_general's per-point work.

noncomputable def chartBridgePackage_of_nonconstant
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) (x : X) :
    Jacobians.Discharge.Manifold.ChartBridgePackage f x

exists_holo_localInverse_of_notMem_criticalSet

Local holomorphic section at a non-critical point. For non-constant holomorphic f and x ∉ criticalSet f, f admits a C^ω local section g near f x with g (f x) = x and f ∘ g = id on an open neighborhood. Composes the manifold inverse function theorem (exists_holo_localInverse) with the critical-set ↔ chart-derivative bridge. The input for the branched-cover trace's fiber sum.

theorem exists_holo_localInverse_of_notMem_criticalSet
    (f : X → Y) (hf : ContMDiff 𝓘(ℂ) 𝓘(ℂ) ω f)
    (hnonconst : ¬ ∃ y₀ : Y, ∀ x, f x = y₀) {x : X} (hxcrit : x ∉ criticalSet f) :
    ∃ (g : Y → X) (V : Set Y), IsOpen V ∧ f x ∈ V ∧ g (f x) = x ∧
      (∀ y ∈ V, f (g y) = y) ∧ ContMDiffOn 𝓘(ℂ) 𝓘(ℂ) ω g V