Theorems · Theorem · category theory

ModuleCat.extendScalars_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₄),
  CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp (f₂₃.comp f₁₂) f₃₄).hom
      (CategoryTheory.Functor.whiskerRight (ModuleCat.extendScalarsComp f₁₂ f₂₃).hom (ModuleCat.extendScalars f₃₄)) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.extendScalarsComp f₁₂ (f₃₄.comp f₂₃)).hom
      (CategoryTheory.CategoryStruct.comp
        ((ModuleCat.extendScalars f₁₂).whiskerLeft (ModuleCat.extendScalarsComp f₂₃ f₃₄).hom)
        ((ModuleCat.extendScalars f₁₂).associator (ModuleCat.extendScalars f₂₃) (ModuleCat.extendScalars f₃₄)).inv)

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingCommRing