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')
:
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)
noncomputable def
PresheafOfModules.restrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ 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.
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)
@[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.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')
:
The isomorphism restrictScalars α ⋙ toPresheaf R ≅ toPresheaf R'
for any
morphism of presheaves of rings α : R ⟶ R'
.