SectionLocalization.lean

def sectionEnd {X : Scheme.{u}} (M : X.Modules) (f : Γ(X, ⊤)) : End M.presheaf where
  app V := M.smul (X.presheaf.map V.unop.leTop.op f)
  naturality {V W} i := by
    symm
    have hsmul : M.smul (X.presheaf.map V.unop.leTop.op f) ≫ M.presheaf.map i =
        M.presheaf.map i ≫ M.smul
          (X.presheaf.map i (X.presheaf.map V.unop.leTop.op f)) := by
      simpa only [Quiver.Hom.op_unop] using
        M.map_comp_smul i.unop (X.presheaf.map V.unop.leTop.op f)
    rw [hsmul]
    have h : X.presheaf.map i (X.presheaf.map V.unop.leTop.op f) =
        X.presheaf.map W.unop.leTop.op f := by
      change (X.presheaf.map V.unop.leTop.op ≫ X.presheaf.map i) f = _
      rw [← Functor.map_comp]
      rfl
    rw [h]

lemma sectionEnd_pow_app {X : Scheme.{u}} (M : X.Modules) (f : Γ(X, ⊤))
    (n : ℕ) (V : X.Opens) :
    ((sectionEnd M f) ^ n).app (op V) =
      M.smul (X.presheaf.map V.leTop.op (f ^ n))

lemma sectionEnd_pow_apply {X : Scheme.{u}} (M : X.Modules) (f : Γ(X, ⊤))
    (n : ℕ) (V : X.Opens) (x : Γ(M, V)) :
    ((sectionEnd M f) ^ n).app (op V) x =
      X.presheaf.map V.leTop.op (f ^ n) • x

lemma sectionEnd_act {X : Scheme.{u}} (M : X.Modules)
    (f : Γ(X, ⊤)) (n : ℕ) (V : X.Opens) (x : Γ(M, V)) :
    AbelianSectionLocalization.act M.presheaf (sectionEnd M f) n V x =
      (X.presheaf.map V.leTop.op f) ^ n • x

lemma restriction_eq_zero_iff {X : Scheme.{u}} (M : X.Modules)
    {U V W : X.Opens} (hVU : V ≤ U) (hWU : W ≤ U) (hVW : V = W) (z : Γ(M, U)) :
    M.presheaf.map (homOfLE hVU).op z = 0 ↔
      M.presheaf.map (homOfLE hWU).op z = 0

lemma clauses_iff {X : Scheme.{u}} (M : X.Modules)
    (f : Γ(X, ⊤)) (V : X.Opens) :
    BasicOpenLocalization M V (X.presheaf.map V.leTop.op f) ↔
      AbelianSectionLocalization.Clauses M.presheaf (sectionEnd M f) (X.basicOpen f) V

lemma top_restriction {X : Scheme.{u}} (f : Γ(X, ⊤)) :
    X.presheaf.map (⊤ : X.Opens).leTop.op f = f

lemma affine_clauses_restrict {X Y : Scheme.{u}} (M : X.Modules)
    (hlocal : ∀ V : X.affineOpens, ∀ f : Γ(X, V.1), BasicOpenLocalization M V.1 f)
    (j : Y ⟶ X) [IsOpenImmersion j] :
    ∀ V : Y.affineOpens, ∀ f : Γ(Y, V.1), BasicOpenLocalization (M.restrict j) V.1 f

lemma clauses_top_of_affine {X : Scheme.{u}} (M : X.Modules)
    (hlocal : ∀ V : X.affineOpens, ∀ f : Γ(X, V.1), BasicOpenLocalization M V.1 f)
    [CompactSpace X] [QuasiSeparatedSpace X] (f : Γ(X, ⊤)) :
    BasicOpenLocalization M ⊤ f

theorem exists_pow_smul_eq_zero_of_affine_localization {X : Scheme.{u}}
    (M : X.Modules)
    (hlocal : ∀ V : X.affineOpens, ∀ f : Γ(X, V.1), BasicOpenLocalization M V.1 f)
    {U : X.Opens} (hU : IsCompact (U : Set X)) (f : Γ(X, U)) (y : Γ(M, U))
    (hy : M.presheaf.map (homOfLE (X.basicOpen_le f)).op y = 0) :
    ∃ n : ℕ, (f ^ n : Γ(X, U)) • y = 0

theorem basicOpenLocalization_of_affine_localization {X : Scheme.{u}}
    (M : X.Modules)
    (hlocal : ∀ V : X.affineOpens, ∀ f : Γ(X, V.1), BasicOpenLocalization M V.1 f)
    {U : X.Opens} (hU : IsCompact (U : Set X))
    (hqs : IsQuasiSeparated (U : Set X)) (f : Γ(X, U)) :
    BasicOpenLocalization M U f

theorem basicOpenLocalization_of_isQuasicoherent_of_qcqs {X : Scheme.{u}}
    (M : X.Modules) [M.IsQuasicoherent] {U : X.Opens}
    (hU : IsCompact (U : Set X)) (hqs : IsQuasiSeparated (U : Set X)) (f : Γ(X, U)) :
    BasicOpenLocalization M U f

theorem isLocalizedModule_basicOpen_of_isQuasicoherent_of_qcqs {X : Scheme.{u}}
    (M : X.Modules) [M.IsQuasicoherent] {U : X.Opens}
    (hU : IsCompact (U : Set X)) (hqs : IsQuasiSeparated (U : Set X)) (f : Γ(X, U)) :
    IsLocalizedModule.Away f
      (show Γ(M, U) →ₗ[Γ(X, U)]
        (ModuleCat.restrictScalars (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom).obj
          (ModuleCat.of Γ(X, X.basicOpen f) Γ(M, X.basicOpen f)) from
        (M.val.map (homOfLE (X.basicOpen_le f)).op).hom) := by
  have h := basicOpenLocalization_of_isQuasicoherent_of_qcqs M hU hqs f
  apply IsLocalizedModule.Away.mk_of_addCommGroup
  · rw [Module.End.isUnit_iff]
    change Function.Bijective (fun x :
      (ModuleCat.restrictScalars
        (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom).obj
          (ModuleCat.of Γ(X, X.basicOpen f) Γ(M, X.basicOpen f)) => f • x)
    have hf : IsUnit ((X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom f) :=
      RingedSpace.isUnit_res_basicOpen X.toRingedSpace f
    have hfun : (fun x :
        (ModuleCat.restrictScalars
          (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom).obj
            (ModuleCat.of Γ(X, X.basicOpen f) Γ(M, X.basicOpen f)) => f • x) =
        (fun x : ModuleCat.of Γ(X, X.basicOpen f) Γ(M, X.basicOpen f) =>
          (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom f • x) := by
      funext x
      exact ModuleCat.restrictScalars.smul_def
        (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom f x
    rw [hfun]
    exact hf.smul_bijective (β := ModuleCat.of Γ(X, X.basicOpen f) Γ(M, X.basicOpen f))
  · intro x
    obtain ⟨n, y, hy⟩ := h.1 x
    refine ⟨n, y, ?_⟩
    rw [ModuleCat.restrictScalars.smul_def]
    exact hy.symm
  · intro y hy
    exact h.2 y hy