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

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
    @[simp]

    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

      The isomorphism restrictScalars α ⋙ toPresheaf R ≅ toPresheaf R' for any morphism of presheaves of rings α : R ⟶ R'.

      Equations
      Instances For