Scheme_Modules_nonempty_iso_unit_of_forall_pullback_rigSection_iso_unit.lean

def pb2 {X₀ X₁ X₂ : Scheme.{u}} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (L : X₂.Modules) :
    (Scheme.Modules.pullback f).obj ((Scheme.Modules.pullback g).obj L) ≅ (Scheme.Modules.pullback
      (f ≫ g)).obj L

theorem nonempty_iso_unit_of_iso_comp {X Y Y' : Scheme.{u}} {K : X.Modules} (f : Y ⟶ X) (f' : Y' ⟶
  X) (e : Y' ⟶ Y)
    [IsIso e] (hef : e ≫ f = f')
    (h : Nonempty ((Scheme.Modules.pullback f).obj K ≅ SheafOfModules.unit Y.ringCatSheaf)) :
    Nonempty ((Scheme.Modules.pullback f').obj K ≅ SheafOfModules.unit Y'.ringCatSheaf)

theorem nonempty_iso_unit_of_iSup_eq_top_of_pairwise_disjoint
    {Y : Scheme.{u}} (N : Y.Modules) {ι' : Type*} (V : ι' → Y.Opens) (hV : ⨆ i, V i = ⊤)
    (hdisj : Pairwise fun i j => Disjoint (V i) (V j))
    (htriv : ∀ i, Nonempty ((Scheme.Modules.pullback (V i).ι).obj N ≅ SheafOfModules.unit (V
      i).toScheme.ringCatSheaf)) :
    Nonempty (N ≅ SheafOfModules.unit Y.ringCatSheaf) := by
  classical
  choose s hs using fun i => Scheme.Modules.exists_isFrameOn_of_pullback_iso_unit (M := N) (V i)
    (htriv i).some
  let F : TopCat.Sheaf Ab Y.toPresheafedSpace := ⟨N.presheaf, N.isSheaf⟩
  have hcompat : TopCat.Presheaf.IsCompatible F.obj V s := by
    intro i j
    by_cases hij : i = j
    · subst hij; rfl
    · have hbot : V i ⊓ V j = ⊥ := (hdisj hij).eq_bot
      apply F.eq_of_locally_eq' (fun e : PEmpty.{1} => e.elim) (V i ⊓ V j) (fun e => e.elim)
      · rw [hbot]; exact bot_le
      · intro e; exact e.elim
  obtain ⟨t, ht, -⟩ := F.existsUnique_gluing' V ⊤ (fun i => homOfLE le_top) (by rw [hV]) s hcompat
  have hframe : ∀ i, Scheme.Modules.IsFrameOn (t : Γ(N, ⊤)) (V i) := by
    intro i W hWU hWV
    have key : N.presheaf.map (homOfLE hWU).op t = N.presheaf.map (homOfLE hWV).op (s i) := by
      rw [← ht i, ← CategoryTheory.comp_apply, ← Functor.map_comp]
      rfl
    have hb := hs i hWV hWV
    simp only [← key] at hb
    exact hb
  have htop : Scheme.Modules.IsFrameOn (t : Γ(N, ⊤)) (⊤ : Y.Opens) := by
    have h := Scheme.Modules.IsFrameOn.of_iSup V hframe
    rwa [hV] at h
  obtain ⟨e⟩ := htop.nonempty_pullback_iso_unit ⊤ le_rfl le_rfl
  have : IsIso (⊤ : Y.Opens).ι := by rw [← Scheme.topIso_hom]; infer_instance
  refine ⟨((Scheme.Modules.pullbackId Y).app N).symm ≪≫
    (Scheme.Modules.pullbackCongr (IsIso.inv_hom_id (⊤ : Y.Opens).ι).symm).app N ≪≫
    (pb2 (inv (⊤ : Y.Opens).ι) (⊤ : Y.Opens).ι N).symm ≪≫
    (Scheme.Modules.pullback (inv (⊤ : Y.Opens).ι)).mapIso e ≪≫ Scheme.Modules.pullbackUnitIso _⟩

theorem isOpenImmersion_of_rationalPoint
    {k : Type u} [Field k] {Z : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of k))
    [IsSeparated z] [IsReduced Z] [DiscreteTopology Z]
    (ζ : SchemeHomOver (𝟙 (Spec (CommRingCat.of k))) z) : IsOpenImmersion ζ.1

theorem
  _root_.AlgebraicGeometry.Scheme.Modules.nonempty_iso_unit_of_forall_pullback_rigSection_iso_unit
    {k : Type u} [Field k] {Z T : Scheme.{u}} (z : Z ⟶ Spec (CommRingCat.of k)) [IsSeparated z]
      [IsReduced Z] [Finite Z]
    (t : T ⟶ Spec (CommRingCat.of k)) {ι : Type v} (ζ : ι → SchemeHomOver (𝟙 (Spec (CommRingCat.of
      k))) z)
    (hcov : ∀ w : Z, ∃ j, (ζ j).1.base (IsLocalRing.closedPoint k) = w)
    (F : (Limits.pullback z t).Modules)
    (htriv : ∀ j, Nonempty ((Scheme.Modules.pullback (rigSection z t (ζ j))).obj F ≅
      SheafOfModules.unit T.ringCatSheaf)) :
    Nonempty (F ≅ SheafOfModules.unit (Limits.pullback z t).ringCatSheaf)