some thing about sheaves of modules

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -497,4 +497,64 @@ def unitHomEquiv (M : PresheafOfModules R) :
     ext X
     exact (LinearMap.ringLmapEquivSelf (R.obj X) ℤ (M.obj X)).apply_symm_apply (s.val X)
 
+noncomputable instance module_over_initial (X : Cᵒᵖ) (hX : Limits.IsInitial X)
+    (c : Cᵒᵖ) (M : PresheafOfModules.{v} R) :
+    Module (R.1.obj X) (M.presheaf.obj c) :=
+  Module.compHom (M.presheaf.obj c) (R.1.map (hX.to c))
+
+@[simps]
+noncomputable def forgetToPresheafModuleCatObj
+    (X : Cᵒᵖ) (hX : Limits.IsInitial X) (M : PresheafOfModules.{v} R) :
+    Cᵒᵖ ⥤ ModuleCat (R.1.obj X) :=
+{ obj := fun c =>
+      letI := module_over_initial (R := R) X hX
+      ModuleCat.of _ (M.presheaf.obj c)
+  map := fun {c₁ c₂} f =>
+    { toFun := fun x => M.presheaf.map f x
+      map_add' := M.presheaf.map f |>.map_add
+      map_smul' := fun r (m : M.presheaf.obj c₁) => by
+        dsimp
+        change M.presheaf.map f (R.1.map (hX.to c₁) _ • m) = R.1.map (hX.to c₂) _ • _
+        rw [M.map_smul, ← CategoryTheory.comp_apply, ← R.map_comp]
+        congr
+        apply hX.hom_ext }
+  map_id := fun c => by
+      dsimp
+      ext x
+      change M.presheaf.map _ x = x
+      rw [M.presheaf.map_id]
+      rfl
+  map_comp := fun {c₁ c₂ c₃} f g => by
+      dsimp
+      ext x
+      change M.presheaf.map _ x = (M.presheaf.map _ ≫ M.presheaf.map _) x
+      rw [← M.presheaf.map_comp] }
+
+@[simps]
+noncomputable def forgetToPresheafModuleCatMap
+    (X : Cᵒᵖ) (hX : Limits.IsInitial X) {M N : PresheafOfModules.{v} R}
+    (f : M ⟶ N) :
+    forgetToPresheafModuleCatObj X hX M ⟶
+    forgetToPresheafModuleCatObj X hX N :=
+  { app := fun c =>
+    { toFun := f.app c
+      map_add' := (f.app c).map_add
+      map_smul' := fun r (m : M.presheaf.obj c) => by
+        change f.app c (R.1.map (hX.to c) _ • m) = R.1.map (hX.to c) _ • _
+        exact (f.app c).map_smul (R.1.map (hX.to c) _) m }
+    naturality := fun {c₁ c₂} i => by
+      dsimp
+      ext x
+      have := f.hom.naturality i
+      exact congr($this x) }
+
+@[simps]
+noncomputable def forgetToPresheafModuleCat (X : Cᵒᵖ) (hX : Limits.IsInitial X) :
+    PresheafOfModules.{v} R ⥤ Cᵒᵖ ⥤ ModuleCat (R.1.obj X) where
+  obj M := forgetToPresheafModuleCatObj X hX M
+  map f := forgetToPresheafModuleCatMap X hX f
+  map_id _ := rfl
+  map_comp _ _ := rfl
+
+
 end PresheafOfModules

Mathlib/Algebra/Category/ModuleCat/Sheaf.lean

@@ -92,6 +92,25 @@ def toSheaf : SheafOfModules.{v} R ⥤ Sheaf J AddCommGrp.{v} where
   obj M := ⟨_, M.isSheaf⟩
   map f := { val := f.val.hom }
 
+@[simps]
+noncomputable def forgetToSheafModuleCat (X : Cᵒᵖ) (hX : Limits.IsInitial X)  :
+    SheafOfModules R ⥤ Sheaf J (ModuleCat (R.1.obj X)) where
+  obj M := ⟨(PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.1, by
+    rw [CategoryTheory.Presheaf.isSheaf_iff_isSheaf_forget J
+      ((PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.1)
+      (CategoryTheory.forget.{max v₁ u₁} (ModuleCat (R.1.obj X)))]
+    let e : (PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.val ⋙
+          CategoryTheory.forget (ModuleCat ↑(R.val.obj X)) ≅
+          (M.1.presheaf ⋙ CategoryTheory.forget AddCommGrp) :=
+      NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
+    -- exact M.isSheaf
+    rw [Presheaf.isSheaf_of_iso_iff e]
+    apply Presheaf.isSheaf_comp_of_isSheaf
+    exact M.2⟩
+  map := sorry
+  map_id := sorry
+  map_comp := sorry
+
 /-- The canonical isomorphism between
 `SheafOfModules.toSheaf R ⋙ sheafToPresheaf J AddCommGrp.{v}`
 and `SheafOfModules.forget R ⋙ PresheafOfModules.toPresheaf R.val`. -/

Mathlib/AlgebraicGeometry/Quasicoherent/Tilde.lean

@@ -178,11 +178,15 @@ noncomputable instance (U : (Opens (PrimeSpectrum.Top R))ᵒᵖ) :
     Module ((𝒪_SpecR).val.obj U) ((Tilde.presheafInAddCommGrp R M).obj U) :=
   inferInstanceAs $ Module _ (Tilde.sectionsSubmodule R M U)
 
+noncomputable instance (U : (Opens (PrimeSpectrum.Top R))ᵒᵖ) :
+    Module ((Spec.structureSheaf R).1.obj U) ((Tilde.presheafInAddCommGrp R M).obj U) :=
+  inferInstanceAs $ Module _ (Tilde.sectionsSubmodule R M U)
+
 open Tilde in
 /--
 `M^~` as a sheaf of `𝒪_{Spec R}`-modules
 -/
-noncomputable def TildeInModules : SheafOfModules (𝒪_SpecR) where
+noncomputable def TildeAsSheafOfModules : SheafOfModules (𝒪_SpecR) where
   val := {
     presheaf := (presheafInAddCommGrp R M)
     module := inferInstance
@@ -197,16 +201,19 @@ noncomputable def TildeInModules : SheafOfModules (𝒪_SpecR) where
   }
   isSheaf := (TildeInAddCommGrp R M).2
 
+-- R ≅ S Mod(R) ≅ Module(S)
+noncomputable def TildeInModuleCat :
+    TopCat.Presheaf (ModuleCat ((Spec.structureSheaf R).1.obj (op ⊤))) (PrimeSpectrum.Top R) :=
+  (PresheafOfModules.forgetToPresheafModuleCat (op ⊤) sorry).obj (TildeAsSheafOfModules R M).1
+
 namespace Tilde
 
-instance (x:PrimeSpectrum.Top R): Module R (TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeInModules R M).1.presheaf x)where
-  smul r m:= by sorry
-  one_smul := sorry
-  mul_smul := sorry
-  smul_zero := sorry
-  smul_add := sorry
-  add_smul := sorry
-  zero_smul := sorry
+    -- { pt := _
+    --   ι := { app := fun U =>
+    --     openToLocalization R M ((OpenNhds.inclusion _).obj (unop U)) x (unop U).2 } }
+
+
+
 
 /-- The ring homomorphism that takes a section of the structure sheaf of `R` on the open set `U`,
 implemented as a subtype of dependent functions to localizations at prime ideals, and evaluates
@@ -230,6 +237,32 @@ theorem openToLocalization_apply (U : Opens (PrimeSpectrum.Top R)) (x : PrimeSpe
     openToLocalization R M U x hx s = (s.1 ⟨x, hx⟩ : _) :=
   rfl
 
+-- stalk of M at x is an R-module
+-- for each open U, M~(U) is an R-module
+-- how should we do the second part? do we want to do it via `Gamma(SpecR) = R`, or do we want to
+-- define R -action on `\prod_{x \in U} M_x`
+noncomputable def smul_by_r (r : R) (x : PrimeSpectrum.Top R) :
+    TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeAsSheafOfModules R M).1.presheaf x ⟶
+    TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeAsSheafOfModules R M).1.presheaf x :=
+  (TopCat.Presheaf.stalkFunctor AddCommGrp.{u} (x)).map
+  { app := fun U =>
+    { toFun := fun (m) => (((TildeAsSheafOfModules R M).1.module _).smul
+              ((Spec.structureSheaf R).1.map (op $ homOfLE le_top)
+                ((StructureSheaf.globalSectionsIso R).hom r)) m)
+      map_zero' := sorry
+      map_add' := sorry }
+    naturality := sorry }
+
+
+noncomputable instance (x:PrimeSpectrum.Top R): Module R (TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeAsSheafOfModules R M).1.presheaf x) where
+  smul r m:= smul_by_r R M r x m
+  one_smul := sorry
+  mul_smul := sorry
+  smul_zero := sorry
+  smul_add := sorry
+  add_smul := sorry
+  zero_smul := sorry
+
 noncomputable def stalkToFiberAddMonoidHom (x : PrimeSpectrum.Top R) :
     (TildeInAddCommGrp R M).presheaf.stalk x ⟶ AddCommGrp.of (LocalizedModule x.asIdeal.primeCompl M) :=
   Limits.colimit.desc ((OpenNhds.inclusion x).op ⋙ (TildeInAddCommGrp R M).1)
@@ -254,9 +287,26 @@ theorem stalkToFiberAddMonoidHom_germ (U : Opens (PrimeSpectrum.Top R)) (x : U)
     stalkToFiberAddMonoidHom R M x ((TildeInAddCommGrp R M).presheaf.germ x s) = s.1 x := by
   cases x; exact stalkToFiberAddMonoidHom_germ' R M U _ _ _
 
+-- example : TopCat.Sheaf (ModuleCat R) (PrimeSpectrum.Top R) := _
+
+-- #check (TildeInModules R M).1.obj (op ⊤)
+-- example : M → (TildeInModules R M).1.presheaf.obj (op ⊤) := _
+-- stalk M at x \iso M_x as R-module addcommgrp
+--                        as R_x module (localization)
+                          -- R_x = stalk Spec R at x
 def localizationToStalk (x : PrimeSpectrum.Top R) :
-    ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M) ⟶ ModuleCat.of R (TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeInModules R M).1.presheaf x) :=
-  show LocalizedModule x.asIdeal.primeCompl M →+ _ from LocalizedModule.lift (x.asIdeal.primeCompl)
+    AddCommGrp.of (LocalizedModule x.asIdeal.primeCompl M) ⟶
+    (TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeAsSheafOfModules R M).1.presheaf x) where
+  toFun := Quotient.lift (fun (m, s) => _) _
+  map_zero' := _
+  map_add' := _
+
+  -- show LocalizedModule x.asIdeal.primeCompl M →+ _ from
+
+  -- have := LocalizedModule.lift (x.asIdeal.primeCompl) (M := M)
+  --   (M'' := TopCat.Presheaf.stalk (C := AddCommGrp.{u}) (TildeInModules R M).1.presheaf x)
+  --   (g := _)
+
 
 
 end Tilde