Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

Change of presheaf of rings #

In this file, we define the restriction of scalars functor restrictScalars α : PresheafOfModules.{v} R' ⥤ PresheafOfModules.{v} R attached to a morphism of presheaves of rings α : R ⟶ R'.

The restriction of scalars of presheaves of modules, on objects.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem PresheafOfModules.restrictScalarsObj_map_hom_apply {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (M' : PresheafOfModules R') (α : R R') {X Y : Cᵒᵖ} (f : X Y) (a : (M'.obj X)) :
    ((M'.restrictScalarsObj α).map f).hom a = (M'.map f).hom a
    @[simp]
    theorem PresheafOfModules.restrictScalarsObj_obj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (M' : PresheafOfModules R') (α : R R') (X : Cᵒᵖ) :
    (M'.restrictScalarsObj α).obj X = (ModuleCat.restrictScalars (α.app X).hom).obj (M'.obj X)

    The restriction of scalars functor PresheafOfModules R' ⥤ PresheafOfModules R induced by a morphism of presheaves of rings R ⟶ R'.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem PresheafOfModules.restrictScalars_map_app {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R R') {X✝ Y✝ : PresheafOfModules R'} (φ' : X✝ Y✝) (X : Cᵒᵖ) :
      ((PresheafOfModules.restrictScalars α).map φ').app X = (ModuleCat.restrictScalars (α.app X).hom).map (φ'.app X)