ModuleCat.isLocalizedModuleAway_restrictScalars
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open CategoryTheory
namespace ModuleCatLean source · statement
theorem isLocalizedModuleAway_restrictScalars (R A : CommRingCat.{u}) (σ : R →+* A)
(M N : ModuleCat.{v} A) (f : M ⟶ N) (r : R)
[IsLocalizedModule (Submonoid.powers (σ r)) f.hom] :
IsLocalizedModule (Submonoid.powers r) ((ModuleCat.restrictScalars σ).map f).hom