K-théorie de Witt des corps de caractéristique 2 et construction de catégories monoïdales symétriques non-biaisées dans un assistant de preuve

Résumé de la thèse

Cette thèse est divisée en deux chapitres indépendants. Dans le premier chapitre, après quelques rappels sur la théorie (mathbb{A}^1)-homotopique stable et instable, nous prouvons que la K-théorie de Witt d'un corps (F) de caractéristique 2 s'identifie aux puissances de l'idéal fondamental dans l'anneau de Witt de (F). Dans le second chapitre, nous présentons une formalisation en Lean 4 du fait qu'une catégorie monoïdale symétrique peut être débiaisée en une catégorie monoïdale symétrique de Lawvere au sens de Cranch, c'est-à-dire, nous montrons qu'une catégorie monoïdale symétrique peut être interprétée comme un pseudofoncteur préservant les produits finis depuis la ((2,1))-catégorie des correspondances d'ensembles finis vers la bicatégorie des catégories. Après avoir formalisé le théorème de cohérence de Mac Lane pour les catégories monoïdales symétriques, nous formalisons un constructeur explicite de pseudofoncteurs depuis les ((2,1))-catégories de correspondances vers des bicatégories arbitraires. En utilisant ce constructeur et le théorème de cohérence, nous formalisons la construction d'un pseudofoncteur de la ((2,1))-catégorie des correspondances d'ensembles finis vers la bicatégorie opposée d'une bicatégorie de Kleisli (mathcal{K}_{mathrm{SList}}) pour une pseudomonade relative appropriée, et qui est telle que toute catégorie monoïdale symétrique définit canoniquement un pseudofoncteur (mathcal{K}_{mathrm{SList}}^{mathrm{op}} o mathrm{Cat}).

This thesis is split between two independent chapters. In the first chapter, after some recollections on stable and unstable (Aone)-homotopy theory, we prove that the Witt K-theory of a field (F) of characteristic 2 identifies with the powers of the fundamental ideal in the Witt ring of (F). In the second chapter, we present a Lean 4 formalization of the fact that a symmetric monoidal category can be unbiased into a Lawvere-symmetric monoidal category as defined by Cranch, i.e., we show that a symmetric monoidal category can be interpreted as a finite-product-preserving pseudofunctor from the ((2,1))-category of spans of finite sets to the bicategory of categories. After formalizing Mac Lane's coherence theorem for symmetric monoidal categories, we formalize an explicit constructor for pseudofunctors out of ((2,1))-categories of spans to arbitrary bicategories. Using this constructor and the coherence theorem, we formalize the construction of a pseudofunctor from the ((2,1))-category of spans of finite sets to the opposite of a Kleisli bicategory (mathcal{K}_{mathrm{SList}}) for a suitable relative pseudomonad, and which is such that every symmetric monoidal category canonically defines a pseudofunctor (mathcal{K}_{mathrm{SList}}^{mathrm{op}} o mathrm{Cat}).