Theorems · Theorem · category theory

ModuleCat.homEquiv_extendScalarsComp

∀ {R₁ R₂ R₃ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] (f₁₂ : R₁ →+* R₂)
  (f₂₃ : R₂ →+* R₃) (M : ModuleCat R₁),
  ((ModuleCat.extendRestrictScalarsAdj (f₂₃.comp f₁₂)).homEquiv M
        (((ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)).obj M))
      ((ModuleCat.extendScalarsComp f₁₂ f₂₃).hom.app M) =
    CategoryTheory.CategoryStruct.comp ((ModuleCat.extendRestrictScalarsAdj f₁₂).unit.app M)
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.restrictScalars f₁₂).map
          ((ModuleCat.extendRestrictScalarsAdj f₂₃).unit.app (ModuleCat.ExtendScalars.obj' f₁₂ M)))
        ((ModuleCat.restrictScalarsComp f₁₂ f₂₃).inv.app
          ((ModuleCat.extendScalars f₂₃).obj (ModuleCat.ExtendScalars.obj' f₁₂ M))))

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRing