Change of sheaf of rings #
In this file, we define the restriction of scalars functor
restrictScalars α : SheafOfModules.{v} R' ⥤ SheafOfModules.{v} R
attached to a morphism of sheaves of rings α : R ⟶ R'.
noncomputable def
SheafOfModules.restrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R R' : CategoryTheory.Sheaf J RingCat}
(α : R ⟶ R')
:
The restriction of scalars functor SheafOfModules R' ⥤ SheafOfModules R
induced by a morphism of sheaves of rings R ⟶ R'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
SheafOfModules.restrictScalars_map_val
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R R' : CategoryTheory.Sheaf J RingCat}
(α : R ⟶ R')
{X✝ Y✝ : SheafOfModules R'}
(φ : X✝ ⟶ Y✝)
:
((SheafOfModules.restrictScalars α).map φ).val = (PresheafOfModules.restrictScalars α.val).map φ.val
@[simp]
theorem
SheafOfModules.restrictScalars_obj_val
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R R' : CategoryTheory.Sheaf J RingCat}
(α : R ⟶ R')
(M' : SheafOfModules R')
:
((SheafOfModules.restrictScalars α).obj M').val = (PresheafOfModules.restrictScalars α.val).obj M'.val
instance
SheafOfModules.instAdditiveRestrictScalars
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R R' : CategoryTheory.Sheaf J RingCat}
(α : R ⟶ R')
:
(SheafOfModules.restrictScalars α).Additive
noncomputable def
PresheafOfModules.restrictHomEquivOfIsLocallySurjective
{C : Type u'}
[CategoryTheory.Category.{v', u'} C]
{J : CategoryTheory.GrothendieckTopology C}
{R R' : CategoryTheory.Functor Cᵒᵖ RingCat}
(α : R ⟶ R')
{M₁ M₂ : PresheafOfModules R'}
(hM₂ : CategoryTheory.Presheaf.IsSheaf J M₂.presheaf)
[CategoryTheory.Presheaf.IsLocallySurjective J α]
:
(M₁ ⟶ M₂) ≃ ((PresheafOfModules.restrictScalars α).obj M₁ ⟶ (PresheafOfModules.restrictScalars α).obj M₂)
The functor PresheafOfModules.restrictScalars α induces bijections on
morphisms if α is locally surjective and the target presheaf is a sheaf.
Equations
- One or more equations did not get rendered due to their size.