В чем разница между стрелками и экспоненциальными объектами в декартовой замкнутой категории?

В декартовой Закрытой категории ( КТС ), существуют так называемые показательные объекты , написанных . Когда КТС рассматривается как модель просто-типизированных -исчисления , экспоненциальный объект как характеризует функциональное пространство от типа к типу . Экспоненциальный объект вводится стрелкой с именем и удаляется с помощью стрелки, называемой (которая, к сожалению, называетсяλ B A A B c u r r y : ( A × B → C ) → ( A → C B ) a p p l y : C B × B → C e v a $B^A$$\lambda$$B^A$$A$$B$$curry : (A \times B \rightarrow C) \rightarrow (A \rightarrow C^B)$$apply : C^B \times B \rightarrow C$$eval$в большинстве текстов по теории категорий). Мои вопросы здесь: есть ли разница между экспоненциальным объектом и стрелкой ? B → $C^B$$B \rightarrow C$

Один является внутренним, а другой - внешним .

Категория состоит из объектов и морфизмов. Когда мы пишем мы имеем в виду , что есть морфизм из объекта к объекту . Мы можем собрать все морфизмы из в в набор морфизмов , называемый "множеством гомов". Этот набор не является объектом , а является объектом категории наборов. f : A → B f A B A $\mathcal{C}$$f : A \to B$$f$$A$$B$$A$$B$ $\mathrm{Hom}_{\mathcal{C}}(A,B)$$\mathcal{C}$

Напротив, экспонента является объектом в . Вот как думает о своих гом-множествах. Таким образом, должен быть снабжен любой структурой, которую имеют объекты .C C B A $B^A$$\mathcal{C}$$\mathcal{C}$$B^A$$\mathcal{C}$

В качестве примера рассмотрим категорию топологических пространств. Тогда является непрерывным отображением из в , а является множеством всех таких непрерывных отображений. Но , если он существует, является топологическим пространством! Вы можете доказать , что точки есть (во взаимно однозначном соответствии с) непрерывных отображений из в . На самом деле это в общем случае: морфизмы (которые являются «глобальными точками ») находятся в биективном соответствии с морфизмами , потому что X Y H o m T o p ( X , Y ) Y X Y X X Y 1 → B A B A A → B H o m ( 1 , B A ) ≅ H o m ( 1 × A , B ) ≅ H o m ( A , $f : X \to Y$$X$$Y$$\mathrm{Hom}_{\mathsf{Top}}(X,Y)$$Y^X$$Y^X$$X$$Y$$1 \to B^A$$B^A$$A \to B$

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

Иногда мы получаем неаккуратно о написании , в отличие от . Фактически, часто эти два являются синонимами, с пониманием, что может означать «о, кстати, здесь я имел в виду другие обозначения, так что это означает, что является морфизмом от к ». Например, когда вы записали морфизм карри вы действительно должны были написать Поэтому мы не можем никого обвинять в том, что мы здесь запутались. Внутренний используется во внутреннем смысле, а внешний - во внешнем. → Б е : → Б е B карри : ( × B → C ) → ( → С Б ) Карри : C A × B → ( C B ) A . $B^A$$A \to B$$f : A \to B$$f$$A$$B$

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

Если мы работаем в простом наборе -calculus, то все, так сказать, внутреннее. У нас есть только базовое решение набрав « имеет тип », написанный , как . Поскольку здесь является типом, а типы соответствуют объектам, то мы явно должны интерпретировать любые экспоненты и стрелки в во внутреннем смысле. Итак, если мы понимаем как типовое суждение в -calculus, все стрелки являются внутренними, так что это так же, как Я надеюсь, что теперь понятно, почему люди используют$\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$