Emily Riehl est une chercheuse de premier plan dans le domaine de la théorie des catégories supérieures et de la théorie de l'homotopie.
Elle est professeur à l'Université Johns Hopkins ( https://emilyriehl.github.io/), et donnera un mini-cours sur les « Elements of ∞-Category Theory » le mardi 15 octobre de 14h à 16h (dans la salle CYCL01) et le mercredi 16 octobre de 14h à 16h (dans la salle CYCL06).
Cet événement s'inscrit dans le cadre d'un projet commun entre les équipes de recherche en théorie des catégories de l'Université Johns Hopkins et de l'UCLouvain, avec le soutien de la « Hoover Foundation ».
Abstract (en) : An ∞-category is an infinite-dimensional weak analogue of an ordinary strict 1-category, intended to capture examples of category-like structure in settings where objects have well-defined "mapping spaces," though perhaps only up to weak homotopy equivalence. In this two-part lecture series, we explain how ideas from formal category theory can be used to extend ordinary 1-category theory to ∞-category theory. Most of our definitions and proof techniques are 2-categorical, deployed in a the 2-category of ∞-categories, ∞-functors, and ∞-natural transformations, which is a defined as a quotient of an infinite-dimensional category called an ∞-cosmos where ∞-categories most naturally live. The first talk will introduce this formal framework and develop the theory of equivalences and adjunctions between ∞-categories. The second talk will turn attention to limits and colimits and left and right Kan extensions, with an application to the theory of stable ∞-categories.
En plus de ces mini-cours Emily Riehl donnera une conférence accessible à un public plus large : "Prospects for Computer Formalization of Infinite-Dimensional Category Theory". Celle-ci aura lieu le jeudi 17 octobre de 10.45 à 11.45 (au A.03 Faculté des Sciences)
Abstract (en) : As mathematics becomes increasingly complicated, the prospect of using a computer proof assistant to (i) certify the correctness of one’s own work and (ii) interact with the formalized mathematical literature becomes increasingly attractive. In this talk, we will describe some recent anecdotes that illustrate what motivates mathematicians to use computer proof assistants and then discuss some particular challenges that arise when it comes to formalizing ∞-category theory.
La dernière conférence se tiendra le jeudi 17 octobre de 12 h à 13h (A.03, Faculté des Sciences) : Collaborative Formalizations of ∞-Category Theory
Abstract (en): We introduce two parallel ongoing collaborative efforts to formalize ∞-category theory in two different proof assistants: Lean and Rzk. We show some sample formalized proofs to highlight the advantages and drawbacks of each formal system and explain how you could contribute to this effort, even if you’ve never used a computer proof assistant before.