small global sections vs definability of 1

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

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