Comments on Sur le topos effectif

> Notons que la définition de la réciproque d'un isomorphisme est très simple sur les relations fonctionnelles : la réciproque de G:X×Y→𝒫(ℕ) et la fonction Y×X→𝒫(ℕ) donnée par (y,x) ↦ G(x,y), et la question de si G définit un isomorphisme s'exprime simplement par le fait que ceci définit bien une relation fonctionnelle (c'est l'existence de u et v qui est en question, celle de d et r étant claire).

Ta formulation me donne l'impression que ça doit être trivial. Je me sens bête mais je ne vois pas pourquoi, j'ai raté un argument évident ?

Je vois comment le montrer, ce n'est pas difficile, mais il faut quand même réfléchir un petit peu. En gros, en supposant G◦H=id, H◦G=id, on refait en intuitionniste et en rajoutant des G(x, x) un peu partout la preuve hypotaupinale de « f◦g=id ∧ g◦f=id ⇒ f, g bijections réciproques » pour prouver que G est bijective dans la logique interne, on en déduit que H': (y, x) ↦ G(x, y) est une relation fonctionnelle, on vérifie que G◦H'=id, H'◦G=id (respectivement grâce à la surjectivité et l'injectivité interne de G), et on conclut H=H' (c.à.d. H, H' équivalentes) par unicité des inverses dans une catégorie.

Peut-être que la validité intuitionniste de « f◦g=id ∧ g◦f=id ⇒ f, g bijections réciproques » est tellement évidente pour toi que tu n'y penses pas ? Moi qui n'ai pas l'habitude des maths intuitionnistes, j'ai eu besoin de faire la vérification. Surtout que je pense habituellement à « f injective » plutôt comme « ∀ x x', x≠x' ⇒ f(x)≠f(x') », or intuitionnistement ça implique « ∀ x x', ¬¬(f(x)=f(x')) ⇒ ¬¬(x=x') » soit « ∀ x x', ¬¬(f(x)=f(x')⇒x=x') », mais pas « ∀ x x', f(x)=f(x')⇒x=x' » a priori.

À cause de toi, en rêvant cette nuit d'un type que je n'ai pas vu depuis le collège-lycée, qui n'a pas dû faire de maths après, et qui était en permanence agité et insupportable, je l'ai vu me demander : « Au fait, tu as trouvé la réponse à la question que je t'avais posée sur les ensembles simpliciaux ? ». À y repenser, c'était *vraiment* bizarre comme rêve.

Étudier les topos est dangereux pour votre santé mentale. À consommer avec modération.

> Il en est la « complétion ex/reg », <URL: https://ncatlab.org/nlab/show/regular+and+exact+completions >

nLab be like: <URL:https://bsky.app/profile/monniauxd.bsky.social/post/3l3ai5p6e562u>

> Mais je pense que c'est indispensable si, par exemple, on veut construire le topos effectif en logique intuitionniste (par exemple au sein d'un autre topos)

Pas faux. Ça doit être pas mal dans le genre prise de tête, par contre :-) Ou il faut vraiment avoir l'habitude de raisonner de manière interne à un topos (que je n'ai pas encore).

> Ce qui est sûr, c'est que faire l'hypothèse E(x,x)≠∅ ne permettra pas de se dispenser de supposer l'existence de divers éléments, par exemple le ‘d’ dans la définition que je donne d'une relation fonctionnelle : ce dernier ne sert pas juste à assurer que E(x,x) et F(y,y) sont habités, mais bien qu'on peut en produire un de façon calculable en fonction d'un élément de G(x,y).

Ah oui, je suis bête, tu as complètement raison, j'étais en train de perdre de vue ce point pourtant central.

> Il faut sans doute penser à E(x) dans le cas d'une assemblée (et E(x,x) dans le cas d'un objet plus général) comme une « façon de désigner x » pour les algorithmes, donc une sorte d'ensemble des noms de x (en gardant à l'esprit l'idée que si le même nom peut désigner plusieurs éléments, alors l'algorithme est magiquement capable de les distinguer).

C'est effectivement l'analogie que prend Bauer dans son texte (que je suis en train de lire en parallèle).

Merci pour les éclaircissements, en tous cas.

Oui, tu as tendance à donner beaucoup de détails, forcément c'est un avantage et un inconvénient à la fois. Trouver le juste équilibre est toujours dur…

En attendant, autre question. Pour l'instant (mais je n'ai pas encore tout lu et encore moins tout compris), je ne saisis pas l'intérêt d'autoriser E(x, x) = ∅ pour un élément x ∈ X d'un objet (X, E), vu qu'en retirant ces x on obtient un objet isomorphe comme tu l'écris toi-même, donc la catégorie serait équivalente, et ils cassent un peu les pieds p.ex. pour définir les relations fonctionnelles parce qu'il faut que les paires soient formés d'objets qui existent (avec un témoin uniforme…). Il y a une raison naturelle de les autoriser ?

Tu dis à un endroit que le topos effectif est la complétion de la catégorie des assemblées (je ne sais pas pour quoi exactement d'ailleurs). Dans la construction de cette complétion, ces éléments qui n'existent pas apparaissent ?

Désolé, j'avais dû comprendre quelque chose de travers, mais je ne comprends plus quoi, et le paragraphe est parfaitement clair. Morale : il est temps de faire dodo.

> Pour donner au moins un exemple dès ce stade, pour n'importe quel objet (X,E), la fonction E définit une relation fonctionnelle de l'objet vers lui-même, appelée relation identité. La vérification de l'existence de d,r,u,v est facile :

Comment est définie l'identité ? Il manque une phrase, j'imagine ? C'est juste G=E ?

J'ai commencé à lire cette entrée, en tant que probabiliste titillé par les topos sans savoir en grand détail ce que c'est. Je me suis pour l'instant arrêté au tout début de la section sur les relations fonctionnelles. J'ai l'impression d'avoir raisonnablement bien compris ce que j'ai lu. Ré-expliquer les choses de façon redondante avec tantôt du formalisme, tantôt de l'intuition, en multipliant les points de vue, ça permet de trouver quelque chose auquel se raccrocher (quelque chose dépendant du lecteur). Je ne prétends pas te l'apprendre, je te signale juste que l'effet escompté est atteint, du moins en ce qui me concerne.

Tu mentionnes le fait que pour un topos de Grothendieck, on a un morphisme géométrique vers le topos des ensembles alors que pour le topos effectif, c'est dans l'autre sens. Y a-t-il une manière simple de faire passer le pourquoi de cette différence ? Du genre "c'est toujours contravariant quand on passe de l'algèbre aux espaces or là il se passe que … " ?

Merci en tout cas pour ton travail.

Une autre référence intéressante et assez lisible : https://arxiv.org/abs/2204.00948