nLab evaluation map



Monoidal categories

monoidal categories

With braiding

With duals for objects

With duals for morphisms

With traces

Closed structure

Special sorts of products



Internal monoids



In higher category theory

Mapping space



Let (π’ž,βŠ—,πŸ™)\big(\mathcal{C}, \otimes, \mathbb{1}\big) be a closed monoidal category. For S,D∈CS, D \in C two objects, with internal hom [S,-][S, \text{-}] right adjoint to the tensor product SβŠ—(-)S \otimes (\text{-}), the evaluation map

ev:SβŠ—[S,D]β†’D ev \;\colon\; S \otimes [S, D] \to D

is the counit of this adjunction, hence the adjunct of the identity morphism

Id:[S,D]β†’[S,D]. Id \;\colon\; [S,D] \to [S,D] \,.

Concretely for π’ž\mathcal{C} = Sets or generally on generalized elements, the evaluation map is given by evaluating a function at a value, whence the name:

SΓ—[S,D] ⟢ev D (s,f) ↦ f(s). \array{ S \times [S,D] &\overset{ev}{\longrightarrow}& D \\ \big( s ,\, f \big) &\mapsto& f(s) \mathrlap{\,.} }

If π’ž\mathcal{C} is moreover compact then for D=πŸ™D = \mathbb{1} the tensor unit we have that [S,πŸ™]=S *[S, \mathbb{1}] \,=\, S^\ast is the dual object to SS, whence the evaluation map becomes the pairing of objects with their duals

SβŠ—S *⟢evπŸ™. S \otimes S^\ast \overset{ev}{\longrightarrow} \mathbb{1} \,.

Therefore, sometimes the pairing map on dual objects may be called β€œevaluation” even when the ambient category is not compact closed.


Syntax and semantics

In a cartesian closed category the evaluation map

[X,Y]×X→evalY [X,Y]\times X \stackrel{eval}{\to} Y

is the categorical semantics of what in the type theory internal language is the dependent type whose syntax is

f:Xβ†’Y,x:X⊒f(x):Y f \colon X \to Y ,\; x \colon X \; \vdash \; f(x) \colon Y

expressing function application. On propositions ((-1)-truncated types) this is the modus ponens deduction rule.

See also

Last revised on September 10, 2023 at 13:36:43. See the history of this page for a list of all contributions to it.