¿Puede derivarse una versión general de la mónada covariante del conjunto de potencias a partir de la propiedad universal de los objetos de potencia?

Question

Como pide el título, me pregunto si en general se puede exprimir una "mónada covariante de objetos de potencia" de un topos (siguiendo el ejemplo habitual en $\mathcal{Set}$ con parte del functor el functor de imagen directa del conjunto de potencias), o si hay un buen contraejemplo que muestre por qué no.

Supongo que la respuesta a esto es negativa, ya que sólo veo que se hable de esta mónada en el caso de $\mathcal{Set}$ así que sospecho que depende de propiedades más especiales de esa categoría; en cuyo caso tengo curiosidad por saber qué propiedades especiales hacen que funcione.

Editar : En particular, entiendo la construcción habitual de la parte del functor, pero he sido incapaz de verificar que los candidatos obvios para la unidad y la multiplicación funcionan realmente como tales.

Answer 1

De hecho, la respuesta es sí. Las álgebras de la mónada son, por supuesto, los semilátices internos de unión completa.

Lo primero es lo primero: la unidad $\eta_X : X \to P X$ está dada por la transposición del morfismo $X \times X \to \Omega$ que clasifica la diagonal $\Delta : X \to X \times X$ . Para ver que es una transformación natural, lo más fácil es utilizar la lógica interna: dado $f : X \to Y$ queremos mostrar $$x : X \vdash \exists_f (\eta_X (x)) = \eta_Y (f (x))$$ que por "extensionalidad" equivale a $$x : X, y : Y \vdash y \in \exists_f (\eta_X (x)) \leftrightarrow y \in \eta_Y (f (x))$$ que por definición de $\exists_f$ equivale a $$x : X, y : Y \vdash (\exists x' : X . x' \in \eta_X (x) \land f (x') = y) \leftrightarrow y \in \eta_Y (f (x))$$ que por definición de $\eta$ equivale a $$x : X, y : Y \vdash (\exists x' : X . x' = x \land f (x') = y) \leftrightarrow y = f (x)$$ lo que obviamente es una tautología.

La multiplicación $\mu_X : P P X \to P X$ tiene una descripción sencilla en la lógica interna: $$\mu_X (t) = \left\{ x : X \mid \exists s : P X . s \in t \land x \in s \right\}$$ Si se despliega esto, equivale a decir que $\mu_X$ es la transposición del morfismo $P P X \times X \to \Omega$ que clasifica la imagen del compuesto $$R \rightarrowtail P P X \times P X \times X \to P P X \times X$$ donde la segunda flecha es la proyección obvia y la primera flecha está definida por el siguiente diagrama de retroceso, $$\require{AMScd} \begin{CD} R @>>> [\ni] \times [\ni] \\ @VVV @VVV \\ P P X \times P X \times X @>>{\mathrm{id} \times \Delta \times \mathrm{id}}> P P X \times P X \times P X \times X \end{CD}$$ donde $[\ni] \rightarrowtail P P X \times P X$ y $[\ni] \rightarrowtail P X \times X$ son las relaciones binarias universales. Por supuesto, sería una pesadilla verificar que $\mu_X$ definida de esta manera es natural en $X$ Por lo tanto, es mejor atenerse a la descripción en la lógica interna. Dejo la verificación a usted - la naturalidad equivale a decir que $\exists$ se desplaza con $\exists$ .

Queda por demostrar que $\eta$ y $\mu$ satisfacen los axiomas de la mónada. No hace falta decir que la mejor manera de proceder es utilizar la lógica interna.

• El axioma de la unidad izquierda es bastante fácil: se traduce en $$s : P X \vdash \mu_X (\eta_{P X} (s)) = s$$ lo que equivale a $$s : P X, x : X \vdash x \in \mu_X (\eta_{P X} (s)) \leftrightarrow x \in s$$ que se amplía a $$s : P X, x : X \vdash (\exists s' : P X . s' \in \eta_{P X} (s) \land x \in s') \leftrightarrow x \in s$$ que se amplía a $$s : P X, x : X \vdash (\exists s' : P X . s' = s \land x \in s') \leftrightarrow x \in s$$ que es una tautología.
• El axioma de la unidad derecha es más complicado: se traduce en $$s : P X \vdash \mu_X (\exists_{\eta_X} (s)) = s$$ lo que equivale a $$s : P X, x : X \vdash x \in \mu_X (\exists_{\eta_X} (s)) \leftrightarrow x \in s$$ que se expande a $$s : P X, x : X \vdash (\exists s' : P X . s' \in \exists_{\eta_X} (s) \land x \in s') \leftrightarrow x \in s$$ que se expande a $$s : P X, x : X \vdash (\exists s' : P X . \exists x' : X . x' \in s \land \eta_X (x') = s' \land x \in s') \leftrightarrow x \in s$$ lo que equivale a $$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x \in \eta_X (x')) \leftrightarrow x \in s$$ que se amplía a $$s : P X, x : X \vdash (\exists x' : X . x' \in s \land x = x') \leftrightarrow x \in s$$ que es una tautología.
• El axioma de asociatividad es aún más complicado de escribir, pero sigue siendo sencillo: equivale a la asociatividad de $\exists$ .