Theorems · Definition · category theory

ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars

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

Given R-module X and S-module Y and a map X ⟶ (restrictScalars f).obj Y, i.e R-linear map X ⟶ Y, there is a map (extend_scalars f).obj X ⟶ Y, i.e S-linear map S ⨂ X → Y by s ⊗ x ↦ s • g x.

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRing