Institut de recherche mathématique avancée

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.

Résumé : On donne une description conjecturale des Valeurs Zêta des schémas arithmétiques en termes de deux complexes parfaits de groupes abéliens et d’une trivialisation canonique. On énonce ensuite un théorème qui peut être vu comme un analogue archimédien de cette conjecture. Afin de prouver la compatibilité avec la conjecture classique de Bloch-Kato, on étudie le carré cartésien de Beilinson d’un point de vue prismatique. Ces résultats impliquent des cas nouveaux de la conjecture de Bloch-Kato. Il s’agit d’un travail en commun avec Matthias Flach et Achim Krause.

Résumé : En l'absence de matière, notre espace-temps est modélisé par l'espace vectoriel R^4 muni d'une forme quadratique Q(x,y,z,t) = x^2 + y^2 + z^2 - t^2 de signature (3,1); trois directions positives (espace) et une direction négative (temps). Un vecteur vérifiant Q(x,y,z,t) <= 0, dit "de type temps", est alors un évènement tel que la distance spatiale de (x,y,z) à l'origine (0,0,0) est, en un sens, plus petite que la distance temporelle entre l'instant 0 et l'instant t. L'évènement (x,y,z,t) peut alors causer (ou être causé) par l'évènement (0,0,0,0). Un chemin lisse de dérivée négative en tout point, dit "causal", peut ainsi être vu comme une suite infinitésimale d'évènements se causant les uns les autres. Dans les modèles d'espace-temps plus généraux, il s'agit plutôt d'une variété de dimension quatre muni d'une métrique lisse de signature (3,1) dite "lorentzienne". Ces objets mathématiques peuvent avoir des propriétés très diverses, dont certaines qui sont incompatibles avec un modèle physique réaliste. Il parait logique, par exemple, de demander qu'il n'existe pas de boucle causale afin qu'un évènement ne puisse pas se causer lui-même. La condition la plus forte pouvant être vérifiée par un espace-temps est l'hyperbolicité globale. Dans cet exposé, nous expliquerons toutes ces notions et nous finirons par discuter leurs généralisations aux espaces munis d'une métrique de signature (p,q), dits "pseudo-riemanniens".