Quelle est la différence entre les flèches et les objets exponentiels dans une catégorie fermée cartésienne?

Dans une catégorie cartésienne ( CCC ), il existe les soi-disant objets exponentielles , écrit . Lorsqu'un CCC est considéré comme un modèle de simplement typé -calcul , un objet exponentielle comme caractérise l'espace de fonction à partir du type type . Un objet exponentiel est introduit par une flèche appelée et éliminé par une flèche appelée (qui malheureusement appeléλ B A A B c u r r y : ( A × B → C ) → ( A → C B$B^A$$\lambda$$B^A$$A$$B$$curry : (A \times B \rightarrow C) \rightarrow (A \rightarrow C^B)$e v a l C B B → $apply : C^B \times B \rightarrow C$$eval$dans la plupart des textes sur la théorie des catégories). Ma question est la suivante: y a-t-il une différence entre l'objet exponentiel et la flèche ?$C^B$$B \rightarrow C$

L'un est interne et l'autre externe .

Une catégorie est constituée d'objets et de morphismes. Quand nous écrivons f : A → B nous voulons dire que f est un morphisme de l' objet A à l' objet B . Nous pouvons collecter tous les morphismes de A à B en un ensemble de morphismes H o m C ( A , B ) , appelé "hom-set". Cet ensemble n'est pas un objet de C , mais plutôt un objet de la catégorie des ensembles.$\mathcal{C}$$f : A \to B$$f$$A$$B$$A$$B$ $\mathrm{Hom}_{\mathcal{C}}(A,B)$$\mathcal{C}$

En revanche, une exponentielle est un objet en C . C'est ainsi que " C pense à ses hom-sets". Ainsi, B A doit être équipé de quelle structure les objets de C ont.$B^A$$\mathcal{C}$$\mathcal{C}$$B^A$$\mathcal{C}$

À titre d'exemple, considérons la catégorie des espaces topologiques. Alors est une carte continue de X à Y , et H o m T o p ( X , Y ) est l'ensemble de toutes ces cartes continues. Mais Y X , s'il existe, est un espace topologique! Vous pouvez prouver que les points de Y X sont (en correspondance biunivoque avec) les cartes continues de X à Y . En fait, cela vaut en général: les morphismes 1 → B $f : X \to Y$$X$$Y$$\mathrm{Hom}_{\mathsf{Top}}(X,Y)$$Y^X$$Y^X$$X$$Y$$1 \to B^A$(qui sont "les points globaux de ") sont en correspondance bijective avec les morphismes A → B , car $B^A$$A \to B$

$$\mathrm{Hom}(1, B^A) \cong \mathrm{Hom}(1 \times A, B) \cong \mathrm{Hom}(A, B).$$

Parfois , nous obtenons bâclée sur l' écriture par rapport à A → B . En fait, souvent ces deux sont des synonymes, étant entendu que f : A → B pourrait signifier «oh au fait ici, je voulais dire l'autre notation, donc cela signifie que f est un morphisme de A à B ». Par exemple, lorsque vous avez noté le morphisme de curry curry : ( A × B → C ) → ( A → C B ), vous devriez vraiment avoir écrit curry$B^A$$A \to B$$f : A \to B$$f$$A$$B$

$$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$ Nous ne pouvons donc pas vraiment reprocher à quiconque de se confondre ici. L'intérieur → est utilisé au sens interne et l'extérieur à l'extérieur. $$\textit{curry}: C^{A \times B} \to {(C^B)}^A.$$ $\to$

$\lambda$$t$$B$$t : B$$B$$B$

$$\textit{curry}: (A \times B \to C) \to (A \to C^B)$$ $\lambda$ $$\textit{curry}: ((C^B)^A)^{C^{A \times B}}.$$ $B^A$$A \to B$