Category Archives: Logique

Oskar Becker 

https://en.m.wikipedia.org/wiki/Oskar_Becker

Advertisements

CCC : cartesian closed category (catégories cartésiennes fermées)

Une catégorie est dite

cartésienne

si elle possède un objet terminal et si tout couple d’objets possède un produit.

https://fr.m.wikipedia.org/wiki/Catégorie_cartésienne

https://fr.m.wikipedia.org/wiki/Produit_(catégorie)

Rappel : objet terminal comme produit sont deux exemples de limites d’un diagramme

https://mathesisuniversalis2.wordpress.com/2015/08/21/diagrammes-cones-et-limites-dans-une-categorie/

Un objet terminal (c’est à dire tel qu’il existe une flèche unique dirigée de tout objet de la catégorie vers cet objet terminal) est limité du diagramme vide (“goutte de néant qui manque à la mer”), un produit de deux objets est la limite du diagramme formé par ces deux objets uniquement (sans flèches)

Une catégorie cartésienne est dite fermée si elle est aussi munie de l’exponentiation, si pour tout couple d’objets Z et Y il existe un objet exponentielle ZY

https://fr.m.wikipedia.org/wiki/Objet_exponentiel

La page en anglais sur les CCC est nettement meilleure:

https://en.m.wikipedia.org/wiki/Cartesian_closed_category

Une exponentielle est définie aussi comme limite d’un diagramme:


image

On comprend plus facilement si l’on regarde ce qui se passe dans le cas de la catégorie des ensembles (qui est un topos, donc possède toutes les limites finies, donc est une CCC):

Si Z et Y sont des ensembles, objets du topos Ens, alors :

ZY est l’ensemble des applications (des flèches, des fonctions) de Y vers Z

ZY = {f | f: Y——-> Z}

La flèche (la fonction, dans le cas des ensembles) eval :

eval : ZY × Y ——–> Z

est la fonction évaluation qui envoie un couple (f, y) sur la valeur de f au point y qui est f(y) et appartient par définition à Z

Et l’application

λg : X ——> ZY

(Notation venant du λ-calcul, voir https://fr.m.wikipedia.org/wiki/Lambda-calcul)

est telle que:

λg(x)(y) = g(x,y)

C’est ce qu’on appelle en programmation la forme curryfiée de g

https://fr.m.wikipedia.org/wiki/Curryfication

A noter qu’une adjonction apparaît, dans le cas d’une CCC (munie d’exponentielle pout tout couple d’objets) : le foncteur qui envoie Z sur ZY est adjoint à droite du foncteur qui envoie A sur A × Y

Et cette adjonction est caractérisée par la bijection naturelle entre les ensembles de flèches :

image

Notes on topos theory

Ces notes passent en revue divers aspects des topoi, notamment les deux sortes de définitions (elementary topoi et Grothendieck topoi) et abordent les aspects logiques liant logique et topologie.

http://rin.io/swashbuckling-topoi/

Et il y a des tas de liens dans le corps du texte, notamment un cours d’introduction:

http://www.fuw.edu.pl/~kostecki/ittt.pdf

une introduction informelle de Leinster:

http://arxiv.org/pdf/1012.5647.pdf

et un article d’Awodey sur les connections entre géométrie, algèbre et logique : “Type theory and homotopy”:

https://www.andrew.cmu.edu/user/awodey/preprints/TTH.pdf