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.

Equations

• M.localizedModule S = ↧(Shrink.{?u.2, max ?u.2 ?u.1} (LocalizedModule S ↑M))

@[instance_reducible]

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)

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• M.localizedModuleMkLinearMap S = ↑(Shrink.linearEquiv R (LocalizedModule S ↑M)).symm ∘ₗ LocalizedModule.mkLinearMap S ↑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.

Equations

• One or more equations did not get rendered due to their size.

@[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.localizedModuleFunctor {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.

Equations

• ModuleCat.localizedModuleFunctor S = { obj := fun (M : ModuleCat R) => M.localizedModule S, map := fun {X Y : ModuleCat R} => ModuleCat.localizedModuleMap S, map_id := ⋯, map_comp := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

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

theorem ModuleCat.isIso_of_isLocalizedModule_comp {R : Type u} [CommRing R] {S : Submonoid R} {M₁ M₂ M₃ : ModuleCat R} {f₁ : M₁ ⟶ M₂} {f₂ : M₂ ⟶ M₃} (h₁ : IsLocalizedModule S (Hom.hom f₁)) (h₂ : IsLocalizedModule S (Hom.hom (CategoryTheory.CategoryStruct.comp f₁ f₂))) : CategoryTheory.IsIso f₂