The pullback map on Jacobians (jacobian-functoriality §8, pullback half)

Unit: jacobian-functoriality. RS.pullbackT (the period-space linear map induced by Form1.trace's dualMap), RS.pullbackT_periodVector (its action on period vectors), RS.periodSubgroup_le_comap_pullbackT (hT for the pullback direction — exact membership via RS.periodVector_traceForm_mem, after conjugating the loop to a regular basepoint (RS.period_conj) and perturbing it off the finite branch locus (RS.Loop.exists_homotopic_avoiding + RS.period_congr_homotopic)), and the assembly Jacobian.pullback via Jacobian.inducedHom (same-universe convention, see PeriodMaps.lean's universe warning).

noncomputable def RS.pullbackT {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : (Fin (genus Y) → ℂ) →ₗ[ℂ] Fin (genus X) → ℂ

The induced ℂ-linear map on period spaces for the pullback direction, from Form1.trace f hf's dualMap (covariant trace transposes to the contravariant direction: Dual (Form1 Y) →ₗ Dual (Form1 X), i.e. period space of Y to period space of X).

Equations

• RS.pullbackT f hf = ↑(RS.periodCoordEquiv X) ∘ₗ (RS.Form1.trace f hf).dualMap ∘ₗ ↑(RS.periodCoordEquiv Y).symm

theorem RS.pullbackT_periodVector {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) {y : Y} (γ : Path y y) : (pullbackT f hf) (periodVector (basis Y) γ) = fun (i : Fin (genus X)) => pathIntegral γ ((Form1.trace f hf) ((basis X) i))

The pullback period map computed at a based loop.

theorem RS.periodSubgroup_le_comap_pullbackT {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u_2} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ConnectedSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : periodSubgroup Y ≤ AddSubgroup.comap (pullbackT f hf).toAddMonoidHom (periodSubgroup X).topologicalClosure

hT for the pullback direction (§8.3): exact membership, via basepoint conjugation + off-branch perturbation + the loop decomposition of the trace integral.

noncomputable def RS.Jacobian.pullback {X' : Type u} [TopologicalSpace X'] [T2Space X'] [CompactSpace X'] [ConnectedSpace X'] [ChartedSpace ℂ X'] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X'] {Y' : Type u} [TopologicalSpace Y'] [T2Space Y'] [CompactSpace Y'] [ConnectedSpace Y'] [ChartedSpace ℂ Y'] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y'] (f : X' → Y') (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) : Jacobian Y' →ₜ+ Jacobian X'

Jacobian.pullback (§8.4): the pullback map between Jacobians associated to a holomorphic map of the underlying curves. Equal to the zero map if the map on curves is constant (Form1.trace's convention).

Equations

• RS.Jacobian.pullback f hf = Jacobian.inducedHom ⋯