Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 15th 2014
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI 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](http://www.numdam.org/item?id=CM_1986__58_1_45_0) 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 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.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeApr 15th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI'm pretty sure they'll coincide. Doesn't the Elephant discuss internal fibrations of sites somewhere in part C?

   I’m pretty sure they’ll coincide. Doesn’t the Elephant discuss internal fibrations of sites somewhere in part C?

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 15th 2014
   • (edited Apr 15th 2014)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexNot _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$.

   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$.

4. • CommentRowNumber4.
   • CommentAuthorJonasFrey
   • CommentTimeApr 15th 2014
   • PermaLink
   Author: JonasFrey
   Format: MarkdownItexConcerning 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeApr 15th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@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.

   @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.

6. • CommentRowNumber6.
   • CommentAuthorJonasFrey
   • CommentTimeApr 16th 2014
   • (edited Apr 16th 2014)
   • PermaLink
   Author: JonasFrey
   Format: MarkdownItexMike, 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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorDavidRoberts
   • CommentTimeApr 16th 2014
   • (edited May 24th 2023)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI think what Mike meant is that you could take the definition of a [fibration in a bicategory](https://ncatlab.org/nlab/show/fibration+in+a+2-category), 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorJonasFrey
   • CommentTimeApr 16th 2014
   • PermaLink
   Author: JonasFrey
   Format: MarkdownItexThanks 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeApr 16th 2014
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex@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](http://golem.ph.utexas.edu/category/2012/01/propositions_as_some_types_and.html) [posts](http://golem.ph.utexas.edu/category/2012/11/freedom_from_logic.html). However, in principle, I think using anafunctors is the "right" solution.

   @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.