Cours (6) du 24 janvier 2013 : le théorème de dualité, par Olivia Caramello

Prise de vue et montage : S. Dugowson

The duality theorem

Statement and proofs of the theorem providing a duality between the subtoposes of the classifying topos of a geometric theory and the quotients of the theory (considered up to syntactic equivalence). Remarks on the proof‐theoretic nature of the notion of Grothendieck topology.

Analysis of the lattice structure on the collection of geometric theories over a given language: transfer of topos‐theoretic notions across the duality and their logical interpretations. The notions of Booleanization and DeMorganization of a geometric theory and their applications in Algebra.

Introduction

Relations entre site et topos. Introduire de nouveaux invariants. Sous-topos.

Sous-topos.

Définition. Opération de clôture sur les sous-objets...

... or, tous les sous-topos sont de cette forme...

[problème technique : il manque un morceau de l'enregistrement vidéo]

Rappel : réciproquement, à tout sous-topos on associe une opération de clotûre.

[problème technique : il manque un morceau de l'enregistrement vidéo]

La notion de sous-topos admet une caractérisation très naturelle en terme de sites.

Remarque : topologies de Lawvere-Tierney

Sous-topos du topos classifiant d'une théorie géométrique

Énoncé du théorème. Quotients d'une théorie géométrique.

Esquisse de démonstration (1)

Esquisse de demonstration (2). Pullback et satisfaction

Esquisse de démonstration (3) : correspondance inverse. Conclusion & Référence.

Référence

Cliquer sur l'image pour accéder

à l'article d'Olivia Caramello sur les treillis de théories

Un théorème en forme d'arche. Remarque sur la dissymétrie des arches.

Interprétation logique.

Transfert du contexte des sous-topos au contexte logique.

Expression diagrammatique du théorème de dualité.

algèbres de (co-)Heyting ( Joyal ); treillis des théories géométriques sur un langage donné.

Topologie de Grothendieck => système démonstratif

Un niveau d'abstraction effrayant... mais pas dangereux !

Opérations de fermeture et axiomatique (ou : "topologie de Grothendieck et théorie de la preuve")

Exemple : un théorème de déduction en logique géométrique.

Sur le pouvoir computationnel des topos de Grothendieck.

Relation entre cribles (topologies de Grothendieck) et séquents (logique géométrique). Bijection entre "théories fermées" des deux systèmes.

Applications du transfert par dualité des notions toposiques.

Sous-topos ouverts; fermés; factorisation épi-mono.

Verbatim

Ce qui nous intéresse le plus, c'est le fait que la notion de sous-topos est un invariant, donc on ne va pas raisonner au niveau des topologies de Grothendieck : on va raisonner au niveau des topos, car là on peut transférer...