Theorems · Definition · category theory

AlgCat.restrictScalars

{R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → CategoryTheory.Functor (AlgCat S) (AlgCat R)

The restriction of scalars functor AlgCat S ⥤ AlgCat R induced by a ring homomorphism R →+* S.

Defined in

Mathlib.Algebra.Category.AlgCat.Basic

Cited by

10 results in Mathlib

Foundations

Depth 31 from the axioms · uses propext, Quot.sound

Assumes

CommRingCommRing