Theorems · Theorem · category theory

ModuleCat.extendScalars_assoc_assoc

∀ {R₁ R₂ R₃ R₄ : Type u₁} [inst : CommRing R₁] [inst_1 : CommRing R₂] [inst_2 : CommRing R₃] [inst_3 : CommRing R₄]
  (f₁₂ : R₁ →+* R₂) (f₂₃ : R₂ →+* R₃) (f₃₄ : R₃ →+* R₄) {Z : CategoryTheory.Functor (ModuleCat R₁) (ModuleCat R₄)}
  (h : ((ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)).comp (ModuleCat.extendScalars f₃₄) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp f₁₂ f₂₃).hom (ModuleCat.extendScalars f₃₄))
        h) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsComp f₂₃ f₃₄).hom)
        (CategoryTheory.CategoryStruct.comp
          ((ModuleCat.extendScalars f₁₂).associator (ModuleCat.extendScalars f₂₃) (ModuleCat.extendScalars f₃₄)).inv h))

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRing