ModuleCat.ihom_coev_app
theorem ModuleCat.ihom_coev_app :
∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
(CategoryTheory.ihom.coev M).app N =
(TensorProduct.mk R ↑(Opposite.op M).unop ↑((CategoryTheory.Functor.id (ModuleCat R)).obj N)).flip
This theorem describes the unit of an adjunction in the category of modules over a ring `R`. The adjunction pairs the tensor product functor `M ⊗ -` with the Hom functor `Hom(M, -)`. For every `R`-module `N`, this theorem establishes a map `N ⟶ Hom(M, M ⊗ N)`. This map is derived from flipping the arguments in the natural `R`-bilinear map `M ⟶ N ⟶ M ⊗ N`. That is, for given modules `M` and `N`, the application of the coevaluation map on `N` is equal to the flipped version of the canonical bilinear map applied to the opposite of `M` and the identity functor applied to `N`.
More concisely: The coevaluation map from an `R`-module `N` to the Hom set `Hom(M, M ⊗ N)` is equal to the flipped version of the canonical `R`-bilinear map from `M` to `M ⊗ N`, where `M` is an `R`-module.
|
ModuleCat.ihom_ev_app
theorem ModuleCat.ihom_ev_app :
∀ {R : Type u} [inst : CommRing R] (M N : ModuleCat R),
(CategoryTheory.ihom.ev M).app N = (TensorProduct.uncurry R (↑M) (↑M →ₗ[R] ↑N) ↑N) LinearMap.id.flip
This theorem describes the counit of the adjunction `M ⊗ - ⊣ Hom(M, -)` in the category of modules over a commutative ring `R`. Given modules `M` and `N` over `R`, it specifies a map from the tensor product of `M` and the set of linear maps from `M` to `N` to `N`. This map is constructed by flipping the order of arguments in the identity map from the set of linear maps from `M` to `N` to a function from `M` to `N`, and then uncurrying the resulting function from `M` to a function from the set of linear maps from `M` to `N` to `N`.
More concisely: The theorem asserts that the adjunction unit of `M ⊗ - ⊣ Hom(M, -)` in the category of `R`-modules is given by the natural transformation from `M ⊗ Hom(M, N)` to `N` obtained by flipping the order of arguments in the identity map from `Hom(M, N)` to `M → N` and then uncurrying.
|