# Grant season II

As part of my grant application, I am required to ghost-write a letter for the Deputy Vice-Chancellor (Research) to sign in support of the said application. It has to contain a lot of puff-piece promotion material about how good the university is, and how I will add to the stellar research the university already does. The template has the following paragraph:

After: What are your/your School’s plans to employ you upon completion of the fellowship? If you have a continuing position now, you should indicate that you will return to this at the completion of the DECRA. If you are on a contract, you could insert a few sentences outlining what you have negotiated with your Head of School regarding your post-DECRA employment, e.g. “The School of <Name> at the University of Adelaide will strongly consider further employment of the DECRA applicant at the completion of the award for sustained performance at the highest international standards”.

I find this hilarious in a ironic way, since that’s not how things work, in my experience. I know of one person who got a permanent job in my department (definitely well-deserved, too) after getting a grant under this scheme, because some serious leverage was applied at the highest levels of the university.

The only real content is the bit when the university commits to a hard dollar figure on extra spending money for successful applicants. Everything else looks like marketing, or is duplicated from elsewhere in the application.

# Grant season

It’s currently grant-writing season here in Australia, and I’m applying for an early-career grant called a DECRA (Discovery Early Career Researcher Award). It’s the type of thing that can make or break one’s career. You can tell how it’s going by the fact I’m procrastinating about being “passionate and yet [writing] in a dispassionate way” (direct quote from one senior Engineering professor who apparently read my draft) because I’m editing my BibTeX file to shorten the length references to give me more space given the page limit…

# Two small set theory items

I’m supervising an undergraduate student, Blake, this summer who is doing a project on the interaction between category theory and set theory, or more accurately, on showing the Algebraic Set Theory (AST) axioms follow from the NBG axioms. There are two things that I feel I much better understand about set theory in working with Blake.

The first is that the Axiom of Class Comprehension, which states that for any formula $\phi(x_1,\ldots x_n)$ quantifying over only sets and not proper classes, there is a class $A = \{ (x_1,\ldots x_n) \mid (x_1,\ldots x_n) \in A \Leftrightarrow \phi(x_1,\ldots x_n) \}$. Alternative approaches, for instance the finite axiomatisation of NBG, give a list of seven specific cases that are enough to prove each instance of Class Comprehension using induction on the length of $\phi$. Unrestricted (set) Comprehension is an axiom one might try to use in set theory almost identical to Class Comprehension but concludes that a set $A$ exists satisfying the condition. This axiom is famously inconsistent, leading to Russell’s Paradox. So what makes Class Comprehension so different? Morse–Kelley set theory has an analogous axiom schema where quantifiers over classes are permitted, but this is legitimately a stronger system. What I realised this week is that Class Comprehension is actually a secret analogue of Bounded Separation, but for the specific class $V$ of all sets. The axiom of Bounded Separation appeared in Zermelo’s original set theory, and says that for any set $X$ and formula $\phi(x)$ where all quantifiers in $\phi$ are of the form $\forall a\in X$ and $\exists b\in X$, there is a set $\{x\in X \mid \phi(x)\}$. This axiom is more natural from the point of view of topos-theoretic foundations, as Bounded Separation corresponds to having a Heyting category. Whereas in ZFC the sets, the only entities that exist, are in some sense floating free in the universe, in NBG they are all elements of another entity in the theory, namely the class $V$. While working in ZFC people still refer to $V$, but it is not something the theory talks about. So Class Comprehension is secretly Bounded Separation for the class $V$, which is cute.

The other thing I feel I understand better is ‘Scott’s trick‘ (named after Dana Scott), which is a way of constructing a quotient class by an equivalence relation on a class, in the absence of, eg Global Choice. The method requires the (or at least ‘a’) cumulative hierarchy of sets, so that $V = \bigcup_{\alpha\in ORD} W_\alpha$, where each $W_\alpha$ is a set. Given a class $C$ with an equivalence relation $R\subseteq C\times C$, consider the problem of how to construct $C/R$. If everything were sets, then one can build the quotient as a subset of the power set (try it!). In any case, elements of the quotient set are the equivalence classes. But proper classes cannot be elements of classes, and if every $R$-equivalence class is a proper class, there’s no way to make the equivalence classes themselves into elements. In the presence of a strong enough choice principle, then one could in fact choose one element from each equivalence class, as the elements of a class—a transversal to the equivalence relation. Scott’s trick does something that at first glance looks kinda weird: form a new class each whose elements is a set in a fixed equivalence class, and which have minimal rank in the given cumulative hierarchy. If that seems like a mouthful to you, then indeed it is. But the idea is actually not so terrible: instead of using some global choice principle to take one element from each equivalence class $[x]$, one uses the stratification of $V$ to pick a subset of $[x]$. In fact any non-empty intersection $W_\alpha \cap [x]$ would define a set that can stand in for the appropriate element in the quotient, but the intersection with the smallest $W_\alpha$ is canonical. The real content of Scott’s trick is that it gives a canonical subclass $C' \subset C$ such that in the restricted equivalence relation, each equivalence class is only a set, and $C'$ intersects every equivalence class.

Now, I was thinking about Scott’s trick in the context of the axioms of AST, one of which is that the category of classes has coequalisers of kernel pairs. Naturally, since kernel pairs give equivalence relations, and coequalisers are quotients, one might naturally think to use Scott’s trick to show such coequalisers do indeed exist. If one is in NBG, then since Regularity is an axiom, then the standard cumulative hierarchy $V_\alpha$ exists, so Scott’s trick is indeed available—but the point of AST is that it is a more flexible structural framework for classes, and shouldn’t rule out Anti-Foundation or other non-well-founded systems. So it was simultaneously a relief and somewhat amusing that Scott’s trick is not needed to construct the necessary coequalisers, though not a deep fact in itself. The key insight is that given a class function $F \colon X\to Y$, the kernel pair $X\times_Y X$ give an equivalence relation on $X$, and the quotient of this is exactly the image of $F$! So in fact only (at most) Class Comprehension is needed for this step, and not Regularity, which is nice.

# This is what a secure job looks like

Matthew Emerton and Toby Gee wrote a paper in 2017 about algebraic stacks. On the arXiv as usual, and one might expect it to eventually turn up in a journal, even if the results are ‘basic’. But last week it was updated with the message

Minor changes. These results have now been completely incorporated into the Stacks project, so we do not intend to publish this note, or to make further updates to it

No formal publication necessary! If only I could write my work up on the nLab and have it count for academic brownie points…

# Summer is coming

Tomorrow may just be the hottest day in Adelaide on record. I was out and about in the 2009 day that hit 45.7°C (114F). It was like standing in front of an open oven with the fan on, except the oven is the whole open sky. As I write this, it’s 40.2°C (104.4F) outside.

Similar to this situation two years ago, I suppose: