Aplicaciones de la Lawvere Teorema de Punto Fijo para los Conjuntos

Question

Yo no estoy familiarizado con el teorema general de cerrado, cartesiano categorías (como no estoy familiarizado con cerrado, cartesiano categorías), pero soy consciente de que esta versión del teorema de punto fijo para los conjuntos:

Deje $A, B$ ser conjuntos. Si existe un surjective función de $f: A \longrightarrow \textbf{Set}(A,B)$, entonces cada función $g:B \longrightarrow B$ tiene un punto fijo.

Soy consciente de dos aplicaciones del teorema: prueba del teorema de Cantor (ajuste $B=\{0,1\}$) y demostrando que $[0,1]$ es incontable (ajuste de $A=\mathbb{N}$, $B= \{0,1\}$, mirando representaciones binarias).

Hay otros limpio aplicaciones de este teorema de punto fijo para los juegos? Por ejemplo, podemos deducir la Tarski teorema de punto fijo para conjuntos (todos los no-decreciente endofunction de un juego de poder de un conjunto tiene un punto fijo) o el Cantor-Bernstein teorema de uso de este teorema?

Sólo pensé que este resultado fue genial, y quería ver qué otras cosas podría hacer con él. Gracias de antemano por las respuestas!

Answer 1

El Lawvere teorema de punto fijo tiene aplicaciones limitadas en $\text{Set}$ porque el único conjunto con el punto fijo de la propiedad es la de un elemento de conjunto $1$, por lo que si $B$ es cualquier otro conjunto que acaba de concluir que no puede haber un surjection $A \to [A, B]$, que para $B \neq 0, 1$ es, básicamente, el Cantor del teorema.

Tiene aplicaciones más interesantes en otros cartesiano categorías cerradas, precisamente, porque a veces estas categorías tienen más interesante objetos con el punto fijo de la propiedad. Por ejemplo, hay algunos cartesiano categorías cerradas que consta de un solo objeto $X$; en particular, esto significa que $X \cong [X, X]$, y la aplicación de la Lawvere teorema de punto fijo para un isomorfismo de esta forma le permite a la conclusión de que la $X$ tiene el punto fijo de la propiedad. Los ccc como este modelo el tipo cálculo lambda, y anotar los puntos fijos explícitamente le da la de Y combinator.