Theorems · Theorem · category theory

ModuleCat.extendRestrictScalarsAdj_homEquiv_apply

∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {M : ModuleCat R}
  {N : ModuleCat S} (φ : (ModuleCat.extendScalars f).obj M ⟶ N) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom (((ModuleCat.extendRestrictScalarsAdj f).homEquiv M N) φ)) m =
    (CategoryTheory.ConcreteCategory.hom φ) (1 ⊗ₜ[R] m)

Defined in

Mathlib.Algebra.Category.ModuleCat.ChangeOfRings

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingCommRing