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 : CategoryTheory.Sheaf J RingCat} {R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R') : CategoryTheory.Functor (SheafOfModules R') (SheafOfModules 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.

@[simp]

theorem SheafOfModules.restrictScalars_map_val {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} {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 : CategoryTheory.Sheaf J RingCat} {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 : CategoryTheory.Sheaf J RingCat} {R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R') : (SheafOfModules.restrictScalars α).Additive

Equations

• ⋯ = ⋯

noncomputable def PresheafOfModules.restrictHomEquivOfIsLocallySurjective {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Functor Cᵒᵖ RingCat} {R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') {M₁ : PresheafOfModules R'} {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.