Internal homs of modules over an internal monoid #
Let A be a monoid object in a closed monoidal category C with equalizers. For left
A-modules M and N, the object Hom_A(M, N) of A-linear maps is the equalizer of the two
maps [M, N] ⇉ [A ⊗ M, N] of internal homs given by precomposition with the action on M and by
postcomposition with the action on N. Tensoring a module on the right with an object of C,
K ↦ M ⊗ K with A acting on M, is left adjoint to Hom_A(M, -): module maps M ⊗ K ⟶ N
are the maps K ⟶ Hom_A(M, N). No braiding is needed for this.
When C is braided and A is commutative, Hom_A(M, N) is itself a left A-module, with
(a • f) m = f (a • m), and module maps act on it by postcomposition. The action is built from the
right action m ⊗ a ↦ a • m of the canonical bimodule Mod.toBimod.obj M. This is the internal hom
Mod.internalHom M of left A-modules. For symmetric spectra, the modules over the commutative
sphere monoid of symmetric sequences, it is the function spectrum.
Main definitions #
Mod.tensorLeft M: the functorK ↦ M ⊗ KfromCto leftA-modules.Mod.tensorRight K: the functorM ↦ M ⊗ Kon leftA-modules.Mod.ihom M: the functorN ↦ Hom_A(M, N)from leftA-modules toC, with the inclusionMod.ihomι M N : Hom_A(M, N) ⟶ [M, N]and the factorizationMod.ihomLift.Mod.ihomAdjunction M : Mod.tensorLeft M ⊣ Mod.ihom M.Mod.internalHom M: over a commutative monoid,Hom_A(M, -)as a functor of leftA-modules.
References #
- M. Hovey, B. Shipley and J. Smith, Symmetric spectra, J. Amer. Math. Soc. 13 (2000), Section 2.2.
With A acting on the left factor, M ⊗ K is a left A-module. For M = A this is the
free module TauCeti.freeModObj A K, which is stated directly with the multiplication of A so
that free modules have the literal carriers A ⊗ K.
Instances For
Tensoring a left A-module M on the right: K ↦ M ⊗ K, with A acting on M.
Instances For
The action on M ⊗ K is the action on M.
Tensor a module on the right by an object, retaining its action on the left factor.
Instances For
Tensoring a module with the unit object gives back the module: the right unitor
M ⊗ 𝟙 ≅ M is A-linear.
Instances For
The isomorphism M ⊗ 𝟙 ≅ M is the right unitor.
The inverse of the isomorphism M ⊗ 𝟙 ≅ M is the inverse right unitor.
The object Hom_A(M, -) of A-linear maps out of a left A-module M. Its value at N
is the equalizer of precomposition with the action on M and postcomposition with the action
on N, as maps [M, N] ⇉ [A ⊗ M, N] of internal homs.
Instances For
The inclusion Hom_A(M, N) ⟶ [M, N] of A-linear maps into all maps.
Instances For
Maps into Hom_A(M, N) are determined by their composites with the inclusion into
[M, N].
The inclusion of A-linear maps is natural in the target module.
The inclusion of A-linear maps is natural in the target module.
A map K ⟶ [M, N] whose uncurried form M ⊗ K ⟶ N is A-linear factors through
Hom_A(M, N).
Instances For
The factorization through Hom_A(M, N) recovers the given map.
The factorization through Hom_A(M, N) recovers the given map.
The uncurried inclusion M ⊗ Hom_A(M, N) ⟶ N, evaluation of A-linear maps, is
A-linear.
The uncurried inclusion M ⊗ Hom_A(M, N) ⟶ N, evaluation of A-linear maps, is
A-linear.
Module maps M ⊗ K ⟶ N correspond to maps K ⟶ Hom_A(M, N) by currying.
Instances For
Currying a module map M ⊗ K ⟶ N into Hom_A(M, N), followed by the inclusion into
[M, N], is the ordinary currying.
Currying a module map M ⊗ K ⟶ N into Hom_A(M, N), followed by the inclusion into
[M, N], is the ordinary currying.
The inverse bijection uncurries a map K ⟶ Hom_A(M, N).
The adjunction M ⊗ - ⊣ Hom_A(M, -) between C and left A-modules.
Instances For
The bijection of the adjunction M ⊗ - ⊣ Hom_A(M, -) is given by currying.
The counit of the adjunction M ⊗ - ⊣ Hom_A(M, -) evaluates A-linear maps.
Over a commutative monoid A, the object Hom_A(M, N) of A-linear maps is a left
A-module, with (a • f) m = f (a • m).
Instances For
The internal hom of left modules over a commutative monoid A: Hom_A(M, N), the object of
A-linear maps, with A acting through its action on M.
Instances For
The action of A on Hom_A(M, N) is precomposition with the action on M:
(a • f) m = f (a • m).
The action of A on Hom_A(M, N) is precomposition with the action on M:
(a • f) m = f (a • m).