The correspondence between homotopy types and higher categorical analogs of groupoids which was first conjectured by Alexander Grothendieck naturally leads to a view of mathematics where sets are used to parametrize collections of objects without "internal structure" while collections of objects with "internal structure" are parametrized by more general homotopy types. Univalent Foundations are based on the combination of this view with the discovery that it is possible to directly formalize reasoning about homotopy types using Martin-Lof type theories.
School of Mathematics
This is a report on some joint work with Mark Reeder and Jiu-Kang Yu. I will review the theory of parahoric subgroups and consider the induced representation of a one-dimensional character of the pro-unipotent radical. A surprising fact is that this induced representation can (in certain situations) have finite length. I will describe the parahorics and characters for which this occurs, and what the Langlands parameters of the corresponding irreducible summands must be.
We study families of filtered phi-modules associated to families of p-adic Galois representations as considered by Berger and Colmez. We show that the weakly admissible locus in a family of filtered phi-modules is open and that the groupoid of weakly admissible modules is in fact an Artin stack. Working in the category of adic spaces instead of the category of rigid analytic spaces one can show that there is an open substack of the weakly admissible locus over which the filtered phi-modules is induced from a family of crystalline representations.
A "proof assistant" is a software package comprising a validity checker for proofs in a particular logic, accompanied by semi-decision procedures called "tactics" that assist the mathematician in filling in the easy parts of the proofs. I will demonstrate the use of the Coq proof assistant in doing simple proofs about inductive structures such as natural numbers, sequences, and trees.
The classical Dvoretzky theorem asserts that for every integer k>1 and every target distortion D>1 there exists an integer n=n(k,D) such that any
There is a way to specify any smooth, closed oriented four-manifold using a surface decorated with simple closed curves, something I call a surface diagram. In this talk I will describe three moves on these objects, two of which are reminiscent of Heegaard diagrams for three-manifolds. These may form part of a uniqueness theorem for such diagrams that is likely to be useful for understanding Floer theories for non-symplectic four-manifolds.