Theorems · Definition · category theory

ModuleCat.restrictScalarsComp

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

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

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

4 results in Mathlib

Foundations

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

Assumes

RingRingRing