Theorems · Definition · category theory

ModuleCat.restrictScalars

{R : Type u₁} →
  {S : Type u₂} → [inst : Ring R] → [inst_1 : Ring S] → (R →+* S) → CategoryTheory.Functor (ModuleCat S) (ModuleCat R)

The restriction of scalars operation is functorial. For any f : R →+* S a ring homomorphism, * an S-module M can be considered as R-module by r • m = f r • m * an S-linear map is also R-linear

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

148 results in Mathlib

Foundations

Depth 32 from the axioms, rests on 292 definitions · uses propext, Quot.sound

Assumes

RingRing