Theorems · Theorem · category theory

ModuleCat.ihom_ev_app

∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
  (CategoryTheory.ihom.ev M).app N =
    ModuleCat.ofHom
      ((TensorProduct.uncurry (RingHom.id R) ↑M ↑(M ⟹ N) ↑N)
        (LinearMap.lcomp R ↑N ↑ModuleCat.homLinearEquiv ∘ₗ LinearMap.id.flip))

Describes the counit of the adjunction M ⊗ - ⊣ Hom(M, -). Given an R-module N this should give a map M ⊗ Hom(M, N) ⟶ N, so we flip the order of the arguments in the identity map Hom(M, N) ⟶ (M ⟶ N) and uncurry the resulting map M ⟶ Hom(M, N) ⟶ N.

Defined in

Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing