Localized Module in ModuleCat

For a ring R satisfying [Small.{v} R] and a submonoid S of R, this file defines an exact functor ModuleCat.{v} R ⥤ ModuleCat.{v} (Localization S), see ModuleCat.localizedModuleFunctor.

theorem instSmallLocalizedModule (R : Type u) [CommRing R] [Small.{v, u} R] (M : Type v) [AddCommGroup M] [Module R M] (S : Submonoid R) : Small.{v, max v u} (LocalizedModule S M)

noncomputable def ModuleCat.localizedModule {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R) : ModuleCat (Localization S)

Shrink of LocalizedModule S M in category which M belongs.

noncomputable instance ModuleCat.instModuleCarrierLocalizationLocalizedModule {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R) : Module R ↑(M.localizedModule S)

The R module structure on M.localizedModule S given by the R module structure on Shrink.{v} (LocalizedModule S M)

instance ModuleCat.instIsScalarTowerLocalizationCarrierLocalizedModule {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R) : IsScalarTower R (Localization S) ↑(M.localizedModule S)

noncomputable def ModuleCat.localizedModuleMkLinearMap {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R) : ↑M →ₗ[R] ↑(M.localizedModule S)

The linear map M →ₗ[R] (M.localizedModule S) which exhibits M.localizedModule S as a localized module of M.

instance ModuleCat.localizedModule_isLocalizedModule {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) (S : Submonoid R) : IsLocalizedModule S (M.localizedModuleMkLinearMap S)

noncomputable def ModuleCat.localizedModuleMap {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} (S : Submonoid R) (f : M ⟶ N) : M.localizedModule S ⟶ N.localizedModule S

IsLocalizedModule.mapExtendScalars as a morphism in ModuleCat.

@[simp]

theorem ModuleCat.localizedModuleMap_hom_apply {R : Type u} [CommRing R] [Small.{v, u} R] {M N : ModuleCat R} (S : Submonoid R) (f : M ⟶ N) (a : ↑(M.localizedModule S)) : (Hom.hom (localizedModuleMap S f)) a = ((IsLocalizedModule.map S (M.localizedModuleMkLinearMap S) (N.localizedModuleMkLinearMap S)) (Hom.hom f)) a

noncomputable def ModuleCat.localizedModule_functor {R : Type u} [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.

@[simp]

theorem ModuleCat.localizedModule_functor_obj {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) (M : ModuleCat R) : (localizedModule_functor S).obj M = M.localizedModule S

@[simp]

theorem ModuleCat.localizedModule_functor_map {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) {X✝ Y✝ : ModuleCat R} (f : X✝ ⟶ Y✝) : (localizedModule_functor S).map f = localizedModuleMap S f

instance ModuleCat.instAdditiveLocalizationLocalizedModule_functor {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : (localizedModule_functor S).Additive

theorem ModuleCat.localizedModule_functor_map_exact {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) (T : CategoryTheory.ShortComplex (ModuleCat R)) (h : T.Exact) : (T.map (localizedModule_functor S)).Exact

instance ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModule_functor {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : CategoryTheory.Limits.PreservesFiniteLimits (localizedModule_functor S)

instance ModuleCat.instPreservesFiniteColimitsLocalizationLocalizedModule_functor {R : Type u} [CommRing R] [Small.{v, u} R] (S : Submonoid R) : CategoryTheory.Limits.PreservesFiniteColimits (localizedModule_functor S)