One thing I learned from Thomas Streicher's paper on universes in toposes is that definability is related to descent — for instance, if you restrict the codomain fibration to a stable class of maps, you get a full subfibration, and definability in the sense of Bénabou is the gap between this subfibration and its stack completion. There is a lot of potential for this idea contributing to future works in category theory; for example, Mike Shulman has extended Bénabou's definability from "classes" of things in a fibration (i.e. properties) to a notion of definability that makes sense for structures; Andrew Swan has given a very interesting and thorough investigation of this generalised definability and its practical implications here: https://arxiv.org/abs/2206.13643.
Definability is quite a fascinating thing. Peter Freyd's work on the core of a topos and the subsequent work on isotropy groups of toposes I find very pretty. One related thing that I am reminded of is the following cute fact. Possibly it is well known; I do not know the SGAs and EGAs very well. Suppose I have a fibration E ---> B and some X in E(b). I can consider the existence of an "object G(X) of group structures on X". What this means is a map f: G(X) ---> b in B, together with a group structure on f^*(X) in E(G(X)), which is universal among such in the expected way. Clearly this is an instance of (the more general?) definability. Let us consider this for the following fibration. The base B is the category of affine schemes, CRng^op. The fibre over a ring k is the category of formal affine k-schemes, i.e., the Ind-completion of the k-Alg^op. This is a full subfibration of the codomain fibration of Ind(k-Alg^op). In the terminal fibre of this fibration we have the affine line L = Spec(Z[x]). This is an internal ring object in the fibre and so we can form its subobject N <= L of nilpotent elements ("Spec of Z[[x]]"). Now for any commutative ring k, to give a group structure on k^*(N) ("Spec of k[[x]]") in the category of formal affine k-schemes is to give a formal group law with coefficients in k. It follows that the "object of group structures on N" is Lazard's universal coefficient ring for a formal group law. What is also quite fun is to compute the object of group structures on the generic group O in the (codomain fibration of) the group classifier [Grp_fp, Set]; this turns out to be O+O. This is because, given any group G, there are G+G ways of making it into a group. Indeed, each g in G yields two group structures on G, one with x * y = x.g^-1.y, and another with x * y = y.g^-1.x. Richard ---------- You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. Leave group: https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27