i did, of course, miss something (as i suspected before hitting return, but didn't resist :) but it seems that fixing the error makes the benabou/lawvere link even nicer. (even if i am still missing something i am sure that the link is there.) the one-to-one correspondence between definable subfibrations of E---->B and the "comprehensions" E---->Sub(B) stands. the claim that the subfibration C---->B is obtained by pullback is wrong, because we don't want to pull back along the "truth" into Sub(B) but along the "comprehension". remember how lawvere defined comprehension of the bifibration E---->B to be (in equivalent to hyperdoctrines) the right adjoint of the cartesian functor Arr(B)---->E mapping (i--f-->j) to f_!(top_i). [[i even introduced Arr(B) in the previous message but oversimplified and didn't use it.]] now i can of course restrict that functor to Sub(B)---->E. a definable subfibration C of E, determines a right adjoint E---->Sub(B) and the adjunction localizes on C. how can i say this for fibrations, without using the direct images? well (now i write Arr(E) as E/E and B/P is the comma into P) E--P-->B is a fibration if and only if the induced functor E/E---->B/P is a reflection (the cartesian liftings induce a right adjoint right splitting). a subcategory C of E is a definable subfibration of P if and only E/E---->B/P restricts to C/E---->Sub/P. i think. apologies that i am thinking so much in public, but there is no shortage of private thinking and there is a shortage of public thinking and we should all think together how to bring lawvere and benabou together :) -- dusko On Mon, Jan 22, 2024 at 3:05 PM Dusko Pavlovic <duskgoo@gmail.com> wrote:
as we are talking about lawvere's and benabou's nachlasse, it occurred to me to ask what would benabou's definability be in lawvere's terms. maybe they both knew this and maybe other people do, but i hope it doesn't hurt to spell it out.
let B be a category with pullbacks so we have the fibrations Arr(B)--Cod-->B and Sub(B)--Cod-->B, where Arr(B) is the category of arrows and Sub(B) is the category of subobjects. the cartesian functors B>--Ids-->Sub(B) and B>--Ids-->Arr(B) are the right adjoints.
Prop. B>--Ids-->Sub(B) is the classifier of definable subfibrations. more precisely, for any fibration E--P-->B and a subfibration C>---->E here is a unique cartesian functor E--c-->Sub(B) such that the fibration C---->B is the pullback of c along B>--Ids-->Sub(B).
i did check this, but i didn't check it twice, so i may still be missing something.
-- dusko
On Mon, Jan 22, 2024 at 10:00 AM Francis Borceux < francis.borceux@uclouvain.be> wrote:
Sorry, and thanks to Jon for noticing the slip of terminology in my mail.
Indeed, Bénabou was insisting on the importance of his notion of definability.
Francis
*********************************** Francis Borceux 6 rue François 1490 Court-Saint-Étienne Belgique Fixe: +32(0)10614205 Mobile: +32(0)478390328
----------
You're receiving this message because you're a member of the Categories mailing list group from Macquarie University.
Leave group:
https://protect-au.mimecast.com/s/JhEqC5QP8ySGq6xkfzFqDC?domain=outlook.offi...
Dear Dusko, I think in your mail you confuse small global sections and definability of 1. What I mean is the following. Let P : XX --> BB be a fibration of cats with 1, i.e. P has a right adjoint right inverse 1. Lawvere"s notion of comprehension means that 1 has a right adjoint right inverse G. The counit eps_X : 1_{GX} --> X of 1 --| G at X has the following universal property: for every f : 1_I --> X (over u : I --> PX) there exists a unique \check{f} : I --> GX with eps_X \circ 1_{\check{f}} = f. This is an instance local smallness for for P in the sense that GX = hom(1,X). This is more general than Lawvere's notion of comprehension which assumes that P has also internal sums in which case maps f : 1_I --> X over u : I --> PX correspond uniquely to maps \coprod_u 1_I --> X. But f also corresponds uniquely to \check{f} : I --> GX with P(eps_X) \circ \check{f} = u . But all this has nothing to do with definablity in the sense of Benabou. But one may consider Id_BB as a full subfibration of P via 1. This being definable in the sense of Benabou would mean that for every X in P(I) there exists a greatest subobject m of I such that m^*X is terminal in its fiber. But notice that P(eps_X) is not monic for Lawvere comprehension as considered above. But for posetal fibrations P(eps_X) is always monic, of course. Indeed for posetal fibrations having small global sections may be thought of as a kind of comprehension. But for non-posetal fibrations P the map P(eps_X) is better thiought of as the P(X)-indexed family whose fiber at i \in PX is thought of as the "set of global elements of X_i". Thomas ---------- 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
hi thomas, i am not managing to find time to think of this during the day and wise people make sure to be asleep at 2am but i am way too young for that ;) i do think that there is more to the link between definability and comprehension than just my confusions. the reason is that the two of them are trying to say closely related things and there must be a way to spell it out, invariant under any mistakes that i could ever make. lawvere said early on that categories could be used as the foundation of mathematics. eilenberg and maclane were shaking their heads about the crazy idea of sets without elements (as he recounted) but then, as we know, they invited him to write the introductory paper for la jolla proceedings. after that he went on: "the main foundational operation is comprehension. **how are categorical predicates (in hyperdoctrines) comprehended as categorical constructs?**" --- and he spelled out comprehension as the right adjoint. (yes, he used the fibrewise terminals and direct images to display the logical intuitions behind this particular adjunction in the foundations. but the construction is more general than that.) benabou, on the other hand, says (i just looked up the paper): "In 1970 I realised the possibility of doing all of naive category theory, without sets, in the context of fibrations, and started work on proving that claim." and his naive category theory is the usual category theory, for which he wants to provide a non-set-theoretic categorical axiomatics. his main question was: "*how are categorical predicates (in fibrations) definable as categorical constructs?**. "morally" (as they say in cambridge) the two of them are trying to do the same thing! there must be some truth in morality (contrary to all evidence :))) the way definability is defined in your benabou notes, as far as i can tell in the middle of the night, seems to be saying that * a subfibration CC>--->XX--P-->BB is definable * when there is a cartesian functor XX--->Sub(BB) ** whose image is a subfibration SC>--->Sub(BB) such that ** the reflection XX/XX--->>BB/P (whose right adjoint makes P into fibration) ** restricts along the inclusion SC/P>--->BB/P ** to the reflection CC/XX--->>SC/P. there is probably a better way to say all this. but the main point is that there is, i think, a bijective correspondence between * definable subfibrations of XX--->BB and * subfibrations of Sub(B)--->BB. g'night and sorry about the typos ;) -- dusko On Tue, Jan 23, 2024 at 12:12 AM Thomas Streicher <streicher@mathematik.tu-darmstadt.de<mailto:streicher@mathematik.tu-darmstadt.de>> wrote: Dear Dusko, I think in your mail you confuse small global sections and definability of 1. What I mean is the following. Let P : XX --> BB be a fibration of cats with 1, i.e. P has a right adjoint right inverse 1. Lawvere"s notion of comprehension means that 1 has a right adjoint right inverse G. The counit eps_X : 1_{GX} --> X of 1 --| G at X has the following universal property: for every f : 1_I --> X (over u : I --> PX) there exists a unique \check{f} : I --> GX with eps_X \circ 1_{\check{f}} = f. This is an instance local smallness for for P in the sense that GX = hom(1,X). This is more general than Lawvere's notion of comprehension which assumes that P has also internal sums in which case maps f : 1_I --> X over u : I --> PX correspond uniquely to maps \coprod_u 1_I --> X. But f also corresponds uniquely to \check{f} : I --> GX with P(eps_X) \circ \check{f} = u . But all this has nothing to do with definablity in the sense of Benabou. But one may consider Id_BB as a full subfibration of P via 1. This being definable in the sense of Benabou would mean that for every X in P(I) there exists a greatest subobject m of I such that m^*X is terminal in its fiber. But notice that P(eps_X) is not monic for Lawvere comprehension as considered above. But for posetal fibrations P(eps_X) is always monic, of course. Indeed for posetal fibrations having small global sections may be thought of as a kind of comprehension. But for non-posetal fibrations P the map P(eps_X) is better thiought of as the P(X)-indexed family whose fiber at i \in PX is thought of as the "set of global elements of X_i". Thomas You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>
Hi Dusko, if you say that both local smallness and definability are formulated as requirements that certain elementary fibrations are representable fibrations are reprsentable then I agree. Elementary fibrations are fibrations of posetal groupoids and representable means that the total category of fibrations has a terminal object. Where I disagree is that local smallness can be formulated as a certain subfibration being definable. But, as I said already previously, a posetal fibration P : X --> B of cats with 1 has comprehension if the subfibration 1 : Id --> P is definable. Moreover, Lawvere comprehension means "small global elements" which in case of a fibration of cc's is equivalent to local smallness in the sense of Benabou. Best wishes, Thomas ---------- 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
participants (3)
-
Dusko Pavlovic -
streicher＠mathematik.tu-darmstadt.de -
Thomas Streicher