Comments on Sur le topos effectif

jeanas (2024-09-30T13:29:37Z)

> 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.

jeanas (2024-09-30T06:32:14Z)

À 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.

jeanas (2024-09-20T09:26:24Z)

jeanas (2024-09-20T09:13:39Z)

> 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.

Ruxor (2024-09-20T08:55:47Z)

@jeanas:

Autoriser E(x,x)=∅ simplifie la définition en évitant d'en faire un cas particulier, et ça doit simplifier divers autres énoncés et preuves. En contrepartie, c'est moins intuitif et on doit plus facilement se prendre les pieds avec des raisonnements vacueux ; et il y a sans doute quelques points où ça complique les choses. 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), donc même si je n'ai pas regardé les détails de ça, c'est une bonne hygiène.

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). Autrement dit, il ne faut pas juste s'assurer que « x existe » et « y existe » à partir de « la relation envoie x sur y », il faut vraiment pouvoir fabriquer algorithmiquement un témoignage du fait que « x existe » et « y existe » à partir d'un témoignage de « la relation envoie x sur y ». Donc même si tous les E(x,x) sont habités, on a quand même besoin de cette forme d'effectivité, et c'est pour ça que supposer E(x,x)≠∅ ne simplifie finalement pas grand-chose. (En général, il n'y a pas d'élément qui appartienne à l'intersection de tous les E(x,x) : supposer ça, pour le coup, c'est une hypothèse forte, et on dit que ces objets sont « uniformes ».)

La situation est la même pour les assemblées : on peut demander que E(x)≠∅ pour tout x, ou bien ne pas le demander. L'avantage si on le demande c'est qu'un morphisme d'assemblées est juste une fonction g:X→Y telle qu'il existe un élément appartenant à l'intersection de tous les E(x)⇛F(g(x)), alors que si on ne le demande pas le morphisme d'assemblées sera une fonction g:X₀→Y vérifiant la même condition, où X₀ est l'ensemble des x tels que E(x)≠∅.

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).

J'aurais vraiment dû commencer par décrire juste la catégorie des assemblées, et parler du topos effectif seulement après. (Il en est la « complétion ex/reg », <URL: https://ncatlab.org/nlab/show/regular+and+exact+completions >, mais intuitivement c'est juste une façon d'ajouter les quotients par des relations d'équivalence.) En tout cas, la question de savoir si on admet ou pas les éléments tels que E(x)=∅ (resp. E(x,x)=∅) est orthogonale au passage de la catégorie des assemblées au topos effectif.

jeanas (2024-09-19T20:15:29Z)

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 ?

Ruxor (2024-09-19T17:25:22Z)

@jeanas: Très honnêtement, à relire ce billet (pas uniquement à cause de ta question mais aussi parce que j'avais besoin de me remémorer certaines choses), je trouve tout le passage sur les morphismes assez épouvantablement mal écrit. J'aurais dû commencer par décrire le cas nettement plus agréable des morphismes entre assemblées avait de commencer à ensevelir le lecteur sous tous les détails fastidieux du cas général. Peut-être que j'ajouterai une sous-section pour ça un jour. En attendant, j'ai ajouté une note encourageant lire en diagonale si nécessaire.

jeanas (2024-09-17T23:21:48Z)

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.

Ruxor (2024-09-17T22:17:10Z)

@jeanas: Oui, c'est juste G=E (la fonction identité a pour graphe la relation d'égalité, si tu veux).

jeanas (2024-09-17T21:23:36Z)

> 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 ?

Essaime (2023-06-22T16:20:51Z)

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.

Damien (2023-06-21T06:38:59Z)

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


You can post a comment using the following fields:
Name or nick (mandatory):
Web site URL (optional):
Email address (optional, will not appear):
Identifier phrase (optional, see below):
Attempt to remember the values above?
The comment itself (mandatory):

Optional message for moderator (hidden to others):

Spam protection: please enter below the following signs in reverse order: 14281e


Recent comments