Equivalência entre duas definições de uma categoria com objetos exponenciais

Question

Uma categoria com produtos é considerada exponencial para todos os objetos$x, y$ existe um objeto $y^x$ equipado com uma flecha $e\colon x\times y^x\to y$ de modo que para todos os objetos $z$ e todas as flechas $f\colon x\times z\to y$ existe uma flecha única $\bar{f}\colon z\to y^x$ satisfatório $e\circ (id_x\times\bar{f})=f$.

Eu vejo que se uma categoria tem exponenciais, então $f\mapsto \bar{f}$ é um isomorfismo natural entre $hom(x\times z, y)$ e $hom(z, y^x)$ com inverso $\bar{f}\mapsto id_x\times\bar{f}$. Daí o functor$x\times (-)$ é deixado adjacente a $(-)^x$.

Estou me perguntando sobre o contrário: se $C$ é uma categoria com produtos tais que $x\times (-)$ tem um adjunto certo, segue-se que $C$ tem exponenciais?

Em particular, se apenas assumirmos que $x\times (-)$ tem um adjunto certo, como equipamos $y^x$ com a flecha $e\colon x\times y^x\to y$. Além disso, como podemos deduzir que a equação$e\circ (id_x\times\bar{f})=f$ segura precisamente?

De alguma forma, a existência de um adjunto certo de $x\times (-)$ parece mais fraco e mais abstrato do que a definição de propriedade universal de uma categoria com exponenciais dados acima.

Answer 1

Suponho que seja necessário AC para escolher um objeto $y^x$ para cada $x$ e $y$.

Aceitando isso, recebe a flecha $e$do formalismo de unidades / contagens em adjuntos. E se$F$ é um adjunto certo de $x\times(-)$ então naturalmente, $$\text{hom}(a,Fy)\cong\text{hom}(x\times a,y).$$ Levar $a=Fy$. Então$$\text{hom}(Fy,Fy)\cong\text{hom}(x\times Fy,y).$$ A identidade à esquerda mapeia para um homomorfismo $e:x\times Fy\to y$a direita. Estamos denotando$Fy$ Como $y^x$, e isto $e:x\times y^x\to y$ é o mapa exponencial.