#HoTT André Joyal : la notion de typos

Voir cet ancien article :

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/14/andre-joyal-hott-tribus-et-⊓-tribus/

et la note de Joyal :

http://www.math.uwaterloo.ca/~asl2013/Slides/Joyal.pdf

Page 15 sur 52 définition du «  push forward functor » associé à une flèche f : A → B dans une catégorie C

Le foncteur est noté f!

Et il est dirigé de la slice category C/A vers C/B ( c’est à dire les catégories dont les objets sont les morphismes de C ayant pour cible A ou B)

selon la formule :

f!( X,p) = (X, fp)

( voir le carré Page 15)

Page 17:

Ce foncteur f! a un foncteur adjoint à droite :

f*: C/B → C/A

Tout ceci étant associé rappelons le à un morphisme f: A → B dans la catégorie C. Ce foncteur est appelé foncteur changement de base (« base change ») et (voir le diagramme page 17) il envoie un morphisme p sur un morphisme q appelé changement de base de p le long de f

Un morphisme dans une tribu (C,F) est dit anodyne s’il appartient à la classe F

C’est à dire les mrphismes tels que u ⋔ f pour un f de F

Un pre-typos est défini page 40 sur 52: c’est une tribu ayant deux propriétés supplémentaires:

– le changement de base le long d’une fibration d’un morhisme anodyne reste anodyne

– tout morphisme f admet une factorisation f= pu avec u anodyne et p une fibration .
Les fibrations sont définies page 22 sur 52: une fibration est une flèche de la classe de morphismes F qui définit la « tribe structure » de C: une tribu est la donnée du couple ( C, F) page 22..
Cette notion se distribue dans différents domaines mathématiques:

https://anthroposophiephilosophieetscience.wordpress.com/2017/09/05/highertopostheory-15-fibrations-densembles-simpliciaux/

https://ncatlab.org/nlab/show/fibrations

Voir aussi:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/17/hott-andre-joyal-tribes-and-fibrations/

Page 42:

Un « path object » PX pour un objet X est une factorisation du morphisme diagonal X → X × X

Comme vu sur le diagramme page 42

Page 43:
Une homotopie entre deux flèches :

f,g : X → Y

Est une flèche de X vers ce « path object » PY faisant commuter le diagramme page 43

S’il existe une homotopie entre f et g on dit que f et g sont homotopique, relation que l’on note:

f ∾ g

Page 43:

Cette relation d’homotopie est une congruence sur les flèches de C, ce qui en prenant le quotient par cette congruence permet de définir une nouvelle catégorie :

Ho(C)= C/ ∾

Appelée en anglais « homotopy category » de C . Cette notion se généralise, voir par exemple le livre de Jacob Lurie ou bien :

https://ncatlab.org/nlab/show/homotopy+category

Une flèche f : X → Y dans C est une équivalence homotopique si elle correspond dans Ho(C) à une flèche inversible ( un isomorphisme)

Un objet X de C est dit « contractible «  si dans la flèche : X → ⊤ ( où ⊤ est l’objet terminal de C, qui existe puisque C est une tribu) est une équivalence homotopique .

Page 44:

Un morphisme de pre – typoi est un foncteur qui préserve :

– l’objet terminal, les fibrations et les changements de base de fibrations

– La relation d’homotopie

Les pre-typoi forment ainsi une catégorie

Exemple de tels foncteurs : le foncteur changement de base :

C(B) → C(A)

Correspondant à un morphisme dans C:

u : A → B

Page 45:

Un pretypos C est un typos si c’est une π- tribu ( Page 29) et si le foncteur produit ( adjoint à droite du foncteur changement de base, voir Page 30 sur 52) correspondant à une fibration f: A → B
Si ce foncteur donc préserve la relation d’homotopie.

Si C est un typos, alors pour tout objet A de C la tribu locale C (A) est aussi un typos.

Page 46 : exemple de typos : la catégorie Grpd des groupoides ( en prenant comme fibrations les isofibrations)

https://ncatlab.org/nlab/show/isofibration

Page 47 : un morphisme de typos est un foncteur qui préserve :

– l’objet terminal , les fibrations et les changement de base de fibrations
– les relations d’homotopie

– les produits internes ( Page 30)

Exemple : le foncteur changement de base correspondant à un morphisme u dans un typos C

Page 48 : si u: A → B est un morphisme dans Un typos C alors le foncteur correspondant

Ho ( u*) : Ho ( C(B)) → Ho (C(A))

a un adjoint à gauche et un adjoint à droite

Le foncteur :

A → Ho (C(A)) est une hyper- doctrine au sens de Lawvere :

https://ncatlab.org/nlab/show/hyperdoctrine

Les pages suivantes abordent les notions de fibration universelle et de typos univalent, mais il vaut mieux ici s’adresser aux cours plus récents et développés de Joyal:

https://anthroposophiephilosophieetscience.wordpress.com/2017/10/20/hott-le-cours-dandre-joyal-en-cinq-parties-sur-les-tribus/

https://mathesismessianisme.wordpress.com/2017/10/14/andre-joyal-what-is-an-elementary-higher-topos-slides/

Sans manquer de noter le théorème de Voevodsky donnant un exemple de typos univalent : la catégorie Kan des complexes de Kan

https://ncatlab.org/nlab/show/Kan+complex

Advertisements
This entry was posted in ∞-catégories, ∞-topoi, homotopy type theory and tagged , , , , . Bookmark the permalink.