Theorems · Theorem · category theory

ModuleCat.localizedModuleMap_hom_apply

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

Defined in

Mathlib.Algebra.Category.ModuleCat.Localization

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingSmall