restrictScalars

Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.restrictScalars

Lean4

/-- The restriction of scalars functor `PresheafOfModules R' ⥤ PresheafOfModules R`
induced by a morphism of presheaves of rings `R ⟶ R'`. -/
@[simps]
noncomputable def restrictScalars (α : R ⟶ R') : PresheafOfModules.{v} R' ⥤ PresheafOfModules.{v} R
    where
  obj M' := M'.restrictScalarsObj α
  map
    φ' :=
    { app := fun X ↦ (ModuleCat.restrictScalars (α.app X).hom).map (Hom.app φ' X)
      naturality := fun {X Y} f ↦ by
        ext x
        exact naturality_apply φ' f x }

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

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

Разделы

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

Аффилиация

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