LinearPencilSums.lean

theorem exists_universal_over_field
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c] (r : ℕ) :
    ∃ (Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of K))
      (U : RelEffCartierDiv c r y), U.IsUniversal

theorem lift_pullbackAlong
    {C S Y T T' : Scheme.{u}} {c : C ⟶ S} {r : ℕ}
    {y : Y ⟶ S} {U : RelEffCartierDiv c r y} (hU : U.IsUniversal)
    {g : T ⟶ S} (D : RelEffCartierDiv c r g)
    {g' : T' ⟶ S} (φ : T' ⟶ T) (hφ : φ ≫ g = g') :
    hU.lift (D.pullbackAlong φ hφ) = φ ≫ hU.lift D

theorem pencilDivisor_fibre_ideal
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (M : C.Modules)
    (hM : Scheme.Modules.IsInvertible M) (v : Fin 2 → Γ(M, ⊤))
    {r : ℕ} (P : RelEffCartierDiv c r lineMap)
    (hP : P.I = Scheme.Modules.zeroSchemeIdeal (pencilMorphism c M v)) (a : K) :
    (P.pullbackAlong (evaluate a) (evaluate_comp_lineMap a)).I.comap
        (inv (pullback.fst c (𝟙 (Spec (CommRingCat.of K))))) =
      Scheme.Modules.zeroSchemeIdeal (homOfGsec
        ((1 - c.appTop ((Scheme.ΓSpecIso (CommRingCat.of K)).inv a)) • v 0 +
          c.appTop ((Scheme.ΓSpecIso (CommRingCat.of K)).inv a) • v 1))

theorem pencilDivisor_endpoint_ideals
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (M : C.Modules)
    (hM : Scheme.Modules.IsInvertible M) (v : Fin 2 → Γ(M, ⊤))
    {r : ℕ} (P : RelEffCartierDiv c r lineMap)
    (hP : P.I = Scheme.Modules.zeroSchemeIdeal (pencilMorphism c M v)) :
    (P.pullbackAlong (evaluate (0 : K)) (evaluate_comp_lineMap 0)).I.comap
        (inv (pullback.fst c (𝟙 (Spec (CommRingCat.of K))))) =
      Scheme.Modules.zeroSchemeIdeal (homOfGsec (v 0)) ∧
    (P.pullbackAlong (evaluate (1 : K)) (evaluate_comp_lineMap 1)).I.comap
        (inv (pullback.fst c (𝟙 (Spec (CommRingCat.of K))))) =
      Scheme.Modules.zeroSchemeIdeal (homOfGsec (v 1))

theorem zeroSchemeIdeal_eq_of_dependent_sections
    {K : Type u} [Field K] {C : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) (M : C.Modules)
    (hM : Scheme.Modules.IsInvertible M) :
    let : Algebra K Γ(C, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ c.appTop).hom.toAlgebra
    let : Module K Γ(M, ⊤) := Module.compHom _ (algebraMap K Γ(C, ⊤))
    ∀ (v : Fin 2 → Γ(M, ⊤)), v 0 ≠ 0 → v 1 ≠ 0 →
      ¬ LinearIndependent K v →
      Scheme.Modules.zeroSchemeIdeal (homOfGsec (v 0)) =
        Scheme.Modules.zeroSchemeIdeal (homOfGsec (v 1)) := by
  intro algK modK v h0 h1 hv
  classical
  have hn : ¬ ∀ a : K, a • v 1 ≠ v 0 := by
    intro h
    exact hv (linearIndependent_fin2.mpr ⟨h1, h⟩)
  obtain ⟨a, ha⟩ := not_forall.mp hn
  have heq : a • v 1 = v 0 := not_not.mp ha
  have ha0 : a ≠ 0 := by
    intro hz
    rw [hz, zero_smul] at heq
    exact h0 heq.symm
  have hu : IsUnit (algebraMap K Γ(C, ⊤) a) :=
    (isUnit_iff_ne_zero.mpr ha0).map (algebraMap K Γ(C, ⊤))
  symm
  apply hM.zeroSchemeIdeal_eq_of_app_eq_smul (homOfGsec (v 1)) (homOfGsec (v 0))
    (algebraMap K Γ(C, ⊤) a) hu
  change gsec (homOfGsec (v 0)) = algebraMap K Γ(C, ⊤) a • gsec (homOfGsec (v 1))
  rw [gsec_homOfGsec, gsec_homOfGsec]
  exact heq.symm

theorem exists_pencilSum
    {K : Type u} [Field K] {C B : Scheme.{u}}
    (c : C ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
    (s : Spec (CommRingCat.of K) ⟶ C) (hs : s ≫ c = 𝟙 _)
    {b : B ⟶ Spec (CommRingCat.of K)} [Smooth b] [IsProper b]
    [GeometricallyIntegral b] (G : RelativeGroupLaw K b) (q : SchemeHomOver c b)
    (M : C.Modules) (hM : Scheme.Modules.IsInvertible M) :
    let : Algebra K Γ(C, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ c.appTop).hom.toAlgebra
    let : Module K Γ(M, ⊤) := Module.compHom _ (algebraMap K Γ(C, ⊤))
    ∀ (v : Fin 2 → Γ(M, ⊤)), LinearIndependent K v →
      ∃ (r : ℕ) (P : RelEffCartierDiv c r lineMap)
        (Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of K))
        (U : RelEffCartierDiv c r y) (hU : U.IsUniversal)
        (σ : finFibrePow c r ⟶ Y) (hσ : σ ≫ y = finFibrePow.toBase c r)
        (sum : SchemeHomOver y b),
        P.I = Scheme.Modules.zeroSchemeIdeal (pencilMorphism c M v) ∧
        U.I.comap (mapOnProdOver c σ hσ) = fibrePowOver.tautIdeal c r ∧
        σ ≫ sum.1 = (G.finiteSumMap c q r).1 ∧
        (∀ (a a' : K),
          hU.lift (P.pullbackAlong (evaluate a) (evaluate_comp_lineMap a)) ≫ sum.1 =
          hU.lift (P.pullbackAlong (evaluate a') (evaluate_comp_lineMap a')) ≫ sum.1) := by
  intro algK modK v hv
  have : GeometricallyConnected c := GeometricallyIrreducible.geometricallyConnected c
  have : GeometricallyConnected b := GeometricallyIrreducible.geometricallyConnected b
  obtain ⟨r, P, hP, -⟩ := exists_pencilDivisor c M hM v hv
  obtain ⟨Y, y, U, hU⟩ := exists_universal_over_field c r
  obtain ⟨σ, hσ, sum, hI, -, -, -, hsum, -⟩ :=
    exists_finiteSumMap_desc c s hs G q hU
  let hB : GoodReductionJacobian.AbelianSchemePropertyBundle K b :=
    ⟨inferInstance, inferInstance, b.isConnected_preimage_singleton, ⟨G⟩⟩
  have hbase : (hU.lift P ≫ sum.1) ≫ b =
      Spec.map (CommRingCat.ofHom (algebraMap K (Polynomial K))) := by
    rw [Category.assoc, sum.2, hU.lift_comp]
    rfl
  obtain ⟨a₀, -, hconst⟩ := GoodReductionJacobian.exists_eq_const_of_affineLine K hB
    (hU.lift P ≫ sum.1) hbase
  change hU.lift P ≫ sum.1 = lineMap ≫ a₀ at hconst
  refine ⟨r, P, Y, y, U, hU, σ, hσ, sum, hP, hI, hsum, ?_⟩
  intro a a'
  rw [lift_pullbackAlong, lift_pullbackAlong, Category.assoc, Category.assoc,
    hconst, ← Category.assoc, ← Category.assoc, evaluate_comp_lineMap,
    evaluate_comp_lineMap]