Theorems · Definition · category theory

ModuleCat.localizedModuleFunctor

{R : Type u} →
  [inst : CommRing R] →
    [Small.{v, u} R] → (S : Submonoid R) → CategoryTheory.Functor (ModuleCat R) (ModuleCat (Localization S))

The functor ModuleCat.{v} R ⥤ ModuleCat.{v} (Localization S) sending M to M.localizedModule S and f : M1 ⟶ M2 to IsLocalizedModule.mapExtendScalars S _ _ (Localization S) f.hom.

Defined in

Mathlib.Algebra.Category.ModuleCat.Localization

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommRingSmall