Period-space plumbing and the pushforward map (jacobian-functoriality §8, pushforward half)

Unit: jacobian-functoriality. RS.periodCoordEquiv (the dualMap/Basis.dualBasis.equivFun coordinatization of the ambient period space, spiked in scratch_jfun.lean), pushforwardT (the induced ℂ-linear map on period spaces from Form1.pullback), and periodSubgroup_le_comap_pushforwardT (hT for the pushforward direction — exact membership, no closure/density needed, via pathIntegral_pullback + basepoint-flexible periodVector_mem_periodSubgroup). Assembles Jacobian.pushforward via Jacobian.inducedHom.

Scope note: only the pushforward direction is built in this unit (see the root file's LEDGER for the pullback-direction gap: Form1.trace's branch-point analyticity and the trace–path-integral relation are not completed, so pullbackT/Jacobian.pullback/ pushforward_pullback cannot be assembled here).

noncomputable def RS.periodCoordEquiv (X : Type u_1) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : Module.Dual ℂ (Form1 X) ≃ₗ[ℂ] Fin (genus X) → ℂ

The dualMap/Basis.dualBasis.equivFun coordinatization of the ambient period space: a period vector periodVector (basis X) γ is exactly pathIntegralₗ γ read in (basis X)'s dual-basis coordinates (§8.1, spiked in scratch_jfun.lean).

Equations

• RS.periodCoordEquiv X = (RS.basis X).dualBasis.equivFun

theorem RS.periodCoordEquiv_apply (X : Type u_1) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (φ : Module.Dual ℂ (Form1 X)) (i : Fin (genus X)) : (periodCoordEquiv X) φ i = φ ((basis X) i)

noncomputable def RS.pushforwardT {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace 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 X) → ℂ) →ₗ[ℂ] Fin (genus Y) → ℂ

The induced ℂ-linear map on period spaces, from Form1.pullback f hf's dualMap (contravariant: Form1 Y →ₗ Form1 X transposes to Dual(Form1 X) →ₗ Dual(Form1 Y), exactly the pushforward direction).

Equations

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

theorem RS.pushforwardT_periodVector {X : Type u_1} [TopologicalSpace X] [T2Space X] [CompactSpace 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) {x : X} (γ : Path x x) : (pushforwardT f hf) (periodVector (basis X) γ) = periodVector (basis Y) (γ.map ⋯)

The pushforward map on period vectors, computed at a based loop: pushforwardT sends the period vector of γ to the period vector of its image loop γ.map hf.continuous (pathIntegral_pullback's naturality, transported through the coordinatization).

theorem RS.periodSubgroup_le_comap_pushforwardT {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 X ≤ AddSubgroup.comap (pushforwardT f hf).toAddMonoidHom (periodSubgroup Y).topologicalClosure

hT for the pushforward direction (§8.2 — exact containment, no closure/density needed).

noncomputable def RS.Jacobian.pushforward {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 X' →ₜ+ Jacobian Y'

Jacobian.pushforward (§8.4): the pushforward map between Jacobians associated to a holomorphic map of the underlying curves.

Equations

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