Documentation

Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

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

source
noncomputable def SheafOfModules.restrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R 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.
Instances For
    source
    @[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✝) :
    ((restrictScalars α).map φ).val = (PresheafOfModules.restrictScalars α.hom).map φ.val
    source
    @[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') :
    ((restrictScalars α).obj M').val = (PresheafOfModules.restrictScalars α.hom).obj M'.val
    source
    instance SheafOfModules.instAdditiveRestrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R R' : CategoryTheory.Sheaf J RingCat} (α : R ⟶ R') :
    (restrictScalars α).Additive
    source
    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₂) ≃ ((restrictScalars α).obj M₁ ⟶ (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.
    Instances For