forgetToSheafModuleCat

Mathlib.Algebra.Category.ModuleCat.Sheaf

URI: https://scilib.ai/kg/mathlib#SheafOfModules.forgetToSheafModuleCat

Lean4

/-- The forgetful functor from sheaves of modules over sheaf of ring `R` to sheaves of `R(X)`-module
when `X` is initial.
-/
@[simps]
noncomputable def forgetToSheafModuleCat (X : Cᵒᵖ) (hX : Limits.IsInitial X) :
    SheafOfModules.{w} R ⥤ Sheaf J (ModuleCat.{w} (R.1.obj X))
    where
  obj
    M :=
    ⟨(PresheafOfModules.forgetToPresheafModuleCat X hX).obj M.1,
      Presheaf.isSheaf_of_isSheaf_comp _ _ (forget₂ (ModuleCat.{w} (R.1.obj X)) AddCommGrpCat.{w}) M.isSheaf⟩
  map f := { val := (PresheafOfModules.forgetToPresheafModuleCat X hX).map f.1 }

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru