I am interested in category theory as a tool for clarifying relationships across mathematics and its applications. Much of my work has focused on monads, a fundamental categorical concept with many uses, including categorical universal algebra. In particular, I've studied codensity and pushforward monads, which generate new monads from functors and other monads.
I've also spent time thinking about enriched categories, which provide a setting
able to encompass on the same footing differential graded categories and metric
spaces. This has led to my interest in the concept of Cauchy dense functor, about which I have written a short article.
Before that, I researched magnitude homology, a homology theory for enriched categories, and hence also metric spaces. I studied when two closed subsets of Euclidean space are magnitude homology equivalent, in the sense of having back-and-forth distance-decreasing maps between them inducing isomorphisms in magnitude homology. This turns out to be characterised up to isometry by an important subset, called the core.
My thesis combines and builds on my papers on Cauchy density and pushforward monads.
A new section is devoted to the interaction between pushforward monads and (π-weak)
distributive laws. It gives conditions for the existence and uniqueness of distributive
laws under codensity monads. I give several new examples of pushforward monads
in the last chapter.
A continuous map of metric spaces whose image is dense is an epimorphism. This
paper considers the corresponding notion for V-functors, as identified by
Lawvere. I call such functors Cauchy dense. I review the result that Cauchy
dense V-functors are the cofully faithful 1-cells of V-Cat. I then show
that the Cauchy completion of a V-category A is the largest V-category
admitting a fully faithful Cauchy dense functor from A. I also study Cauchy
dense functors in special cases, such as between monoids in V.
Pushforward monads
Theory and Applications of Categories, Vol 44, No. 30
·
2025
Let T be a monad on A and G: A → B
be a functor. The pushforward G#T of T along G
is the monad on B most closely related to T through G. It is given by the
right Kan extension of GT along G, when it exists. In this paper, I study
the general properties of this construction and produce several examples. The most
important example here is that the pushforward of the powerset monad along the
inclusion FinSet → Set is the filter monad.
Magnitude homology equivalence of Euclidean sets
with
Tom Leinster ·
Algebraic and Geometric Topology 26
·
2024
Magnitude homology is a homology theory for metric spaces. We study what pairs of back-and-forth distance-decreasing maps induce inverse isomorphisms in magnitude homology. We give a concrete geometric characterisation of this situation for closed subsets of Euclidean space. Along the way, we prove a strengthening for closed convex sets of Carathéodory's theorem, and introduce the inner boundary and core of a space.
Encoding dependently-typed constructions into simple type theory
This conference paper was the result of a summer research internship at the Computer Lab in Cambridge. I formalised the theory of strict ω-categories in Isabelle/HOL, which then served as an example of how to encode traditionally dependently-typed constructions in a simple type theory.
This expository article was written as a group. It introduces persistent
homology (prominent in the field of topological data analysis) and relates it
to three other areas. Together with part of the introduction, I focused on the
relationship between persistent homology and magnitude homology.
My master's thesis, supervised by Jacob Rasmussen.
It builds up to the construction of HOMFLY-PT homology of oriented links, which
itself categorifies the HOMFLY-PT polynomial. In doing so it introduces, the
category of Soergel bimodules, which is a categorification of the Hecke algebra.
It sketches a proof of the invariance of HOMFLY-PT homology under link isotopy,
and carefully computes the homology of the (2,n)-torus link.
Exploring the capabilities of the Lean interactive theorem prover
This is my undergraduate final year thesis. I learned how to use the proof
assistant Lean and used it to
formalise several IMO problems, as well as the Jordan–Hölder theorem of
group theory.