Exists_iso_fibre_pullback_fibreModule_tensor_sectionTwist_iso.lean

theorem fibreIdE9_comap_pow {X Y : Scheme.{u}} (I : Y.IdealSheafData) (f : X ⟶ Y) (n : ℕ) :
    (I ^ n).comap f = (I.comap f) ^ n

theorem fibreIdE9_isInvertible_sectionIdeal (c : C ⟶ Spec (CommRingCat.of k))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c) (t : T ⟶ Spec (CommRingCat.of k)) :
    (RelPicard.sectionIdeal c ε t).IsInvertible

theorem fibreIdE9_sectionIdeal_comap_section (c : C ⟶ Spec (CommRingCat.of k)) [IsSeparated c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c) (t : T ⟶ Spec (CommRingCat.of k))
    (x : Spec (CommRingCat.of k) ⟶ T) (hx : x ≫ t = 𝟙 _)
    (ix : C ⟶ pullback c t) (hix_fst : ix ≫ pullback.fst c t = 𝟙 C)
    (hix_snd : ix ≫ pullback.snd c t = c ≫ x) :
    (RelPicard.sectionIdeal c ε t).comap ix = ε.1.ker

theorem fibreIdE9_nonempty_pullback_sectionTwist_iso (c : C ⟶ Spec (CommRingCat.of k))
    [IsSeparated c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c) (t : T ⟶ Spec (CommRingCat.of k))
    (x : Spec (CommRingCat.of k) ⟶ T) (hx : x ≫ t = 𝟙 _)
    (ix : C ⟶ pullback c t) (hix_fst : ix ≫ pullback.fst c t = 𝟙 C)
    (hix_snd : ix ≫ pullback.snd c t = c ≫ x) (d : ℕ) :
    Nonempty ((Scheme.Modules.pullback ix).obj (RelPicard.sectionTwist c ε t d) ≅
      ((ε.1.ker) ^ d).invModule)

theorem
    _root_.AlgebraicGeometry.RelPicard.exists_iso_fibre_pullback_fibreModule_tensor_sectionTwist_iso
    {k : Type u} [Field k] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of k))
    [IsProper c] [SmoothOfRelativeDimension 1 c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) c) (t : T ⟶ Spec (CommRingCat.of k))
    (x : Spec (CommRingCat.of k) ⟶ T) (hx : x ≫ t = 𝟙 _) :
    ∃ φ : C ≅ pullback (pullback.snd c t) x,
      φ.hom ≫ fibreAt c t x = c ∧
      φ.hom ≫ pullback.fst (pullback.snd c t) x =
        pullback.lift (𝟙 C) (c ≫ x) (by rw [Category.id_comp, Category.assoc, hx,
          Category.comp_id]) ∧
      ∀ (F : (pullback c t).Modules) (d : ℕ),
        Nonempty ((Scheme.Modules.pullback φ.hom).obj (fibreModule c t x (F ⊗ sectionTwist c ε t
          d)) ≅
          (Scheme.Modules.pullback
              (pullback.lift (𝟙 C) (c ≫ x) (by rw [Category.id_comp, Category.assoc, hx,
                Category.comp_id]))).obj F ⊗
            ((ε.1.ker) ^ d).invModule) := by
  have hix : 𝟙 C ≫ c = (c ≫ x) ≫ t := by rw [Category.id_comp, Category.assoc, hx, Category.comp_id]
  let ix : C ⟶ pullback c t := pullback.lift (𝟙 C) (c ≫ x) hix
  have hix_fst : ix ≫ pullback.fst c t = 𝟙 C := pullback.lift_fst _ _ _
  have hix_snd : ix ≫ pullback.snd c t = c ≫ x := pullback.lift_snd _ _ _
  have hA : pullback.fst (pullback.snd c t) x ≫ pullback.fst c t ≫ c =
      pullback.snd (pullback.snd c t) x := by
    rw [pullback.condition (f := c) (g := t), ← Category.assoc,
      pullback.condition (f := pullback.snd c t) (g := x), Category.assoc, hx, Category.comp_id]
  let φhom : C ⟶ pullback (pullback.snd c t) x := pullback.lift ix c (by rw [hix_snd])
  have hφ_fst : φhom ≫ pullback.fst (pullback.snd c t) x = ix := pullback.lift_fst _ _ _
  have hφ_snd : φhom ≫ pullback.snd (pullback.snd c t) x = c := pullback.lift_snd _ _ _
  let φ : C ≅ pullback (pullback.snd c t) x :=
    { hom := φhom
      inv := pullback.fst (pullback.snd c t) x ≫ pullback.fst c t
      hom_inv_id := by rw [← Category.assoc, hφ_fst, hix_fst]
      inv_hom_id := by
        apply pullback.hom_ext
        · rw [Category.assoc, Category.assoc, hφ_fst, Category.id_comp]
          apply pullback.hom_ext
          · rw [Category.assoc, Category.assoc, hix_fst, Category.comp_id]
          · rw [Category.assoc, Category.assoc, hix_snd,
              pullback.condition (f := pullback.snd c t) (g := x), ← hA]
            simp only [Category.assoc]
        · rw [Category.assoc, Category.assoc, hφ_snd, Category.id_comp, hA] }
  refine ⟨φ, ?_, hφ_fst, fun F d => ?_⟩
  · change φhom ≫ pullback.snd (pullback.snd c t) x = c
    exact hφ_snd
  · obtain ⟨e4⟩ :=
      AlgebraicGeometry.fibreIdE9_nonempty_pullback_sectionTwist_iso c ε t x hx ix hix_fst hix_snd d
    exact ⟨(Scheme.Modules.pullbackComp φhom (pullback.fst (pullback.snd c t) x)).app
        (F ⊗ sectionTwist c ε t d) ≪≫
      (Scheme.Modules.pullbackCongr hφ_fst).app (F ⊗ sectionTwist c ε t d) ≪≫
      Scheme.Modules.pullbackTensorObjIso ix F (sectionTwist c ε t d) ≪≫
      whiskerLeftIso ((Scheme.Modules.pullback ix).obj F) e4⟩