PhD Thesis Defence

Speaker: Siyuan Yu (Western)

"Symplectic embeddings of five balls into the complex projective plane"

Time: 13:00

Room: MC 107

In 1985, Gromov proved the remarkable Non-Squeezing Theorem: a symplectic embedding of a closed ball of radius r into the symplectic cylinder $Z^{2n}(R)=B^2(R)\times \mathbb{R}^{(2n-2)}$ exists if and only if $r\le R$. This show that in general, symplectic embeddings have more obstructions than volume constraints. One of the obstructions is known as the Gromov’s capacity. In this thesis, we study the problem of symplectic embeddings of five disjoint closed balls of Gromov’s capacities $c_1,…,c_5$ into the complex projective space $\mathbb{C}P^2$. By investigation of the action of the group of symplectomorphisms of $\mathbb{C}P^2$ on the space of symplectic embeddings, the homotopy type of the space of symplectic embeddings can be computed: it is homotopy equivalent to a union of strata in the configuration space of five points on $\mathbb{C}P^2$, with the precise strata determined by the chosen capacities. Moreover, the homotopy type of the space of symplectic embeddings of five balls remains constant as the capacities vary within any given stability chamber of capacities. The complete set of stability chambers is also determined.

Mathematics Departmental Presentation 2026

Speaker: Thomas Thorbjørnsen (Western)

"Finitely Adequate Modules in Synthetic Algebraic Geometry"

Time: 15:30

Room: MC 108

Synthetic algebraic geometry (SAG) is an extension of homotopy type theory that provides a language for internal reasoning about the big Zariski topos. In SAG, we postulate the existence of a generic local ring R with some additional properties. Schemes over R are not defined by giving the underlying space a structure sheaf; rather, they are defined by a property of the space itself. Sheaves on a scheme are then expressed as bundles over the scheme, and on the sheaves themselves we have many of the usual operations, such as taking cohomology.

However, algebraic geometry often looks different from this internal point of view, compared to the classical external one. For instance, we can show that the generic local ring R is not Noetherian, and so the category of finitely presented R-modules is not abelian. In particular, the cohomology groups of sheaves of finitely presented R-modules may no longer be finitely presented. In this talk, we shall study the abelian closure of the finitely presented R-modules in the category of all R-modules, which we call the finitely adequate R-modules. We will characterize the finitely adequate R-modules which are injective and projective in this subcategory. Then, we prove that finitely adequate R-modules are closed under extensions. We hope that the category of finitely adequate R-modules gives us a suitable replacement for the category of finitely presented modules, so that the cohomology groups of finitely adequate sheaves are finitely adequate.

Ph.D. Candidacy Exam Lecture

Speaker: Theo Chatzidiamantis Christoforidis (Western)

"Fixed Point Properties in Synthetic Homotopy Theory"

Time: 10:00

Room: MC 107

In topology, results such as Brouwer's fixed point theorem are often not accessible from the homotopy-theoretic point of view, since they usually depend on more than just the homotopy type of a given space, and many are also not constructively provable. By working in the setting of homotopy type theory, we will see that studying the property "every self-map has a fixed point" provides a different, homotopy-invariant notion.

After constructing counterexamples, we show that classifying spaces of non-Abelian finite simple groups satisfy this property. Along the way, we compute the homotopy groups of the space of maps into a classifying space in homotopy type theory. In particular, if G and H are finite groups, we will show that we can completely describe the space of maps between their classifying spaces constructively. Our results are formalised in the Rocq proof assistant.

This talk is based on joint work with Dan Christensen.

Ph.D. Candidacy Exam Lecture

Speaker: Zack Dooley (Western)

"The Internal Language Conjecture"

Time: 14:00

Room: MC 107

Dependent type theory is an alternative foundation to mathematics that has provided the basis for proof assistant software such as Rocq or Lean. This is enabled by the nice computational properties of type theory, but another valuable aspect of type theory is its syntax/semantics relationship with category theory. This relationship allows us to not just study our foundations using category theory, but also to study (higher) category theory using type theory. While we understand this relationship well in certain cases, such as with the lambda calculus and Cartesian closed categories, for many type theories, including most of those used in proof assistants, our understanding of this relationship is still incomplete. In this talk I will discuss the nature of this relationship and explain part of the internal language conjectures which posit an equivalence between certain type theories and higher categories.