Jacobians — the assembled challenge API

Final assembly of Kevin Buzzard's AI challenge docs/Jacobian_challenge.lean (v0.4): every placeholder of the gist is discharged by the development under Jacobian/, with zero axioms beyond propext/Classical.choice/Quot.sound.

Most gist declarations already live at their gist names (root level / Jacobian namespace) inside the units that built them; this file adds ONLY what was still missing — the root-level Jacobian.pushforward/Jacobian.pullback functorial API (the built maps live at RS.Jacobian.*) — and closes with a self-auditing GistCheck section containing one witness per gist item.

Item-by-item map (gist declaration → providing declaration)

• genus → genus (Jacobian/Forms/Genus.lean, root, gist signature verbatim).
• genus_eq_zero_iff_homeo → genus_eq_zero_iff_homeo (Jacobian/GenusSphereHeadline/Basic.lean, root, gist statement verbatim).
• Jacobian → Jacobian (Jacobian/JacobianConstruction/Basic.lean, root, Type u → Type u as the gist demands; an abbrev — ULift shell around the honest Type 0 quotient).
• instance : AddCommGroup/TopologicalSpace/T2Space (Jacobian X) → unconditional instances in Jacobian/JacobianConstruction/Basic.lean.
• instance : CompactSpace/ChartedSpace/IsManifold/LieAddGroup … (Jacobian X) → the gated instances of Jacobian/JacobianConstruction/Basic.lean, whose gates (DiscreteTopology (RS.periodSubgroup X).topologicalClosure, IsZLattice …) are global instances since Jacobian/CechCount/Final.lean; all fire by inferInstance (see GistCheck).
• Jacobian.ofCurve → Jacobian.ofCurve; Jacobian.ofCurve_self → Jacobian.ofCurve_self (Jacobian/JacobianConstruction/OfCurve.lean, gist names/signatures).
• Jacobian.ofCurve_contMDiff → Jacobian.ofCurve_contMDiff (same file; carries one extra instance-implicit [DiscreteTopology (RS.periodSubgroup X).topologicalClosure], globally discharged — every gist-shaped use elaborates verbatim).
• Jacobian.ofCurve_inj → Jacobian.ofCurve_inj (Jacobian/CechCount/Final.lean), the exact gist name and signature (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P), hypothesis-free (the development-time gated variant lives on as Jacobian.ofCurve_inj_of_upgrade in Jacobian/Abel/OfCurveInj.lean).
• Jacobian.pushforward → defined below (wrapper of RS.Jacobian.pushforward).
• Jacobian.pushforward_contMDiff → below (from RS.Jacobian.pushforward_contMDiff; its discreteness gates are global instances, so the gist statement holds unconditionally).
• Jacobian.pushforward_id_apply / Jacobian.pushforward_comp_apply → below.
• Jacobian.pullback → below (wrapper of RS.Jacobian.pullback).
• Jacobian.pullback_contMDiff, Jacobian.pullback_id_apply, Jacobian.pullback_comp_apply → below.
• ContMDiff.degree → ContMDiff.degree (Jacobian/ProperDegree/ChallengeDegree.lean, root, gist signature verbatim, f explicit).
• Jacobian.pushforward_pullback → below (from RS.Jacobian.pushforward_pullback).

Universe convention (the one deviation from the gist's variable blocks)

The gist declares {X Y Z : Type*} — three independent universes. Jacobian X is the ULift shell around a Type 0 quotient, and the underlying Jacobian.inducedHom substrate demands both surfaces in ONE Type u: instantiating any Jacobian X-to-Jacobian Y declaration at distinct universes does not fail cleanly but sends the elaborator into a ULift/quotient defeq grind (deterministic heartbeat timeout — documented in Jacobian/JacFunctorial.lean's LEDGER and re-verified during this assembly). The functorial declarations below therefore state their surfaces in a single shared universe u. This only restricts universes; every statement is otherwise the gist's, and the (overwhelmingly common) same-universe uses — including everything in Type 0 — elaborate verbatim.

noncomputable def 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

The pushforward map between Jacobians associated to a map of the underlying curves.

Equations

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

theorem Jacobian.pushforward_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) : ContMDiff (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) ⊤ ⇑(pushforward f hf)

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

noncomputable def 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

Pullback map between Jacobians associated to a map of the underlying curves. Equal to the zero map if the map on curves is constant.

Equations

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

theorem 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) : ContMDiff (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ⊤ ⇑(pullback f hf)

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

theorem 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

GistCheck — self-audit

One witness per declaration of docs/Jacobian_challenge.lean, each stated in the gist's own shape and discharged by the providing declaration. Single-surface items use the gist's Type* variables verbatim; the multi-surface functorial items share one universe (see the module docstring).