LinearPencilDivisor.lean

def pencilMorphism {K : Type u} [Field K] {X : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (M : X.Modules) (v : Fin 2 → Γ(M, ⊤)) :
    𝟙_ (pullback c lineMap).Modules ⟶
      (Scheme.Modules.pullback (pullback.fst c lineMap)).obj M

theorem pencilMorphism_apply_one {K : Type u} [Field K] {X : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (M : X.Modules) (v : Fin 2 → Γ(M, ⊤)) :
    (pencilMorphism c M v).app ⊤ (toUnitSection ⊤ 1) =
      pencilSection c M (v 0) (v 1)

theorem zeroSchemeIdeal_pencilMorphism_fibre
    {K : Type u} [Field K] {X : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) (M : X.Modules) (hM : IsInvertible M)
    (v : Fin 2 → Γ(M, ⊤)) (a : K) :
    (zeroSchemeIdeal (pencilMorphism c M v)).comap (fibre c a) =
      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 independent_pullback
    {K L : Type u} [Field K] [Field L] [Algebra K L]
    {X X' : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of K))
    [QuasiCompact c] [IsSeparated c]
    (c' : X' ⟶ Spec (CommRingCat.of L)) (p : X' ⟶ X)
    (hp : IsPullback p c' c (Spec.map (CommRingCat.ofHom (algebraMap K L))))
    (M : X.Modules) (hM : IsInvertible M) :
    let : Algebra K Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ c.appTop).hom.toAlgebra
    let : Module K Γ(M, ⊤) := Module.compHom _ (algebraMap K Γ(X, ⊤))
    let : Algebra L Γ(X', ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of L)).inv ≫ c'.appTop).hom.toAlgebra
    let : Module L Γ((Scheme.Modules.pullback p).obj M, ⊤) :=
      Module.compHom _ (algebraMap L Γ(X', ⊤))
    ∀ (v : Fin 2 → Γ(M, ⊤)), LinearIndependent K v →
      LinearIndependent L (M := Γ((Scheme.Modules.pullback p).obj M, ⊤))
        (fun i => (pullbackLocalSection p (v i) :
        Γ((Scheme.Modules.pullback p).obj M, ⊤))) := by
  intro algK modK algL modL v hv
  obtain ⟨β, hβ⟩ := hM.exists_tensorProduct_linearEquiv_sections_pullback_of_flat
    L c c' p hp M
  have h := (Module.Flat.linearIndependent_one_tmul (S := L) hv).map'
    β.toLinearMap (LinearMap.ker_eq_bot.mpr β.injective)
  have heq : (fun i => β ((1 : L) ⊗ₜ[K] v i)) =
      (fun i => pullbackLocalSection p (v i)) := by
    funext i
    exact hβ (v i)
  exact heq ▸ h

theorem combination_ne_zero
    {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    (v : Fin 2 → V) (hv : LinearIndependent K v) (a : K) :
    (1 - a) • v 0 + a • v 1 ≠ 0

theorem pencilSection_fibre_ne_zero
    {K : Type u} [Field K] {X : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) [QuasiCompact c] [IsSeparated c]
    (M : X.Modules) (hM : IsInvertible M) :
    let : Algebra K Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ c.appTop).hom.toAlgebra
    let : Module K Γ(M, ⊤) := Module.compHom _ (algebraMap K Γ(X, ⊤))
    ∀ (v : Fin 2 → Γ(M, ⊤)), LinearIndependent K v →
      ∀ (k : Type u) [Field k]
        (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of (Polynomial K))),
      pullbackLocalSection (mapOnProdOver c x rfl)
        (pencilSection c M (v 0) (v 1)) ≠ 0 := by
  intro algK modK v hv k _ x
  let ρ : CommRingCat.of K ⟶ CommRingCat.of k := Spec.preimage (x ≫ lineMap)
  let : Algebra K k := ρ.hom.toAlgebra
  have hρ : Spec.map (CommRingCat.ofHom (algebraMap K k)) = x ≫ lineMap :=
    Spec.map_preimage (x ≫ lineMap)
  let Y := pullback c (x ≫ lineMap)
  let c' : Y ⟶ Spec (CommRingCat.of k) := pullback.snd c (x ≫ lineMap)
  let F : Y ⟶ pullback c lineMap := mapOnProdOver c x rfl
  let p : Y ⟶ X := F ≫ pullback.fst c lineMap
  have hp : IsPullback p c' c (Spec.map (CommRingCat.ofHom (algebraMap K k))) := by
    change IsPullback (mapOnProdOver c x rfl ≫ pullback.fst c lineMap)
      (pullback.snd c (x ≫ lineMap)) c _
    rw [mapOnProdOver_fst, hρ]
    exact IsPullback.of_hasPullback c (x ≫ lineMap)
  let algk : Algebra k Γ(Y, ⊤) :=
    ((Scheme.ΓSpecIso (CommRingCat.of k)).inv ≫ c'.appTop).hom.toAlgebra
  let V : Y.Modules := (Scheme.Modules.pullback p).obj M
  let modk : Module k Γ(V, ⊤) := Module.compHom _ (algebraMap k Γ(Y, ⊤))
  let w : Fin 2 → Γ(V, ⊤) := fun i => pullbackLocalSection p (v i)
  have hw : LinearIndependent k w := independent_pullback c c' p hp M hM v hv
  let a : k := (Scheme.ΓSpecIso (CommRingCat.of k)).hom
    (x.appTop ((Scheme.ΓSpecIso (CommRingCat.of (Polynomial K))).inv Polynomial.X))
  have hparameter : F.appTop (parameter c) = algebraMap k Γ(Y, ⊤) a := by
    change ((pullback.snd c lineMap).appTop ≫ F.appTop)
      ((Scheme.ΓSpecIso (CommRingCat.of (Polynomial K))).inv Polynomial.X) =
      c'.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv a)
    rw [← Scheme.Hom.comp_appTop]
    change (mapOnProdOver c x rfl ≫ pullback.snd c lineMap).appTop _ = _
    rw [mapOnProdOver_snd, Scheme.Hom.comp_appTop]
    change c'.appTop _ = c'.appTop ((Scheme.ΓSpecIso (CommRingCat.of k)).inv a)
    exact congrArg c'.appTop (Iso.inv_hom_id_apply _ _).symm
  have hcomb := combination_ne_zero w hw a
  change (algebraMap k Γ(Y, ⊤) (1 - a)) • w 0 +
    (algebraMap k Γ(Y, ⊤) a) • w 1 ≠ 0 at hcomb
  rw [map_sub, map_one, ← hparameter] at hcomb
  intro hz
  have hcalc := pencilSection_pullback c F M (v 0) (v 1)
  change ((pullbackComp F (pullback.fst c lineMap)).hom.app M).app ⊤
    (pullbackLocalSection F (pencilSection c M (v 0) (v 1))) =
      (1 - F.appTop (parameter c)) • w 0 + F.appTop (parameter c) • w 1 at hcalc
  rw [hz] at hcalc
  exact hcomb (hcalc.symm.trans
    (((pullbackComp F (pullback.fst c lineMap)).hom.app M).app ⊤).hom.map_zero)

theorem exists_divisor_of_fibre_divisors
    {C S T : Scheme.{u}} {c : C ⟶ S} [IsProper c]
    [SmoothOfRelativeDimension 1 c] (g : T ⟶ S)
    [IsLocallyNoetherian T] [ConnectedSpace T]
    {M : (pullback c g).Modules} (hM : IsInvertible M)
    (s : 𝟙_ (pullback c g).Modules ⟶ M)
    (hfib : ∀ (k : Type u) [Field k] [IsAlgClosed k]
      (x : Spec (CommRingCat.of k) ⟶ T),
      ∃ (r : ℕ) (D : RelEffCartierDiv c r (x ≫ g)),
        D.I = (zeroSchemeIdeal s).comap (mapOnProdOver c x rfl)) :
    ∃ (r : ℕ) (D : RelEffCartierDiv c r g),
      D.I = zeroSchemeIdeal s ∧
      ∃ e : M ≅ D.lineBundle, s ≫ e.hom = D.I.invModuleSection

theorem exists_pencilDivisor
    {K : Type u} [Field K] {X : Scheme.{u}}
    (c : X ⟶ Spec (CommRingCat.of K)) [IsProper c]
    [SmoothOfRelativeDimension 1 c] [GeometricallyIrreducible c]
    (M : X.Modules) (hM : IsInvertible M) :
    let : Algebra K Γ(X, ⊤) :=
      ((Scheme.ΓSpecIso (CommRingCat.of K)).inv ≫ c.appTop).hom.toAlgebra
    let : Module K Γ(M, ⊤) := Module.compHom _ (algebraMap K Γ(X, ⊤))
    ∀ (v : Fin 2 → Γ(M, ⊤)), LinearIndependent K v →
      ∃ (r : ℕ) (D : RelEffCartierDiv c r lineMap),
        D.I = zeroSchemeIdeal (pencilMorphism c M v) ∧
        ∃ e : (Scheme.Modules.pullback (pullback.fst c lineMap)).obj M ≅ D.lineBundle,
          pencilMorphism c M v ≫ e.hom = D.I.invModuleSection := by
  intro algK modK v hv
  have hN : IsInvertible ((Scheme.Modules.pullback (pullback.fst c lineMap)).obj M) :=
    hM.pullback (pullback.fst c lineMap)
  apply exists_divisor_of_fibre_divisors lineMap hN (pencilMorphism c M v)
  intro k _ _ x
  let F : pullback c (x ≫ lineMap) ⟶ pullback c lineMap := mapOnProdOver c x rfl
  have hnonzero : pullbackSection F (pencilMorphism c M v) ≠ 0 := by
    intro hz
    have h := congrArg gsec hz
    rw [gsec_pullbackSection, gsec_def, pencilMorphism_apply_one] at h
    apply pencilSection_fibre_ne_zero c M hM v hv k x
    exact h.trans (show gsec (0 : 𝟙_ (pullback c (x ≫ lineMap)).Modules ⟶
      (Scheme.Modules.pullback F).obj
        ((Scheme.Modules.pullback (pullback.fst c lineMap)).obj M)) = 0 from rfl)
  obtain ⟨r, D, hD⟩ := RelEffCartierDiv.exists_I_eq_zeroSchemeIdeal_of_ne_zero_of_isProper
    (x ≫ lineMap) (hN.pullback F) (pullbackSection F (pencilMorphism c M v)) hnonzero
  refine ⟨r, D, ?_⟩
  exact hD.trans (hN.comap_zeroSchemeIdeal F (pencilMorphism c M v)).symm