Theorems · Definition · category theory

ModuleCat.ExtendRestrictScalarsAdj.Counit.map

{R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) → {Y : ModuleCat S} → ((ModuleCat.restrictScalars f).comp (ModuleCat.extendScalars f)).obj Y ⟶ Y

For any S-module Y, there is a natural R-linear map from S ⨂ Y to Y by s ⊗ y ↦ s • y

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRing