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...
Booleanisation.
La double négation est une opération de clôture. Remarque sur topos élémentaires et ceux de Grothendieck.
Booleanisation d'une théorie géométrique. La logique géométrique est intrinsèquement constructive.
De Morganisation pour la théorie des corps.
Théorème d'existence d'un sous-topos dense maximal de De Morgan.
Préfaisceaux sur la catégorie des corps finis.
Références.
Dans le cadre des théories de type préfaisceaux...
Théories de type préfaisceaux.
Relation entre syntaxe et sémantique. Construction sémantique du topos classifiant.
Modèles J-homogènes.
Référence :
topologie atomique et modèles faiblement homogènes
Exemples de (topologie => syntaxe) : groupoïde => booléen; amalgamation => De Morgan; cohérence, compacité,..
.
Conclusion du cours du 24 janvier 2013
***