Institut de recherche mathématique avancée

Résumé : In this talk we focus our attention on compactly supported Hamiltonian diffeomorphisms of the plane. To each pair of distinct fixed points we can associate an integer, the linking number of the pair. Moreover, we can describe the dynamics of the diffeomorphism itself via the Morse complex of a generating function. This Morse complex is classically known to be filtered by action. In this talk we are going to show how we can equip its tensor power with a secondary filtration which keeps track of the linking numbers of pairs of orbits. The proof relies on foundational work on twist maps carried out by Patrice Le Calvez in the '90s, and on uniqueness properties of generating functions. Moreover, we are going to explain how using this language one may provide a finite-dimensional proof of Hofer-lower semicontinuity of the topological entropy, first proved by Alves and Meiwes. One can define a similar filtration on Floer complexes using intersection products of pseudo-holomorphic cylinders as defined by Siefring: if time permits, we are going to provide a sketch of this construction.

Résumé : The talk will present the adaptation of the Neural Semi-Lagrangian method applied to hyperbolic balance law systems that have been linearized using kinetic relaxation. First, the usual process for kinetically relaxing a hyperbolic system with a source term will be briefly explained. Next, the Neural Semi-Lagrangian algorithm adapted to the relaxed hyperbolic system will be presented, where we will have a neural network representing the approximation of the solution of the system for each time of a temporal discretization. Subsequently, the extension of this method will be presented in order to approximate the solution of a family of hyperbolic systems that depend on certain parameters, which is mainly the objective of applying this type of method in the field of neural networks. Finally, an approach will be presented on how to make these methods well-balanced, in the sense that they preserve global stationary solutions of the initial hyperbolic system. Each of the cases will be accompanied by numerical examples applied to the Burgers equation with and without a source, as well as to 1D SWEs with and without bathymetry, and to 2D SWEs.

Résumé : Résumé : Une opérade est une suite symétrique (ou espèce) munie d’une structure de monoïde pour le produit de composition. En caractéristique nulle, la donnée d’une suite symétrique est équivalente à celle de son caractère, qui est une fonction symétrique ; le pléthysme de deux fonctions symétriques correspond alors au produit de composition des suites symétriques associées.

Dans cet exposé, j’expliquerai comment définir des analogues du pléthysme pour différentes décatégorifications de structures opéradiques : les opérades colorées, les props et les propérades. Ces analogues admettent une description calculable et permettent, entre autres, de déterminer la décomposition en facteurs irréductibles de l’homologie stable tordue des groupes d’automorphismes de groupes libres, ainsi que de la cohomologie d’Albanese des groupes d’automorphismes IA.

(Travail en collaboration avec Erik Lindell.)

Résumé : Martin-Löf's intensional type theory is a logical system which can function both as a foundation of mathematics and as a programming language. While the original motivations behind this system were arguably rooted in a desire to give constructive mathematics a more computational interpretation, it turns out that it also has deep links with a seemingly unrelated branch of mathematics: homotopy theory. By adding two features to (intensional) type theory – higher inductive types (roughly: cell complexes) and Voevodsky's univalence axiom (roughly: equality = isomorphism) – we obtain homotopy type theory (HoTT). This language allows us to use type theory to talk about concepts from homotopy theory/algebraic topology such as spaces, paths, homotopies, and so on. Because type theory also functions as a programming language, HoTT is ideal for translating (formalising) proofs from homotopy theory into code which can be formally verified using so-called proof assistants.

In this talk, I will present a recently finished formalisation project of a cornerstone result from homotopy theory: the Serre finiteness theorem. This theorem, which in its simplest form states that homotopy groups of spheres are finitely presented, was recently given a proof entirely in the language of HoTT by Barton and Campion. It is this proof that we have formalised in the HoTT-based proof assistant Cubical Agda. Because HoTT is a constructive language and Cubical Agda is fully computational, our formalised proof of the Serre finiteness theorem can be viewed as an (executable) algorithm which takes as input any homotopy group of any sphere and returns a finite presentation of it. I plan on giving a rough outline of the proof and its formalisation. I will also discuss what problems we run into when actually trying to run our proof/algorithm on a computer. Before doing any of this, however, I will give a quick recap of the very basics of (homotopy) type theory and (Cubical) Agda.

This talk is based on joint work with Reid Barton, Owen Milner, Anders Mörtberg, and Loïc Pujet.

About the speaker : Axel Ljungström is a postdoc at the School of Computer Science at the University of Nottingham working with Ulrik Buchholtz. The position is funded by a scholarship he was awarded from the Knut and Alice Wallenberg foundation. Recently, he was a Ph.D. student in the computational mathematics division of the department of mathematics at Stockholm University. There, he was working on a project on homotopy type theory under the supervision of Anders Mörtberg.

His primary research interests are synthetic homotopy theory and computer formalisation, primarily in (Cubical) Agda. His thesis was mainly concerned the formalisation of cohomology theories and Guillaume Brunerie’s Ph.D. thesis.