Emily Riehl is a leading researcher in higher category theory and homotopy theory.
She is professor at Johns Hopkins University ( https://emilyriehl.github.io/ ) and will give a mini-course on the « Elements of ∞-Category Theory » on Tuesday 15th October from 2 p.m. to 4 p.m. (in room CYCL01) and on Wednesday 16th October from 2 p.m. to 4 p.m. (in room CYCL06).
This event is part of a joint project between the category theory research teams of Johns Hopkins University and UCLouvain, with the support of the "Hoover Foundation ».
Abstract : 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.
In addition to these mini-courses, Emily Riehl will give a lecture accessible to a wider audience: ‘Prospects for Computer Formalization of Infinite-Dimensional Category Theory’. This will take place on Thursday 17 October from 10.45 am to 11.45 am (in A.03 Faculty of Sciences).
Abstract : 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.
The last talk on Thursday 17 will be from 12 a.m. to 1 p.m. (in room A.03, Faculty of Science) : Collaborative Formalizations of ∞-Category Theory
Abstract: 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.