Theorems · Definition · category theory

ModuleCat.coextendScalars

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

For any rings R, S and a ring homomorphism f : R →+* S, there is a functor from R-module to S-module defined by M ↦ (S →ₗ[R] M) where S is considered as an R-module via restriction of scalars and g : M ⟶ M' is sent to h ↦ g ∘ h. The definition of (coextendScalars f).obj is given by CoextendScalars.equiv.

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

8 results in Mathlib

Foundations

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

Assumes

RingRing