Theorems · Definition · category theory

ModuleCat.extendScalarsComp

{R₁ R₂ R₃ : Type u₁} →
  [inst : CommRing R₁] →
    [inst_1 : CommRing R₂] →
      [inst_2 : CommRing R₃] →
        (f₁₂ : R₁ →+* R₂) →
          (f₂₃ : R₂ →+* R₃) →
            ModuleCat.extendScalars (f₂₃.comp f₁₂) ≅ (ModuleCat.extendScalars f₁₂).comp (ModuleCat.extendScalars f₂₃)

The extension of scalars by a composition of commutative ring morphisms identifies to the composition of the extension of scalars functors.

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRing