Theorems · Definition · category theory

SheafOfModules.restrictScalars

{C : Type u'} →
  [inst : 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'.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings

Cited by

2 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category