tildeInModuleCat

Mathlib.AlgebraicGeometry.Modules.Tilde

URI: https://scilib.ai/kg/mathlib#ModuleCat.tildeInModuleCat

Lean4

/-- This is `M^~` as a sheaf of `R`-modules.
-/
noncomputable def tildeInModuleCat : TopCat.Presheaf (ModuleCat R) (PrimeSpectrum.Top R) :=
  (PresheafOfModules.forgetToPresheafModuleCat (op ⊤) <| Limits.initialOpOfTerminal Limits.isTerminalTop).obj
      (tilde M).1 ⋙
    ModuleCat.restrictScalars (StructureSheaf.globalSectionsIso R).hom.hom

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

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

Разделы

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

Аффилиация

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