Categorias como funções

Question

Estou trabalhando no livro de Teoria das Categorias para Programadores .

Aqui no livro eu encontro a relação "<=" como um exemplo de categoria: ela respeita a relação de identidade ( a <= a) e é combinável ( a <= b, b <= c -> a <= c).

O que não está claro para mim é a analogia entre morfismos e funções, conforme mencionado no livro na página 3: uma função não pode implementar a categoria de pedido, pois não pode retornar nenhum valor <= de um determinado, então ... o que é a relação entre morfismos e funções? Parece que os morfismos são conexões entre tipos, ao passo que as definições de funções são conexões entre valores, de modo que o último soa para mim como uma implementação especial do primeiro.

Isso estaria em contraste com todos os exemplos de funções de identidade que eu vi lá fora, embora, como uma função de identidade mapearia um tipo com o mesmo tipo, não um valor com o mesmo valor, então, por exemplo, f x = x + 1seria um correto " arrow "de e para o mesmo tipo, o que evidentemente não é verdade.

Por outro lado, porém, vejo essas representações de categoria:

Aqui, A é um tipo ou um objeto?

Answer 1

Não entendo muito bem por que você está confuso e, em particular, não entendo muito bem o que você entende por "uma função não pode implementar a categoria de pedido", então direi apenas algumas coisas que espero que sejam relevantes.

1. Os morfismos não começam como tendo qualquer interpretação particular em termos de funções. Os axiomas de categoria simples fornecem um monte de objetos e setas e axiomas de como as setas devem se compor, e esses axiomas são satisfeitos por qualquer ordem parcial $\le$, e é isso. Ao começar, acho que a maneira menos confusa de pensar sobre categorias dessa maneira "nua" é pensar nelas como gráficos direcionados equipados com uma operação de composição nas arestas.

2. Por outro lado, cada categoria $C$tem uma incorporação Yoneda $C \to [C^{op}, \text{Set}]$, o que nos dá uma interpretação distinta dos morfismos $f : x \to y$ como funções $f : \text{Hom}(a, x) \to \text{Hom}(a, y)$em pontos generalizados , onde um ponto generalizado de$x$ é qualquer morfismo $a \to x$qualquer. Isso nos permite interpretar os morfismos$x \le y$em uma ordem parcial como funções (necessariamente exclusivas) dos downsets $\{ a : a \le x \}$ para os downsets $\{ a : a \le y \}$, ou seja, a função única de envio $a$ para $a$.

3. Os objetos também não começam como tendo qualquer interpretação particular em termos de tipos. A teoria dos tipos é uma maneira particular de ver as categorias, ou uma maneira particular de gerá-las, e não é a única. Na semântica categórica padrão para teorias de tipo, os objetos são (interpretados como) tipos$A$ e morfismos $f : A \to B$ são (interpretadas como) funções com tipo de entrada $A$ e tipo de saída $B$. Se uma categoria tem um objeto terminal $1$ (que pode ser interpretado como um tipo de unidade), então morfismos $1 \to A$ podem ser interpretados como termos do tipo $A$, e um morfismo $f : A \to B$ então induz uma função genuína $\text{Hom}(1, A) \to \text{Hom}(1, B)$ enviando termos do tipo $A$ aos termos do tipo $B$. Muitas vezes não há "pontos" suficientes (funções$1 \to A$) para tornar esta operação interessante em muitas categorias; por exemplo, em posets$1$, se existe, é um elemento máximo , então$\text{Hom}(1, A)$ está vazio a menos que $A$ também é máximo.