Aggiunzioni di Sub(f), iperdottrine del primo ordine

[antizanzare]

Ciao, sto cercando, piano piano e se possibile anche con più calma, di studiare l'iperdottrina dei sottoggetti di un topos elementare.

Riporto la definizione di iperdottrina che al momento utilizzo:Un'iperdottrina (del primo ordine) è un funtore $p: \mathcal{C}^{op} \to$ Heyt, dove $\mathcal{C}$ è una categoria cartesiana e Heyt categoria che ha come oggetti le algebre di Heyting, tale che per ogni $f: A \to B$ in $\mathcal{C}$, la freccia $p(f): p(B) \to p(A)$ abbia un aggiunto destro $\forall_f$ e un aggiunto sinistro $\exists_f$ che soddisfi la condizione di Beck-Chevalley.
In particolare voglio verificare che

$ \text{Sub}: \mathcal{C}^{op} \to $ Set

con $\mathcal{C}$ topos elementare, può essere visto come un'iperdottrina del primo ordine.
Dopo aver verificato che $\text{Sub}_\mathcal{C}(A)$ può essere dotato della struttura di algebra di Heyting $\forall A \in \text{Ogg}(\mathcal{C})$, perciò $\text{Sub}: \mathcal{C}^{op} \to $Heyt, vanno verificate le condizioni sugli aggiunti.
Per individuare l'aggiunzione sinistra, ricordiamo che, presa $f : B \to A$, vale che \( \exists_f \dashv \text{Sub}_\mathcal{C}(f) \) se e solo se ho un'aggiunzione \( \text{Hom}(\exists_f (j), i) \to \text{Hom}(j, \text{Sub}_\mathcal{C}(f)(i)) \) ovvero se è vero che, per $j: J \to B$, $i: I \to A$ monomorfismi, \(j \leq_B f^*(i) \) se e solo se \(\exists_f (j) \leq_A i\). Questo vale nelle categorie regolari, quindi segue l'esistenza dell'aggiunto sinistro.

Il problema lo incontro quando invece cerco di trovare un aggiunto destro. Le dispense tracciano la seguente strada.
Osservare che se conosco gli aggiunti destri $\forall_{\pi_2}$ delle frecce $\pi_2: B \times A \to A$, allora si può verificare che per ogni $f : B \to A$ si ha $\forall_{\pi_2}(\text{Sub}_\mathcal{C}(f \times \text{id}_A)(\exists_{\Delta_A}(\top)) \to \text{Sub}_\mathcal{C}(\pi_1)(j))$ è aggiunto destro di $\text{Sub}_\mathcal{C}(f)$. Dopodichè viene fatto vedere che definendo $\forall_{\pi_2}$ in modo che $\forall_{\pi_2}(i)$ sia il pullback di \(\lceil \text{true} \circ !_{1 \times B} \rceil\) lungo \(\lceil \chi_i \circ \langle \pi_2, \pi_1 \rangle \rceil\).

Ora, io posso pure verificare che queste definizioni mi verifichino le condizioni di aggiunzioni (e non è nemmeno così semplice, halp), ma il tutto resta per me gibberish: continuo a non capire chi sia questo aggiunto nè saprei ritrovarlo autonomamente.
Dunque ... se avete idea di come capire che cos'è $\forall_f$ in un modo che sia un filo meno simile ad una apparizione miracolosa, vi ringrazio.

[megas_archon]

Siccome adesso ho capito cosa vuoi, lo riscrivo: una volta che sai come trovare \(\forall_\pi\) per ogni proiezione, puoi trovare \(\forall_f\) con quel trucco (e questo è un fatto fondamentale delle iperdottrine), cioè \(f^*\dashv \forall_{\pi_2}\big((f\times 1)^*\exists_\Delta 1\Rightarrow \pi_1^*(-)\big)\). La dimostrazione è un po' god given, nel senso che fai questa cosa e controlli che funzioni, e per unicità degli aggiunti \(\text{sleppa}=\forall_f\). Che \(f^*U\le V\iff U\le \text{sleppa}(V)\) si mostra con l'aggiunzione tra le varie mappe, con Beck-Cavallo e con un po' di olio di bestemmie. Inizia così:
\[U\le \text{sleppa}(V)=\forall_{\pi_2}\big((f\times 1)^*\exists_\Delta 1\Rightarrow \pi_1^*V\big)\iff
\pi_2^*U \land ((f\times 1)^*\exists_\Delta 1) \le \pi_1^*V\iff\dots\](ho il dubbio ti serva anche la reciprocità di Frobenius qua)

Ora. Tu vuoi una manifestazione del principio generale per cui questo aggiunto si trova così. Si può fare, ma si paga il prezzo di dover usare più category theory, non meno (devi sapere cosa sono schifezze come una "estensione di Kan" e una "coend"), quindi non credo ti convenga.

[antizanzare]

Intanto grazie e no, almeno per un po' voglio che le estensioni di kan restino un nome buffo per il mio cervellino.

Dopodichè, per i posteri, la dimostrazione dovrebbe essere una cosa del tipo:
\[ U\le_{A} \forall_{\pi_2}\big((f\times \text{id}_A)^*\exists_\Delta 1\Rightarrow \pi_1^*V\big) \iff \pi_2^*U \land ((f\times \text{id}_A)^*\exists_\Delta 1) \le_{B \times A} \pi_1^*V \] Preso il diagramma di pullback
\[
\begin{array}[c]{ccc}
B&\stackrel{id_B, f}{\longrightarrow}&B \times A\\
\big\downarrow\scriptstyle{f}&&\big\downarrow\scriptstyle{f \times id_A}\\
A&\stackrel{\Delta_A}{\longrightarrow}&A \times A
\end{array}
\]
per la condizione di Beck-Chevalley avrò la commutatività del seguente diagramma.
\[
\begin{array}[c]{ccc}
\text{Sub}(A)&\stackrel{\exists_{\Delta_A}}{\longrightarrow}&\text{Sub}(A \times A)\\
\big\downarrow\scriptstyle{f^*}&&\big\downarrow\scriptstyle{(f \times id_A)^*}\\
\text{Sub}(B)&\stackrel{\exists_{id_B, f}}{\longrightarrow}&\text{Sub}(B \times A)
\end{array}
\]
Dunque la disuguaglianza varrà se e solo se \[ (\pi_2)^*U \land \exists_{id_B, f}(f^*(1)) \leq_{B \times A} \pi_1^* V \iff (\pi_2)^*U \land \exists_{id_B, f}(1) \leq_{B \times A} \pi_1^* V \] Usando l'identità di Froebenius allora avremo \[ \exists_{id_B,f} \big( ((id_B,f)^*(\pi_2)^*U) \land 1\leq_{B\times A}\pi_1^*V \] Infine, per definizione di \(\land\) e funtorialità di \((-)^*\) la disuguaglianza risulta vera se e solo se \[ \exists_{id_B, f}(\pi_2 \circ (id_B, f))^*(U) \leq_{B \times A} \pi_1^*V \iff \exists_{id_B, f}f^*U \leq_{B \times A} \pi_1^*V \iff f^*U \leq_{B \times A} (id_B,f)^* \pi_1^*V = (\pi_1 (id_B, f))^*V = V\]

Spero sia tutto giusto e di non aver sminchiato nulla :3

[megas_archon]

Mi sembra tutto giusto, benvenut@ nel fantastico mondo delle iperdottrine, o come diceva mio nonno "sito ndà a dottrina?"

Bello fare tutta questa fatica per dimostrare le cose, eh?