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'.

noncomputable def PresheafOfModules.restrictScalarsObj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (M' : PresheafOfModules R') (α : R ⟶ R') : PresheafOfModules R

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

Equations

• One or more equations did not get rendered due to their size.

@[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)

noncomputable def PresheafOfModules.restrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') : CategoryTheory.Functor (PresheafOfModules R') (PresheafOfModules R)

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.

@[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)

@[simp]

theorem PresheafOfModules.restrictScalars_obj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') (M' : PresheafOfModules R') : (PresheafOfModules.restrictScalars α).obj M' = M'.restrictScalarsObj α

instance PresheafOfModules.instAdditiveRestrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') : (PresheafOfModules.restrictScalars α).Additive

instance PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} : (PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R)).Full

instance PresheafOfModules.instFaithfulRestrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') : (PresheafOfModules.restrictScalars α).Faithful

noncomputable def PresheafOfModules.restrictScalarsCompToPresheaf {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') : (PresheafOfModules.restrictScalars α).comp (PresheafOfModules.toPresheaf R) ≅ PresheafOfModules.toPresheaf R'

The isomorphism restrictScalars α ⋙ toPresheaf R ≅ toPresheaf R' for any morphism of presheaves of rings α : R ⟶ R'.

Equations

• PresheafOfModules.restrictScalarsCompToPresheaf α = CategoryTheory.Iso.refl ((PresheafOfModules.restrictScalars α).comp (PresheafOfModules.toPresheaf R))