Lean4
/-- `M^~` as a sheaf of `𝒪_{Spec R}`-modules
-/
noncomputable def tilde : (Spec <| .of R).Modules
where
val :=
{ obj := fun U ↦ ModuleCat.of _ (M.tildeInType.val.obj U)
map := fun {U V} i ↦
ofHom (Y :=
(restrictScalars ((Spec <| .of R).ringCatSheaf.val.map i).hom).obj
(of ((Spec <| .of R).ringCatSheaf.val.obj V) (M.tildeInType.val.obj V)))
{ toFun := M.tildeInType.val.map i
map_smul' := by intros; rfl
map_add' := by intros; rfl } }
isSheaf := (TopCat.Presheaf.isSheaf_iff_isSheaf_comp (forget AddCommGrpCat) _).2 M.tildeInType.2