Challenge-signature functoriality laws and the projection formula (jacobian-functoriality §9)

Unit: jacobian-functoriality. The remaining challenge exports (docs/Jacobian_challenge.lean:104-153):

• Jacobian.pullback_contMDiff (free from Jacobian.contMDiff_inducedHom, inheriting the [DiscreteTopology (periodSubgroup _).topologicalClosure] gate transparently).
• Jacobian.pushforward_id_apply / Jacobian.pushforward_comp_apply and Jacobian.pullback_id_apply / Jacobian.pullback_comp_apply — via representative-level computation (RS.Jacobian.inducedHom_apply_up_mk) and the Form1-level laws (Form1.pullback_id/comp, Form1.trace_id/comp) transported through dualMap.
• Jacobian.pushforward_pullback — the projection formula, from Form1.trace_pullback (Tr_f ∘ f^* = deg f).

Same-universe convention throughout (see PeriodMaps.lean's universe warning).

pullback_contMDiff

theorem RS.Jacobian.pullback_contMDiff {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) [DiscreteTopology ↥(periodSubgroup X).topologicalClosure] [DiscreteTopology ↥(periodSubgroup Y).topologicalClosure] : ContMDiff (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ⊤ ⇑(pullback f hf)

The pullback map on Jacobians is holomorphic (§9.1 — free from Jacobian.contMDiff_inducedHom, same inherited gate as pushforward_contMDiff).

Representative-level computation

theorem RS.Jacobian.exists_rep {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : Jacobian X) : ∃ (v : Fin (genus X) → ℂ), P = { down := ↑v }

Every point of the Jacobian is (the lift of) a residue class of an ambient vector.

theorem RS.Jacobian.inducedHom_apply_up_mk {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 : periodSubgroup X ≤ AddSubgroup.comap T.toAddMonoidHom (periodSubgroup Y).topologicalClosure) (v : Fin (genus X) → ℂ) : (Jacobian.inducedHom hT) { down := ↑v } = { down := ↑(T v) }

Jacobian.inducedHom on representatives.

T-level functoriality

theorem RS.pushforwardT_id {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : pushforwardT id ⋯ = LinearMap.id

theorem RS.pullbackT_id {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] : pullbackT id ⋯ = LinearMap.id

theorem RS.pushforwardT_comp {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {Y : Type u} [TopologicalSpace Y] [T2Space Y] [CompactSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {Z : Type u} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) : pushforwardT (g ∘ f) ⋯ = pushforwardT g hg ∘ₗ pushforwardT f hf

theorem RS.pullbackT_comp {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] {Z : Type u} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) : pullbackT (g ∘ f) ⋯ = pullbackT f hf ∘ₗ pullbackT g hg

theorem RS.pushforwardT_pullbackT_apply {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) (v : Fin (genus Y) → ℂ) : (pushforwardT f hf) ((pullbackT f hf) v) = ↑(ContMDiff.degree f hf) • v

The composed period map of pullback then pushforward is multiplication by the degree (the T-level projection formula, from Form1.trace_pullback).

The challenge laws

theorem RS.Jacobian.pushforward_id_apply {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : Jacobian X) : (pushforward id ⋯) P = P

theorem RS.Jacobian.pullback_id_apply {X : Type u} [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (P : Jacobian X) : (pullback id ⋯) P = P

theorem RS.Jacobian.pushforward_comp_apply {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] {Z : Type u} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z] [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) (P : Jacobian X) : (pushforward (g ∘ f) ⋯) P = (pushforward g hg) ((pushforward f hf) P)

theorem RS.Jacobian.pullback_comp_apply {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] {Z : Type u} [TopologicalSpace Z] [T2Space Z] [CompactSpace Z] [ConnectedSpace Z] [ChartedSpace ℂ Z] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Z] (f : X → Y) (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ f) (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g) (P : Jacobian Z) : (pullback (g ∘ f) ⋯) P = (pullback f hf) ((pullback g hg) P)

theorem RS.Jacobian.pushforward_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) (P : Jacobian Y) : (pushforward f hf) ((pullback f hf) P) = ContMDiff.degree f hf • P

The projection formula on Jacobians: pushforward f ∘ pullback f = deg f (docs/Jacobian_challenge.lean:151-152).