The →ₜ+ functoriality substrate, wrapped through the ULift shell (§9.4)

Unit: jacobian-construction. Wraps Torus.inducedHom/Torus.contMDiff_inducedHom (the abstract V ⧸ L → V' ⧸ L' substrate, §9.2–§9.3) through the ULift shell to produce a →ₜ+ map Jacobian X →ₜ+ Jacobian Y from a ℂ-linear map T between the ambient period spaces respecting the period subgroups.

Out of scope for this unit (flagged, not silently dropped, per design §9.4/R4): constructing the specific T for a given holomorphic f : X → Y (via pullback-of-forms), and the actual Jacobian.pushforward/Jacobian.pullback challenge definitions built from a real f. No blueprint unit currently owns "pullback of holomorphic 1-forms along a holomorphic map" — see this unit's final report for the flag to the orchestrator.

ULift as a →ₜ+ equivalence (generic transport toolkit)

def RS.uliftUpHom {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] : G →ₜ+ ULift.{u, u_1} G

ULift.up, bundled as a continuous additive homomorphism.

Equations

• RS.uliftUpHom = { toAddMonoidHom := AddEquiv.ulift.symm.toAddMonoidHom, continuous_toFun := ⋯ }

def RS.uliftDownHom {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] : ULift.{u, u_1} G →ₜ+ G

ULift.down, bundled as a continuous additive homomorphism.

Equations

• RS.uliftDownHom = { toAddMonoidHom := AddEquiv.ulift.toAddMonoidHom, continuous_toFun := ⋯ }

@[simp]

theorem RS.uliftUpHom_apply {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] (x : G) : uliftUpHom x = { down := x }

@[simp]

theorem RS.uliftDownHom_apply {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] (x : ULift.{u, u_1} G) : uliftDownHom x = x.down

noncomputable def Jacobian.inducedHom {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] {T : (Fin (genus X) → ℂ) →ₗ[ℂ] Fin (genus Y) → ℂ} (hT : RS.periodSubgroup X ≤ AddSubgroup.comap T.toAddMonoidHom (RS.periodSubgroup Y).topologicalClosure) : Jacobian X →ₜ+ Jacobian Y

A ℂ-linear map on the ambient period spaces, respecting the period subgroups (at the raw, undiscretized periodSubgroup level — the natural hypothesis to check for a map arising from a holomorphic f : X → Y, e.g. via naturality of periods under post-composition), induces the functoriality substrate Jacobian X →ₜ+ Jacobian Y. The closure-level hypothesis Torus.inducedHom needs is derived from this one via minimality of the topological closure (AddSubgroup.topologicalClosure_minimal), since (periodSubgroup Y).topologicalClosure is already closed and T is continuous (finite-dimensional).

Equations

• Jacobian.inducedHom hT = RS.uliftUpHom.comp ((RS.inducedHom (RS.periodSubgroup X).topologicalClosure (RS.periodSubgroup Y).topologicalClosure T ⋯).comp RS.uliftDownHom)

theorem Jacobian.contMDiff_inducedHom {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] {T : (Fin (genus X) → ℂ) →ₗ[ℂ] Fin (genus Y) → ℂ} (hT : RS.periodSubgroup X ≤ AddSubgroup.comap T.toAddMonoidHom (RS.periodSubgroup Y).topologicalClosure) [DiscreteTopology ↥(RS.periodSubgroup X).topologicalClosure] [DiscreteTopology ↥(RS.periodSubgroup Y).topologicalClosure] : ContMDiff (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) ⊤ ⇑(inducedHom hT)

The induced map on Jacobians is ω-smooth, given discreteness of both period-subgroup closures (needed for the manifold structure on either side, per Basic.lean's ledger).