Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 9 of 9
I see the definitions of discrete fibration and fibration in a 2-category in the nLab, and one could that there is a natural development from these, namely a fibration of internal categories (thinking of internal categories as forming a 2-category). In the Elephant (just before Examples B.2.5.4) Johnstone writes that it is possible to develop the notion of internal split (op)fibration in an arbitrary cartesian category, but doesn’t “pursue the details”.
I’m interested, and I’m guessing it may not be as trivial as all that, because I’d like to work out Moerdijk’s notion of fibration of sites for internal sites in a base topos, at least in the nice case that said fibration induces an open surjection of sheaf toposes. So there is at least two possible definitions, namely a translation into the internal language of a topos of a fibration, and a purely diagrammatic definition (say, using comma categories and adjoints). It would be nice if these coincided, but if not, that’s also interesting.
I’m pretty sure they’ll coincide. Doesn’t the Elephant discuss internal fibrations of sites somewhere in part C?
Not internal fibrations.
EDIT: at least not explicitly. All the material is constructive, but done assuming the base topos is $Set$, with the note that it could be done in general $S$.
Concerning the equivalence of “fibration” in the internal and in the 2-categorical sense, I think there is a subtlety regarding internal vs external existence. If $\mathcal{S}$ is a topos and $P:\mathbb{X}\to\mathbb{C}$ is an internal functor that is a fibration in the internal logic, then it is not necessarily a fibration in the representable sense in $\mathbf{Cat}(\mathcal{S})$. In fact if supports do not split in $\mathcal{S}$, not even the functor $\mathbf{Cat}(\mathcal{S})(1,\mathbb{X})\to\mathbf{Cat}(\mathcal{S})(1,\mathbb{C})$ is necesssarily a fibration. For, if $X$ is an ‘external/global’ object of $\mathbb{X}$, and $f$ is an external morphism in $\mathbb{C}$ such that $P(X)=\mathrm{cod}(f)$, the fact that $P$ is an internal fibration only tells us that the statement “there exists a cartesian lifting of $X$ along $f$” holds in the internal logic, which does not necessarily yield a global element if supports don’t split.
Here is a sketchy way I think can be used to construct counterexamples: A category $\mathcal{C}$ internal to a presheaf category is simply a presheaf of categories, and an internal Grothendieck fibration into such an internal category is the same as a Grothendieck fibration into the Grothendieck construction of $\mathcal{C}$.
Now if we don’t want supports to split, we can take e.g. presheaves on $\mathbb{S}=(L\leftarrow \bot \rightarrow R)$. Taking $\mathcal{C}=\Delta(0\to 1)$ it is easy to construct a fibration on $\int\mathcal{C}=\mathbb{S}\times (0\to 1)$ such that the corresponding internal functor is not a fibration in the 2-categorical sense.
@Jonas: Ah, yes, that’s right — you’d have to use an “algebraic” sort of definition of fibration or interpret “existence” in the pure-constructive way — or else take the morphisms in your 2-category of internal categories to be anafunctors.
@David: Ah, right, I was thinking of C2.5.7 where he shows that fibrations of sites are the “externalization” of certain internal sites, but that’s the other way ’round.
Mike, I agree with you that it works when you use an algebraic definition of fibration. Concretely, I think all you need is “cleaved fibrations”, i.e. fibrations that are equipped with choices of cartesian liftings.
But I don’t understand what you mean by interpreting existence in a “pure constructive way”, or how to resolve the mismatch using anafunctors. Do you mean one should consider internal anafunctors where one leg is an internal Street fibrations? I don’t see how this would solve the problem, since it would make the class of internal fibrations even bigger.
On the other hand, I don’t see how to apply a concept of anafunctor to the 2-categorical setting since here the concept of equivalence is defined algebraically and thus any equivalence has a weak inverse by definition and every ’anafunctor’ is equivalent to an ordinary 1-cell.
I think what Mike meant is that you could take the definition of a fibration in a bicategory, and take the bicategory to be that of internal categories, anafunctors and transformations, where every anafunctor is most definitely not isomorphic to a functor (and just the ordinary notion of anafunctor: backwards leg is an epimorphic on objects, fully faithful internal functor). This in some sense recovers the interpretation of constructive existence as ’local existence’ wrt to some Grothendieck topology (in the topos case, just the canonical topology).
Johnstone mentions that cloven fibrations are an algebraic notion, so go through without change, but I don’t think I want this, even though the fibrations in question (fibrations of sites a la Moerdijk) have a right adjoint that is a section.
Thanks for the explanation David, that makes sense. Unfortunately i don’t know the work of Moerdijk that you are interested in, but I might have a look if I find time.
@David 7 yes, that’s what I meant for anafunctors.
As for what I meant by “pure constructive existence”, I don’t have time to explain here in detail, but I’ll link to propositions as types and two blog posts. However, in principle, I think using anafunctors is the “right” solution.
1 to 9 of 9