Topology Seminar Thursday 3 August, 13:15-14:00, Simastuen 656

Ulrik Buchholtz (Nottingham): The Geometry of Simplicial Type Theory

Abstract: Simplicial Type Theory is an extension of Homotopy Type Theory proposed by Emily Riehl and Mike Shulman. The intended model is the higher topos of simplicial spaces (or simplicial objects in an arbitrary higher topos)., Via this interpretation it gives a “synthetic” way of talking about higher categories qua complete Segal objects (or sheaves of higher categories over the base topos). But the type theory isn't quite strong enough to nail down this interpretation, in particular, it could also be modeled in reflexive graphs over the base, or other strange things. I'll talk about using geometric logic to improve this situation, inspired in part by work by Ingo Blechschmidt and coworkers on synthetic algebraic geometry. I might also say something about a 2-Yoneda lemma done in this setting.

Topology Seminar Thursday 3 August, 14:15-15:00, Simastuen 656

Jonathan Weinberger: Formalizing the \(\infty\)-categorical Yoneda lemmma

Abstract: Computer proof assistants are computer programs to check the correctness of a mathematical proof. There exists a wide variety of those, and they have been used increasingly in recent decades. Notable examples include verifications of:

• Ferguson-Hales's proof of the Kepler conjecture (2003-2014, in Isabelle)
• Feit-Thompson's Odd Order Theorem, playing a central role in the classification of finite simple groups (2006-2012, in Coq)
• some of Scholze and Clausen's work on condensed mathematics, implemented as the "Liquid Tensor Experiment" (2020-2022, in Lean)

Modern-day algebraic geometry and homotopy theory make heavy use of \(\infty\)-category theory, the formalization of which in a computer proof assistant has largely remained elusive. The natively homotopical flavor of \(\infty\)-category theory makes it a challenge to find a good foundational system that makes formalization amenable.

This is, in fact, made possible in the new proof assistant Rzk (https://rzk-lang.github.io/rzk), developed by Kudasov. The underlying theory is based on Riehl-Shulman's simplicial type theory from 2017, a version of homotopy type theory augmented with a directed interval. This formal language permits the synthetic development of parts of \(\infty\)-category theory as done in work by Riehl-Shulman, Buchholtz-W, and Bardomiano Martínez. But these used "pen and paper" rather than a proof assistant.

Now, together with Riehl and Kudasov, we have formalized Riehl-Shulman's version of the synthetic \(\infty\)-categorical Yoneda Lemma in Rzk (https://emilyriehl.github.io/yoneda/). Additional formalizations have been contributed by Bakke in Rzk, and by Hazratpour in Lean who formalized a version of the 1-categorical Yoneda lemma.

In the talk, I'll briefly introduce the basic vocabulary of Riehl-Shulman's synthetic \(\infty\)-category theory and present a demo of the formalized \(\infty\)-categorical Yoneda lemma in Kudasov's Rzk proof assistant. Using the case study of the Yoneda lemma, we will explain the conceptual and practical advantages as well as challenges that arise when doing synthetic \(\infty\)-category theory in this setting.

Topology Seminar Thursday 22 August, 15:00-16:00, Simastuen 656

Alexander Schmeding (NTNU): What is and why care about infinite-dimensional differential geometry?

Abstract: In this talk I will give an introduction to current topics in infinite-dimensional geometry together with some applications of the theory. Starting from manifolds of (differentiable) mappings we will see some examples of infinite-dimensional Lie groups. Then we shall briefly visit (weak) Riemannian geometry in an infinite-dimensional setting and discuss how geometric techniques on manifolds of mappings provide tools for relevant finite dimensional problems. In particular, we will discuss applications in geometric hydrodynamics and shape analysis.

Topology Seminar Thursday 14 September, 14:15-15:00, Simastuen 656

Jonas Stelzig (LMU München): Formality and dominant maps

Abstract: A map of orientable equidimensional closed manifolds that induces a surjection in rational homology is called dominant. In general, one expects the target of a dominant map to be simpler than the source. A manifold is called formal if the graded-commutative differential graded algebra of forms is quasi-isomorphic to the cohomology. This implies (under some condition on the fundamental group) that the whole rational homotopy type is determined by the cohomology ring. I will explain that the target of a dominant map is formal if the source is and discuss the context of this result. Joint work with Aleksandar Milivojevic and Leopold Zoller.

Seminar Thursday 9 November, 11:00-12:00, Simastuen 656

Drew Heard (NTNU): The spectrum of Goodwillie calculus

Abstract: We will explain a recent computation of the Balmer spectrum of n-excisive functors from finite spectra to spectra. We will spend the majority of the time trying to explain what this means. This is joint work with Arone, Barthel, and Sanders.

Seminar Thursday 16 November, 14:15-15:15 (note the unusual time), Simastuen 656

Sebastian Martensen (NTNU): Toda brackets in n-angulated categories

Abstract: Toda brackets is a tool originally introduced to help calculate stable stems. Today they have been defined in arbitrary triangulated categories and, in triangulated categories with an algebraic enhancement, they coincide with Massey products. In joint work with Martin Frankland and Marius Thaule, we generalise the various constructions for Toda brackets that exist to the setting of the so-called “n-angulated categories” and show that they coincide.

In this talk I will attempt to introduce and motivate Toda brackets along with their n-angulated counterparts, and talk about how these two notions are explicitly related.