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'
.
@[simp]
theorem
PresheafOfModules.restrictScalarsObj_obj
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(M' : PresheafOfModules R')
(α : R ⟶ R')
(X : Cᵒᵖ)
:
(M'.restrictScalarsObj α).obj X = (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)
@[simp]
theorem
PresheafOfModules.restrictScalarsObj_map_apply
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(M' : PresheafOfModules R')
(α : R ⟶ R')
{X : Cᵒᵖ}
{Y : Cᵒᵖ}
(f : X ⟶ Y)
(a : ↑(M'.obj X))
:
((M'.restrictScalarsObj α).map f) a = (M'.map f) a
noncomputable def
PresheafOfModules.restrictScalarsObj
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{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.restrictScalars_map_app
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
:
∀ {X Y : PresheafOfModules R'} (φ' : X ⟶ Y) (X_1 : Cᵒᵖ),
((PresheafOfModules.restrictScalars α).map φ').app X_1 = (ModuleCat.restrictScalars (α.app X_1)).map (φ'.app X_1)
@[simp]
theorem
PresheafOfModules.restrictScalars_obj
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
(M' : PresheafOfModules R')
:
(PresheafOfModules.restrictScalars α).obj M' = M'.restrictScalarsObj α
noncomputable def
PresheafOfModules.restrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{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
instance
PresheafOfModules.instAdditiveRestrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
:
(PresheafOfModules.restrictScalars α).Additive
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
:
Equations
- ⋯ = ⋯
instance
PresheafOfModules.instFaithfulRestrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
:
(PresheafOfModules.restrictScalars α).Faithful
Equations
- ⋯ = ⋯
noncomputable def
PresheafOfModules.restrictScalarsCompToPresheaf
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{R : CategoryTheory.Functor Cᵒᵖ RingCat}
{R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
:
The isomorphism restrictScalars α ⋙ toPresheaf R ≅ toPresheaf R'
for any
morphism of presheaves of rings α : R ⟶ R'
.