*Sorry@ 2024-01-22 12:21 Francis Borceux2024-01-22 20:19 ` Sorry Wesley Phoa [not found] ` <CAMH9A7ni+vD17O_NzuUDJjVcW90=7QeXDM3y27VPTGmtbwwH8Q@mail.gmail.com> 0 siblings, 2 replies; 8+ messages in thread From: Francis Borceux @ 2024-01-22 12:21 UTC (permalink / raw) To: categories 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://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b ^ permalink raw reply [flat|nested] 8+ messages in thread

*Re: Sorry2024-01-22 12:21 Sorry Francis Borceux@ 2024-01-22 20:19 ` Wesley Phoa2024-01-24 8:08 ` Sorry Vaughan Pratt [not found] ` <CAMH9A7ni+vD17O_NzuUDJjVcW90=7QeXDM3y27VPTGmtbwwH8Q@mail.gmail.com> 1 sibling, 1 reply; 8+ messages in thread From: Wesley Phoa @ 2024-01-22 20:19 UTC (permalink / raw) To: Francis Borceux;+Cc:categories [-- Attachment #1: Type: text/plain, Size: 883 bytes --] Ungated link to the 1985 JSL paper (see p35 for definition of definability): https://protect-au.mimecast.com/s/Y-NsC2xMRkUwx1OqunZtxI?domain=artscimedia.case.edu Sent > On Jan 22, 2024, at 12:00 PM, 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/AyZTC3QNl1SQ8q01uqrVr5?domain=outlook.office365.com [-- Attachment #2: Type: text/html, Size: 1782 bytes --] ^ permalink raw reply [flat|nested] 8+ messages in thread

*[not found] ` <CAMH9A7ni+vD17O_NzuUDJjVcW90=7QeXDM3y27VPTGmtbwwH8Q@mail.gmail.com>Re: Sorry@ 2024-01-23 3:11 ` Dusko Pavlovic2024-01-23 10:12 ` small global sections vs definability of 1 Thomas Streicher 0 siblings, 1 reply; 8+ messages in thread From: Dusko Pavlovic @ 2024-01-23 3:11 UTC (permalink / raw) To: Francis Borceux;+Cc:categories [-- Attachment #1: Type: text/plain, Size: 3404 bytes --] 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.office365.com >> > [-- Attachment #2: Type: text/html, Size: 4522 bytes --] ^ permalink raw reply [flat|nested] 8+ messages in thread

*small global sections vs definability of 12024-01-23 3:11 ` Sorry Dusko Pavlovic@ 2024-01-23 10:12 ` Thomas Streicher2024-02-08 12:51 ` Dusko Pavlovic 0 siblings, 1 reply; 8+ messages in thread From: Thomas Streicher @ 2024-01-23 10:12 UTC (permalink / raw) To: Dusko Pavlovic;+Cc:Francis Borceux, categories 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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b ^ permalink raw reply [flat|nested] 8+ messages in thread

*Re: Sorry2024-01-22 20:19 ` Sorry Wesley Phoa@ 2024-01-24 8:08 ` Vaughan Pratt2024-01-24 11:02 ` Sorry Thomas Streicher 0 siblings, 1 reply; 8+ messages in thread From: Vaughan Pratt @ 2024-01-24 8:08 UTC (permalink / raw) To: Wesley Phoa;+Cc:Francis Borceux, categories [-- Attachment #1: Type: text/plain, Size: 2624 bytes --] Thanks for that "ungated" link to Bénabou's 1985 JSL paper, Wes. As it turned out, I'd downloaded all 28 pages back in 2011, I can't remember why. Moreover it arrived 26 years earlier in my mailbox in 1985, but who reads every article, especially if you're more on the universal algebra side than the category theory side in 1985. Now that it's 2024, what I'm wondering is, is there 28 pages of useful information there? I appreciate the idea of a fibration as a functor C → B where B is a "base category" looking enough like *Set* (aka *Ens*). In recent years I've been writing about the Yoneda embedding as a way of viewing Chu spaces over *Set*, namely as Set-valued functors representing structured objects. This sort of thing is closer to toposes than abelian categories, both of which I like a lot given that the Big Bang seems to have evolved from a topos to (at least in our neighborhood) an abelian category. What I'm having difficulty with is why Jean took 28 pages to make his point. It seemed better suited to the Journal of Philosophical Logic than to JSL. I'm a great fan of Einstein's "make everything as simple as possible but no simpler". However that implies that there's a boundary, and in the case of fibrations and definability, I'm not at all clear as to where that boundary should be drawn. Vaughan Pratt https://protect-au.mimecast.com/s/3wnSC81Vq2CRLlpYinMtKz?domain=clim8.stanford.edu On Mon, Jan 22, 2024 at 4:03 PM Wesley Phoa <doctorwes@gmail.com> wrote: > Ungated link to the 1985 JSL paper (see p35 for definition of > definability): > https://protect-au.mimecast.com/s/dV7XC91W8rCB9vE2CEg1qQ?domain=artscimedia.case.edu > <https://protect-au.mimecast.com/s/dV7XC91W8rCB9vE2CEg1qQ?domain=artscimedia.case.edu> > > > Sent > > On Jan 22, 2024, at 12:00 PM, 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/tWvzC0YKgRs3ZKwmh2TvYJ?domain=outlook.office365.com > <https://protect-au.mimecast.com/s/tWvzC0YKgRs3ZKwmh2TvYJ?domain=outlook.office365.com> > > [-- Attachment #2: Type: text/html, Size: 4611 bytes --] ^ permalink raw reply [flat|nested] 8+ messages in thread

*Re: Sorry2024-01-24 8:08 ` Sorry Vaughan Pratt@ 2024-01-24 11:02 ` Thomas Streicher0 siblings, 0 replies; 8+ messages in thread From: Thomas Streicher @ 2024-01-24 11:02 UTC (permalink / raw) To: Vaughan Pratt;+Cc:Wesley Phoa, Francis Borceux, categories Dear Vaughan, Benabou"s JSL paper is certainly more of a philosophical character than a mathematical one. But philosophical issues can be relevant and in this case definitely are. I think the following analogy might be helpful. Using strong choice principles every vector space can be endowed with a basis. But nobody thinks that they should form part of the definition or even be preserved by morphisms between them. And so it is with Grothendieck fibrations. They are the right notion but one may choose cleavages. However, they are not part of the structure and certainly should not be preserved by morphism, i.e. cartesian functors. 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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b ^ permalink raw reply [flat|nested] 8+ messages in thread

*Re: small global sections vs definability of 12024-01-23 10:12 ` small global sections vs definability of 1 Thomas Streicher@ 2024-02-08 12:51 ` Dusko Pavlovic2024-02-08 16:36 ` **EXTERN** " streicher 0 siblings, 1 reply; 8+ messages in thread From: Dusko Pavlovic @ 2024-02-08 12:51 UTC (permalink / raw) To: Thomas Streicher;+Cc:Francis Borceux, categories [-- Attachment #1: Type: text/plain, Size: 4924 bytes --] 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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=4eb9b40c-9b3a-48a5-9781-836e5a171e8b> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g> [-- Attachment #2: Type: text/html, Size: 7431 bytes --] ^ permalink raw reply [flat|nested] 8+ messages in thread

*Re: **EXTERN** Re: small global sections vs definability of 12024-02-08 12:51 ` Dusko Pavlovic@ 2024-02-08 16:36 ` streicher0 siblings, 0 replies; 8+ messages in thread From: streicher @ 2024-02-08 16:36 UTC (permalink / raw) To: Dusko Pavlovic;+Cc:Thomas Streicher, Francis Borceux, categories 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=4eb9b40c-9b3a-48a5-9781-836e5a171e8b ^ permalink raw reply [flat|nested] 8+ messages in thread

end of thread, other threads:[~2024-02-08 20:31 UTC | newest]Thread overview:8+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2024-01-22 12:21 Sorry Francis Borceux 2024-01-22 20:19 ` Sorry Wesley Phoa 2024-01-24 8:08 ` Sorry Vaughan Pratt 2024-01-24 11:02 ` Sorry Thomas Streicher [not found] ` <CAMH9A7ni+vD17O_NzuUDJjVcW90=7QeXDM3y27VPTGmtbwwH8Q@mail.gmail.com> 2024-01-23 3:11 ` Sorry Dusko Pavlovic 2024-01-23 10:12 ` small global sections vs definability of 1 Thomas Streicher 2024-02-08 12:51 ` Dusko Pavlovic 2024-02-08 16:36 ` **EXTERN** " streicher

This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).