une formalisation des faisceaux et des schémas affines en théorie des types avec Coq
Résumé
On présente ici un début de formalisation de la géométrie algébrique en théorie des types avec la définition des schémas affines. Pour cela topologie, algèbre et théorie des faisceaux ont étés développées en Coq, nous décrivons leurs spécifications, ainsi que les problèmes rencontrés lors de ce travail.