Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings

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

source
@[simp]
theorem PresheafOfModules.restrictScalarsBundledCore_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'.restrictScalarsBundledCore α).map f) a = (M'.map f) a
source
@[simp]
theorem PresheafOfModules.restrictScalarsBundledCore_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'.restrictScalarsBundledCore α).obj X = (ModuleCat.restrictScalars (α.app X)).obj (M'.obj X)
source
noncomputable def PresheafOfModules.restrictScalarsBundledCore {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {R' : CategoryTheory.Functor Cᵒᵖ RingCat} (M' : PresheafOfModules R') (α : R ⟶ R') :
BundledCorePresheafOfModules 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
    source
    @[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'.restrictScalarsBundledCore α).toPresheafOfModules
    source
    @[simp]
    theorem PresheafOfModules.restrictScalars_map_hom {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') {M₁' : PresheafOfModules R'} {M₂' : PresheafOfModules R'} (φ : M₁' ⟶ M₂') :
    ((PresheafOfModules.restrictScalars α).map φ).hom = φ.hom
    source
    noncomputable def PresheafOfModules.restrictScalars {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {R' : CategoryTheory.Functor Cᵒᵖ RingCat} (α : R ⟶ R') :
    CategoryTheory.Functor (PresheafOfModules R') (PresheafOfModules 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
      source
      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
      • ⋯ = ⋯
      source
      instance PresheafOfModules.instFullRestrictScalarsIdFunctorOppositeRingCat {C : Type u'} [CategoryTheory.Category.{v', u'} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} :
      (PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R)).Full
      Equations
      • ⋯ = ⋯
      source
      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
      • ⋯ = ⋯