Jacobian of a compact Riemann surface (Buzzard challenge)

jacobian_challenge_diffgeo

Submitter: Kevin Buzzard.

Notes: Unavailable.

Source: https://leanprover.zulipchat.com/#narrow/stream/583336-Autoformalization/topic/Jacobian%20challenge

Informal solution: Construct J(X) as H^0(X, Omega^1)* / H_1(X, Z), the period lattice quotient; the Abel-Jacobi map sends a point to the linear functional 'integrate from a fixed basepoint to here'. Functoriality and the projection formula come from pushforward and pullback of differential forms.

def declaration uses `sorry`genus (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : ℕ := sorry

theorem declaration uses `sorry`genus_eq_zero_iff_homeo :
    genus X = 0 ↔ Nonempty (X ≃ₜ (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1)) :=
  sorry

def declaration uses `sorry`Jacobian (X : Type u) [TopologicalSpace X] [T2Space X] [CompactSpace X] [ConnectedSpace X]
    [Nonempty X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ω X] : Type u := sorry

instance declaration uses `sorry`instAddCommGroup : AddCommGroup (Jacobian X) := sorry

instance declaration uses `sorry`instTopologicalSpace : TopologicalSpace (Jacobian X) := sorry

instance declaration uses `sorry`instT2Space : T2Space (Jacobian X) := sorry

instance declaration uses `sorry`instCompactSpace : CompactSpace (Jacobian X) := sorry

instance declaration uses `sorry`instChartedSpace : ChartedSpace (Fin (genus X) → ℂ) (Jacobian X) := sorry

instance declaration uses `sorry`instIsManifold :
    IsManifold (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorry

instance declaration uses `sorry`instLieAddGroup :
    LieAddGroup (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (Jacobian X) := sorry

def declaration uses `sorry`ofCurve (P : X) : X → Jacobian X := sorry

theorem declaration uses `sorry`ofCurve_contMDiff (P : X) :
    ContMDiff (modelWithCornersSelf ℂ ℂ)
      (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (ofCurve P) := sorry

theorem declaration uses `sorry`ofCurve_self (P : X) : ofCurve P P = 0 := sorry

theorem declaration uses `sorry`ofCurve_inj (P : X) (h : 0 < genus X) : Function.Injective (ofCurve P) := sorry

def declaration uses `sorry`pushforward (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    Jacobian X →ₜ+ Jacobian Y := sorry

theorem declaration uses `sorry`pushforward_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (genus X) → ℂ))
      (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ)) ω (pushforward f hf) := sorry

theorem declaration uses `sorry`pushforward_id_apply (P : Jacobian X) :
    pushforward id contMDiff_id P = P := sorry

theorem declaration uses `sorry`pushforward_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
    (P : Jacobian X) :
    pushforward (g ∘ f) (hg.comp hf) P = pushforward g hg (pushforward f hf P) :=
  sorry

def declaration uses `sorry`pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    Jacobian Y →ₜ+ Jacobian X := sorry

theorem declaration uses `sorry`pullback_contMDiff (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) :
    ContMDiff (modelWithCornersSelf ℂ (Fin (genus Y) → ℂ))
      (modelWithCornersSelf ℂ (Fin (genus X) → ℂ)) ω (pullback f hf) := sorry

theorem declaration uses `sorry`pullback_id_apply (P : Jacobian X) :
    pullback id contMDiff_id P = P := sorry

theorem declaration uses `sorry`pullback_comp_apply (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (g : Y → Z) (hg : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω g)
    (P : Jacobian Z) :
    pullback (g.comp f) (hg.comp hf) P = pullback f hf (pullback g hg P) := sorry

def declaration uses `sorry`degree (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f) : ℕ :=
  sorry -- 0 for constant case

theorem declaration uses `sorry`pushforward_pullback (f : X → Y)
    (hf : ContMDiff (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ω f)
    (P : Jacobian Y) :
    pushforward f hf (pullback f hf P) = (degree f hf) • P := sorry

Solved by

Not yet solved.