Sorry

Sorry

[Francis Borceux]

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

Re: Sorry

[Wesley Phoa]

[-- 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 --]

Re: Sorry

[Dusko Pavlovic]

[-- 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 --]

small global sections vs definability of 1

[Thomas Streicher]

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

Re: Sorry

[Vaughan Pratt]

[-- 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 --]

Re: Sorry

[Thomas Streicher]

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

Re: small global sections vs definability of 1

[Dusko Pavlovic]

[-- 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 --]

Re: **EXTERN** Re: small global sections vs definability of 1

[streicher]

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