FrameDescent.lean

abbrev res (M : X.Modules) (m : Γ(M, ⊤)) (W : X.Opens) : Γ(M, W)

def IsFrame (M : X.Modules) (m : Γ(M, ⊤)) (U : X.Opens) : Prop

theorem res_map (M : X.Modules) (m : Γ(M, ⊤)) {W W' : X.Opens} (i : W' ⟶ W) :
    M.presheaf.map i.op (res M m W) = res M m W'

theorem smul_res (M : X.Modules) (m : Γ(M, ⊤)) {W W' : X.Opens} (i : W' ⟶ W) (g : Γ(X, W)) :
    M.presheaf.map i.op (g • res M m W) = X.presheaf.map i.op g • res M m W'

theorem res_smul (M : X.Modules) (H : Γ(X, ⊤)) (m : Γ(M, ⊤)) (W : X.Opens) :
    res M (H • m) W = X.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op H • res M m W

theorem app_res {M N : X.Modules} (φ : M ⟶ N) (m : Γ(M, ⊤)) (W : X.Opens) :
    φ.app W (res M m W) = res N (φ.app ⊤ m) W

theorem IsFrame.of_iso {M N : X.Modules} (e : M ≅ N) {m : Γ(M, ⊤)} {U : X.Opens}
    (hm : IsFrame M m U) :
    IsFrame N (e.hom.app ⊤ m) U

theorem isFrame_of_iso_unit {M : X.Modules} (e : M ≅ SheafOfModules.unit X.ringCatSheaf) :
    IsFrame M (e.inv.app ⊤ (show Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), ⊤) from
      (1 : Γ(X, ⊤)))) ⊤ := by
  have h1 : IsFrame (SheafOfModules.unit X.ringCatSheaf : X.Modules)
      (show Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), ⊤) from (1 : Γ(X, ⊤))) ⊤ := by
    intro W _
    have hres : res (SheafOfModules.unit X.ringCatSheaf : X.Modules)
        (show Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), ⊤) from (1 : Γ(X, ⊤))) W =
        (show Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), W) from (1 : Γ(X, W))) := by
      change ((X.ringCatSheaf.obj.map (homOfLE (le_top : W ≤ ⊤)).op).hom 1) = 1
      exact map_one _
    rw [hres]
    change Function.Bijective fun g : Γ(X, W) => g * 1
    simp only [mul_one]
    exact Function.bijective_id
  exact h1.of_iso e.symm

theorem isUnit_germ_of_isFrame_smul {M : X.Modules} {T : Γ(M, ⊤)} {U : X.Opens} (hT : IsFrame M T U)
    (H : Γ(X, ⊤)) {z : X} {V : X.Opens} (hzV : z ∈ V) (hVU : V ≤ U) (hHT : IsFrame M (H • T) V) :
    IsUnit (X.presheaf.germ V z hzV (X.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op H))

theorem exists_isFrame_smul_of_isUnit_germ {M : X.Modules} {T : Γ(M, ⊤)} {U : X.Opens}
    (hT : IsFrame M T U)
    (H : Γ(X, ⊤)) {z : X} (hzU : z ∈ U)
    (hu : IsUnit (X.presheaf.germ U z hzU (X.presheaf.map (homOfLE (le_top : U ≤ ⊤)).op H))) :
    ∃ V : X.Opens, z ∈ V ∧ IsFrame M (H • T) V

theorem res_top (M : X.Modules) (m : Γ(M, ⊤)) : res M m ⊤ = m

theorem IsFrame.of_openImmersion {Y : Scheme.{u}} (j : Y ⟶ X) [IsOpenImmersion j]
    (M : X.Modules) (m : Γ(M, ⊤))
    {U' : Y.Opens}
    (hfr : IsFrame ((Scheme.Modules.pullback j).obj M)
      (show Γ((Scheme.Modules.pullback j).obj M, ⊤) from
        (((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M).app ⊤) m) U') :
    IsFrame M m (j ''ᵁ U') := by
  intro V hV
  have hVr : V ≤ j.opensRange := hV.trans (j.image_le_opensRange U')
  have : IsIso (j.app V) := j.isIso_app V hVr
  have ha : Function.Bijective (j.app V) := ConcreteCategory.bijective_of_isIso (j.app V)
  have hb : Function.Bijective
      (((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M).app V) :=
    Scheme.Modules.bijective_unit_app_of_le_opensRange j M V hVr
  have hW' : j ⁻¹ᵁ V ≤ U' :=
    (show j ⁻¹ᵁ V ≤ j ⁻¹ᵁ (j ''ᵁ U') from fun x hx => hV hx).trans_eq (j.preimage_image_eq U')
  have hψ := hfr (j ⁻¹ᵁ V) hW'
  have key : (((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M).app V) ∘
      (fun g : Γ(X, V) => g • res M m V) =
      (fun g : Γ(Y, j ⁻¹ᵁ V) => g • res ((Scheme.Modules.pullback j).obj M)
        (show Γ((Scheme.Modules.pullback j).obj M, ⊤) from
          (((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M).app ⊤) m)
          (j ⁻¹ᵁ V)) ∘ (j.app V) := by
    funext g
    simp only [Function.comp_apply]
    erw [Scheme.Modules.Hom.app_smul, app_res]
    rfl
  have hcomp : Function.Bijective
      ((((Scheme.Modules.pullbackPushforwardAdjunction j).unit.app M).app V) ∘
      (fun g : Γ(X, V) => g • res M m V)) := by
    rw [key]; exact hψ.comp ha
  exact (Function.Bijective.of_comp_iff' hb _).1 hcomp

theorem exists_iso_forall_unit_eq {X Y Z : Scheme.{u}} (g : Z ⟶ Y) (f : Y ⟶ X) (h : Z ⟶ X)
    (hh : g ≫ f = h) (M : X.Modules) :
    ∃ e : (Scheme.Modules.pullback h).obj M ≅
      (Scheme.Modules.pullback g).obj ((Scheme.Modules.pullback f).obj M),
      ∀ s : Γ(M, ⊤),
        (e.hom.app ⊤) ((((Scheme.Modules.pullbackPushforwardAdjunction h).unit.app M).app ⊤) s) =
          (show Γ((Scheme.Modules.pullback g).obj ((Scheme.Modules.pullback f).obj M), ⊤) from
            (((Scheme.Modules.pullbackPushforwardAdjunction g).unit.app
              ((Scheme.Modules.pullback f).obj M)).app ⊤)
              (show Γ((Scheme.Modules.pullback f).obj M, ⊤) from
                (((Scheme.Modules.pullbackPushforwardAdjunction f).unit.app M).app ⊤) s)) := by
  subst hh
  refine ⟨((Scheme.Modules.pullbackComp g f).app M).symm, fun s => ?_⟩
  exact CategoryTheory.ConcreteCategory.congr_hom
    (Scheme.Modules.unit_app_comp_pullbackComp_inv g f M ⊤) s

abbrev pb {X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules) (m : Γ(M, ⊤)) :
    Γ((Scheme.Modules.pullback p).obj M, ⊤)

theorem pb_smul {X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules) (r : Γ(X, ⊤)) (m : Γ(M, ⊤)) :
    pb p M (r • m) = p.appTop r • pb p M m

theorem main {X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
    (m : Γ(M, ⊤)) (z : X')
    (h : ∃ U' : X'.Opens, z ∈ U' ∧ IsFrame ((Scheme.Modules.pullback p).obj M) (pb p M m) U') :
    ∃ U : X.Opens, p z ∈ U ∧ IsFrame M m U

theorem _root_.AlgebraicGeometry.Scheme.Modules.exists_frame_of_frame_pullback
    {X X' : Scheme.{u}} (p : X' ⟶ X) (M : X.Modules) (hM : Scheme.Modules.IsInvertible M)
    (m : Γ(M, ⊤)) (z : X')
    (h : ∃ U' : X'.Opens, z ∈ U' ∧ ∀ V' : X'.Opens, V' ≤ U' →
      Function.Bijective fun g : Γ(X', V') =>
        g • (((Scheme.Modules.pullback p).obj M).presheaf.map (homOfLE (le_top : V' ≤ ⊤)).op
          ((((Scheme.Modules.pullbackPushforwardAdjunction p).unit.app M).app ⊤) m) :
            Γ((Scheme.Modules.pullback p).obj M, V'))) :
    ∃ U : X.Opens, p z ∈ U ∧ ∀ V : X.Opens, V ≤ U →
      Function.Bijective fun g : Γ(X, V) =>
        g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op m : Γ(M, V)) :=
  FrameSpecSol.main p M hM m z h