exists_openCharts_relSubPicPresheaf_algEquivZeroCut_of_relEffCartierDiv_supportedIn_of_fibrewise_zeroScheme.lean

theorem exists_openCharts_of_relEffCartierDiv_supportedIn_of_fibrewise_zeroScheme
    (R : Type u) [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of
      R))
    [IsProper c] [Flat c] (𝒱 : C.TwoAffineOpenCover)
    (hH0 : ∀ (A : Type u) [CommRing A] [Algebra R A],
      let _ : Algebra A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A), ⊤) :=
        Scheme.TwoAffineOpenCover.algebraOfHom
        (Limits.pullback.snd c (Scheme.TwoAffineOpenCover.specMap R A)) ⊤
      Function.Bijective (algebraMap A Γ(Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R A),
        ⊤)))
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
    (hlfp : AffineLimit.IsLFPSurj (relSubPicPresheaf c ε (algEquivZeroCut c ε)))
    (U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
    (hεU : Set.range ε.1 ⊆ (U : Set C))
    {ι : Type u} [Finite ι] (g e r : ℕ) (hr : g + e = r)
    (hg : ∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ Spec
      (CommRingCat.of R))
      (𝒲 : (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).TwoAffineOpenCover),
      Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
        (𝟙_ (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).Modules)).H1 = g)
    (Y : Scheme.{u}) (y : Y ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType y] [CompactSpace Y]
    (Duniv : RelEffCartierDiv c g y) (hDunivU : Duniv.SupportedIn U)
    (huniv : ∀ ⦃T : Scheme.{u}⦄ (g' : T ⟶ Spec (CommRingCat.of R)) (D : RelEffCartierDiv c g g'),
      D.SupportedIn U →
        ∃! φ : {φ : T ⟶ Y // φ ≫ y = g'}, PullsBackOver Duniv φ.1 φ.2 D)
    (hsect : ∀ ⦃V : Scheme.{u}⦄ (u : V ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType u] (M :
      (pullback c u).Modules),
      Scheme.Modules.IsInvertible M →
      (∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ V) (𝒲 : (pullback (pullback.snd c u)
        s).TwoAffineOpenCover),
        Subsingleton (𝒲.sectionsOf (fibreAt c u s) (fibreModule c u s M)).H1 ∧
          Module.finrank k (𝒲.sectionsOf (fibreAt c u s) (fibreModule c u s M)).H0 = 1) →
      (∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ V)
        (σ : 𝟙_ (pullback c (x ≫ u)).Modules ⟶ (Scheme.Modules.pullback (mapOnProdOver c x
          rfl)).obj M), σ ≠ 0 →
        ∃ Dx : RelEffCartierDiv c g (x ≫ u), Dx.I = Scheme.Modules.zeroSchemeIdeal σ ∧
          Dx.SupportedIn U) →
      ∃ (D₀ : RelEffCartierDiv c g u) (N : V.Modules), Scheme.Modules.IsInvertible N ∧
        Nonempty (D₀.lineBundle ≅ M ⊗ (Scheme.Modules.pullback (pullback.snd c u)).obj N) ∧
        ∀ (d' : ℕ) (D' : RelEffCartierDiv c d' u) (N' : V.Modules), Scheme.Modules.IsInvertible N'
          → D'.SupportedIn U →
          Nonempty (D'.lineBundle ≅ M ⊗ (Scheme.Modules.pullback (pullback.snd c u)).obj N') → D'.I
            = D₀.I)
    (Dγ : ι → RelEffCartierDiv c e (𝟙 (Spec (CommRingCat.of R))))
    (hDγU : ∀ i, (Dγ i).SupportedIn U)
    (hχ : ∀ (i : ι) (k : Type u) [Field k] [IsAlgClosed k]
      (x : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
      (𝒲 : (pullback (pullback.snd c (𝟙 (Spec (CommRingCat.of R)))) x).TwoAffineOpenCover),
      (Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
          (fibreModule c (𝟙 _) x (sectionTwist c ε (𝟙 _) r ⊗ (Dγ i).idealModule))).H0 : ℤ) -
        Module.finrank k (𝒲.sectionsOf (fibreAt c (𝟙 _) x)
          (fibreModule c (𝟙 _) x (sectionTwist c ε (𝟙 _) r ⊗ (Dγ i).idealModule))).H1 = 1)
    (hZfibγ : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
      (L : RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
      ∀ (k : Type u) [Field k] [IsAlgClosed k] (x : Spec (CommRingCat.of k) ⟶ T)
        (σ : 𝟙_ (pullback c (x ≫ t)).Modules ⟶ (Scheme.Modules.pullback (mapOnProdOver c x rfl)).obj
          (L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
            t)).idealModule))), σ ≠ 0 →
        ∃ Dx : RelEffCartierDiv c g (x ≫ t), Dx.I = Scheme.Modules.zeroSchemeIdeal σ ∧
          Dx.SupportedIn U)
    (hH0one : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) (L :
      RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
      ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (𝒲 : (pullback (pullback.snd c t)
        s).TwoAffineOpenCover),
        Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          (L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
            t)).idealModule)))).H1 →
        Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          (L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
            t)).idealModule)))).H0 = 1)
    (hcover : ∀ ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) (L : RigidifiedLineBundle c ε t),
      FibrewiseAlgEquivZero L → ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T),
      ∃ i : ι, ∀ (𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover),
        Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s
          (L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
            t)).idealModule)))).H1)
    (havoid : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
      (L : RigidifiedLineBundle c ε t), FibrewiseAlgEquivZero L →
      ∀ (D₀ : RelEffCartierDiv c g t) (N : T.Modules), Scheme.Modules.IsInvertible N →
        Nonempty (D₀.lineBundle ≅
          (L.L ⊗ (sectionTwist c ε t r ⊗ ((Dγ i).pullbackAlong t (Category.comp_id
            t)).idealModule)) ⊗
            (Scheme.Modules.pullback (pullback.snd c t)).obj N) →
        D₀.SupportedIn U)
    (hcut : ∀ (i : ι) ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
      (D : RelEffCartierDiv c r t) (D₀ : RelEffCartierDiv c g t), D₀.SupportedIn U →
      D.I = D₀.I * ((Dγ i).pullbackAlong t (Category.comp_id t)).I →
      ∃ W : T.Opens, ∀ (k : Type u) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ T),
        Set.range ⇑s ⊆ (W : Set T) ↔
          IsAlgEquivZero (fibreAt c t s)
            ((Scheme.Modules.pullback (pullback.fst (pullback.snd c t) s)).obj (D.twistModule c
              ε))) :
    ∃ (X : ι → Scheme.{u})
      (f : ∀ i, uliftYoneda.{u + 1}.obj (X i) ⟶ (relSubPicPresheaf c ε (algEquivZeroCut c
        ε)).overTotal),
      (∀ i, MorphismProperty.presheafULift.{u + 1} @IsOpenImmersion (f i)) ∧
      (∀ i, LocallyOfFiniteType (uliftYonedaEquiv (f i)).1) ∧
      (∀ i, CompactSpace (X i)) ∧
      Presheaf.IsLocallySurjective Scheme.zariskiTopology (Limits.Sigma.desc f) ∧
      (∀ (i : ι) ⦃T : Scheme.{u}⦄
        (x : uliftYoneda.{u + 1}.obj T ⟶ (relSubPicPresheaf c ε (algEquivZeroCut c ε)).overTotal),
        LocallyOfFiniteType (uliftYonedaEquiv x).1 →
        ∀ (L : RigidifiedLineBundle c ε (uliftYonedaEquiv x).1), Quotient.mk _ L =
          (uliftYonedaEquiv x).2.1 →
        ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T),
          (∀ (𝒲 : (pullback (pullback.snd c (uliftYonedaEquiv x).1) s).TwoAffineOpenCover),
            Subsingleton (𝒲.sectionsOf (fibreAt c (uliftYonedaEquiv x).1 s) (fibreModule c
              (uliftYonedaEquiv x).1 s
              (L.L ⊗ (sectionTwist c ε (uliftYonedaEquiv x).1 r ⊗
                ((Dγ i).pullbackAlong (uliftYonedaEquiv x).1 (Category.comp_id
                  _)).idealModule)))).H1) →
          ∃ φ' : Spec (CommRingCat.of k) ⟶ X i,
            uliftYoneda.{u + 1}.map φ' ≫ f i = uliftYoneda.{u + 1}.map s ≫ x) ∧
      (∀ i, ∃ j : X i ⟶ Y, IsOpenImmersion j ∧ j ≫ y = (uliftYonedaEquiv (f i)).1) := by
  classical
  have hch := fun i =>
    exists_openChart_openImmersion_relSubPicPresheaf_algEquivZeroCut_of_fibrewise_zeroScheme
    R c 𝒱 hH0 ε U hεU g e r hr hg Y y Duniv hDunivU huniv (Dγ i) (hDγU i) (hχ i) hsect (hZfibγ i)
      (hH0one i) (havoid i) (hcut i)
  choose X f hft hqc hj hH using hch
  have hGover : Presieve.IsSheaf (Scheme.zariskiTopology.over (Spec (CommRingCat.of R)))
      (relSubPicPresheaf c ε (algEquivZeroCut c ε)) :=
    isSheaf_relSubPicPresheaf_algEquivZeroCut_zariski_of_bijective_sections R c ε hH0
  have hG : Presieve.IsSheaf Scheme.zariskiTopology (relSubPicPresheaf c ε (algEquivZeroCut c
    ε)).overTotal :=
    (relSubPicPresheaf c ε (algEquivZeroCut c ε)).overTotal_isSheaf _ hGover
  have hinj := isLFPInj_relSubPicPresheaf_algEquivZeroCut_of_twoAffineOpenCover R c 𝒱 ε
  have hX : ∀ i, HomIsLFP (uliftYonedaEquiv (f i)).1 := fun i => by
    have : LocallyOfFiniteType (uliftYonedaEquiv (f i)).1 := hft i
    have : IsLocallyNoetherian (Spec (CommRingCat.of R)) := inferInstance
    have : LocallyOfFinitePresentation (uliftYonedaEquiv (f i)).1 := inferInstance
    exact homIsLFP_of_locallyOfFinitePresentation R _
  have H : ∀ ⦃T : Scheme.{u}⦄ (x : uliftYoneda.{u + 1}.obj T ⟶ (relSubPicPresheaf c ε
    (algEquivZeroCut c ε)).overTotal),
      LocallyOfFiniteType (uliftYonedaEquiv x).1 →
      ∃ (U' : ι → T.Opens) (φ : ∀ i, (↑(U' i) : Scheme.{u}) ⟶ X i),
        (⨆ i, U' i) = ⊤ ∧
        ∀ i, uliftYoneda.{u + 1}.map (φ i) ≫ f i = uliftYoneda.{u + 1}.map (U' i).ι ≫ x ∧
          ∀ ⦃T' : Scheme.{u}⦄ (ψ : T' ⟶ T) (φ' : T' ⟶ X i),
            LocallyOfFiniteType (ψ ≫ (uliftYonedaEquiv x).1) →
            uliftYoneda.{u + 1}.map φ' ≫ f i = uliftYoneda.{u + 1}.map ψ ≫ x →
            ∃ χ : T' ⟶ ↑(U' i), χ ≫ (U' i).ι = ψ ∧ χ ≫ φ i = φ' := by
    intro T x hxft
    have : LocallyOfFiniteType (uliftYonedaEquiv x).1 := hxft
    choose U' φ hU'φ using fun i => hH i x hxft
    refine ⟨U', φ, ?_, fun i => ⟨(hU'φ i).2.1, (hU'φ i).2.2⟩⟩
    rw [eq_top_iff]
    rintro p -
    obtain ⟨L, hLx⟩ := Quotient.exists_rep (uliftYonedaEquiv x).2.1
    have hL : FibrewiseAlgEquivZero L := by
      have h2 := (uliftYonedaEquiv x).2.2
      rw [← hLx] at h2
      exact h2
    let s : Spec (CommRingCat.of (T.residueField p)) ⟶ T := T.fromSpecResidueField p
    obtain ⟨i, hi⟩ := hcover (uliftYonedaEquiv x).1 L hL (T.residueField p) s
    have hsub : Set.range ⇑s ⊆ (U' i : Set T) := ((hU'φ i).1 L hLx (T.residueField p) s).2 hi
    have hp : p ∈ (U' i : Set T) := hsub ⟨IsLocalRing.closedPoint _,
      Scheme.fromSpecResidueField_apply p _⟩
    exact TopologicalSpace.Opens.mem_iSup.2 ⟨i, hp⟩
  obtain ⟨hopen, hsurj⟩ :=
    presheafULift_isOpenImmersion_and_isLocallySurjective_of_locallyOfFiniteType R
      (relSubPicPresheaf c ε (algEquivZeroCut c ε)) hG hlfp hinj X f hX H
  refine ⟨X, f, hopen, hft, hqc, hsurj, ?_, hj⟩
  intro i T x hxft L hLx k _ s hs
  have : LocallyOfFiniteType (uliftYonedaEquiv x).1 := hxft
  obtain ⟨U', φ, hU'⟩ := hH i x hxft
  have hsub : Set.range ⇑s ⊆ (U' : Set T) := (hU'.1 L hLx k s).2 hs
  have hsub' : Set.range ⇑s ⊆ Set.range ⇑U'.ι := by rwa [Scheme.Opens.range_ι]
  refine ⟨IsOpenImmersion.lift U'.ι s hsub' ≫ φ, ?_⟩
  rw [Functor.map_comp, Category.assoc, hU'.2.1, ← Category.assoc, ← Functor.map_comp,
    IsOpenImmersion.lift_fac]