Theorems · Definition · category theory

ModuleCat.CoextendScalars.equiv

{R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : ModuleCat R) →
            ↑((ModuleCat.coextendScalars f).obj M) ≃ₗ[S]
              ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] ↑M

The carrier of (coextendScalars f).obj M is S →ₗ[R] M where S is considered as an R-module via restriction of scalars.

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

7 results in Mathlib

Foundations

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

Assumes

RingRing