Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

December 6, 2011

Reflective Subfibrations, Factorization Systems, and Stable Units

Posted by Mike Shulman

In my last post, I described how in the search for an “internal” description of reflective subcategories of a category HH, we are led to axiomatize instead the following notions:

  1. A reflective subfibration of HH is a system of reflective subcategories C xH/xC_x\subseteq H/x, such that pullback preserves the CC’s and commutes with the reflectors. A reflective subfibration has an underlying reflective subcategory C 1HC_1 \subseteq H.

  2. A stable factorization system is an orthogonal factorization system (E,M)(E,M) for which EE-maps (and hence, the factorizations) are stable under pullback. Given such, we define C x=M/xC_x = M/x, the category of maps yxy\to x lying in MM. The factorizations make C xH/xC_x \subseteq H/x reflective, and stability of EE shows that pullback commutes with the reflectors; thus every stable factorization system has an underlying reflective subfibration.

    Conversely, a reflective subfibration arises in this way exactly when it has the property that if xyx\to y is an object of C yC_y and yzy\to z is an object of C zC_z, then the composite xyzx\to y\to z is also an object of C zC_z. (I think this observation is due to Carboni and Janelidze and Kelly and Paré, “On localization and stabilization for factorization systems”.) The underlying reflective subcategory is M/1M/1, the category of all xx such that x1x\to 1 is in MM.

  3. A lex-reflective subcategory is, of course, a reflective subcategory whose reflector preserves finite limits. Given such a subcategory CHC\subseteq H, we define EE to be the class of maps inverted by the reflector LL, and MM the class of maps right orthogonal to EE. Then (E,M)(E,M) is a stable factorization system whose underlying reflective subcategory is CC. Conversely, a stable factorization system arises from a lex-reflective subcategory in this way exactly when EE satisfies the 2-out-of-3 property, which makes it a reflective factorization system.

In simply trying to axiomatize “a reflective subcategory”, we were essentially forced to these stronger notions, because everything in the “internal logic” automatically happens “locally”, i.e. coherently in each slice. But in this post, I’m not going to go into the internal logic at all (so you can breathe a sigh of relief if you’re getting tired of all that stuff). Rather, I want to know more about reflective subfibrations and stable factorization systems categorically, which seem like rather unfamiliar beasts compared to lex-reflective subcategories. Specifically, I want to address the question: when does a reflective subcategory underlie some reflective subfibration or stable factorization system?

First, a note about categorical dimensions. The last post was all about (,1)(\infty,1)-toposes and their (conjectural) internal homotopy type theory. This post could also be in that world, but I’m not going to use any \infty-ness, so I think everything I say today will make sense in the 1-categorical world as well. I will assume that HH is locally cartesian closed, and we’ll also need some “presentability” conditions that I won’t make precise.

Now, the first observation is that not every reflective subcategory can underlie a reflective subfibration, because the underlying reflective subcategory of any reflective subfibration is an exponential ideal, and hence its reflector must preserve finite products. (This is also true “locally” for each C xH/xC_x\subseteq H/x.) To see why, let C xH/xC_x \subseteq H/x be a system of reflective subcategories, with the reflector L x:H/xC xL_x\colon H/x \to C_x commuting with pullback f *f^\ast along any f:xyf\colon x\to y. This implies that the right adjoint of L xL_x, namely the inclusion C xH/xC_x \hookrightarrow H/x, commutes with the right adjoint of f *f^\ast, namely dependent product Π f\Pi_f. Since the exponential y xy^x can be computed by pulling yy back to H/xH/x, then applying Π x:H/xH\Pi_x\colon H/x \to H, this implies that if yC 1y\in C_1, then so is y xy^x; thus C 1C_1 is an exponential ideal. And a standard argument implies that a reflective subcategory is an exponential ideal if and only if its reflector preserves finite products.

What about the converse — does every reflective exponential ideal underlie a reflective subfibration? To answer this, it’s useful to think of reflective subcategories as localizations. Recall that given a class SS of morphisms in HH, an object of HH is SS-local if (f):H(y,z)H(x,z)(-\circ f)\colon H(y,z) \to H(x,z) is an equivalence for all f:xyf\colon x\to y in SS. Under suitable conditions on SS and HH (such as if HH is locally presentable and SS is small-generated), the SS-local objects form a reflective subcategory, called the localization of HH at SS (the reflector also happens to be the universal functor inverting all maps in SS). Conversely, any reflective subcategory CHC\subseteq H is the localization at some SS; we may take SS to be the class S CS_C of all morphisms inverted by the reflector.

Now we observed that CHC\subseteq H is an exponential ideal if and only if its reflector preserves finite products, and this is easily seen to be equivalent to saying that S CS_C is closed under finite products — in other words, if f:xyf\colon x\to y lies in S CS_C, then for any aHa\in H we have that also a×f:a×xa×ya\times f\colon a\times x\to a\times y lies in S CS_C. Conversely, by the opposite argument, if SS is a class of morphisms which is closed under finite products in this sense, then the SS-local objects must be an exponential ideal. Thus, a reflective subcategory is an exponential ideal just when it is the localization at some class of morphisms closed under finite products.

In particular, this means that the reflective exponential ideals are the internal localizations, in the following sense. Given any class SS, say that zz is internally SS-local if for any f:xyf\colon x\to y in SS, the induced map z yz xz^y \to z^x is an equivalence in HH. By the Yoneda lemma, this is equivalent to saying that H(a,z y)H(a,z x)H(a,z^y) \to H(a,z^x) is an equivalence for all aa, and therefore also equivalent to saying that zz is S¯\overline{S}-local in the usual sense, where S¯={a×f|fS}\overline{S} = \{ a\times f \;|\; f\in S \}. Of course, if SS is closed under products, then S¯=S\overline{S}=S. Thus, just as every reflective subcategory is a localization, every reflective exponential ideal is an internal localization.

Now, suppose that SS is closed under products, and for any aHa\in H, define a *(S)a^\ast(S) to consist of all morphisms c×x c×f c×y a\array{ c\times x & \xrightarrow{c\times f} & c\times y\\ & \searrow & \downarrow\\ & & a } in H/aH/a, for all f:xyf\colon x\to y in SS and all morphisms cac\to a. By assumption on SS, we have 1 *(S)=S1^\ast(S) = S.

Moreover, for any morphism g:abg\colon a\to b, the pullback functor g *:H/bH/ag^\ast\colon H/b \to H/a takes b *(S)b^\ast(S) into a *(S)a^\ast(S), while its left adjoint Σ g:H/aH/b\Sigma_g\colon H/a \to H/b takes a *(S)a^\ast(S) into b *(S)b^\ast(S). By adjunction, the first property implies that if zH/az\in H/a is a *(S)a^\ast(S)-local, then Π g(z)H/b\Pi_g(z) \in H/b is b *(S)b^\ast(S)-local, while the second property implies that if xH/bx\in H/b is b *(S)b^\ast(S)-local, then g *xg^\ast x is a *(S)a^\ast(S)-local.

Suppose HH and SS are such that the localization of H/aH/a at a *(S)a^\ast(S) exists, for all aa; call it C aC_a. Then since pullback preserves local objects, we have a pullback-stable system of reflective subcategories of slice categories; to see that it is a reflective subfibration, we need to check that the reflectors commute with pullback. But for this it suffices to show that the right adjoints of the reflectors — namely, the inclusions C aH/aC_a \subseteq H/a — commute with the right adjoints of pullback — namely the dependent product functors Π g\Pi_g — and this follows from the above observation that Π g\Pi_g preserves local objects. Finally, C 1=CC_1 = C is the localization at SS, since 1 *(S)=S1^\ast(S) = S.

Hence, modulo size considerations, a reflective subcategory underlies a reflective subfibration if and only if it is an exponential ideal. And to extend a reflective exponential ideal CC to a reflective subfibration, we just need to pick a suitable SS, closed under finite products, such that CC is localization at SS. (I presume that in general, different choices of SS for the same CC can produce different reflective subfibrations, but I don’t know any examples.)

This might also be a good point at which to mention that localization can also be performed quite naturally in the internal logic, using a higher inductive type; see this post.


What about extensions to a stable factorization system? It’s natural to expect that we’ll need a “left exactness” condition on the reflector that lies in between preserving finite products and preserving finite limits, and it turns out that the appropriate such condition is called having stable units. This condition on a reflective subcategory CHC\subseteq H was first isolated by Cassidy, Hébert, and Kelly; it has the following equivalent characterizations:

  1. For every xCx\in C, the reflective subcategory C/xH/xC/x \subseteq H/x is an exponential ideal.
  2. The reflector LL preserves all pullbacks over an object of CC.
  3. Every pullback of a unit xLxx \to L x of the reflection is inverted by LL.

The second condition says exactly that the reflector of C/xH/xC/x \subseteq H/x preserves products, so the equivalence of the first and second conditions is by the standard argument. And clearly the second implies the third; the converse is less obvious but true. Note that since 1C1\in C always, having stable units implies that LL preserves products, while of course if LL is left exact then it preserves all pullbacks and hence has stable units.

I remarked above that for any reflective subfibration, the reflective subcategory C xH/xC_x \subseteq H/x is an exponential ideal. Thus, if it happens that C x=C/xC_x = C/x, then the reflector for C=C 1C = C_1 has stable units. However, asking for the inclusion C xC/xC_x \subseteq C/x means asking that the composite of an object yxy\to x of C xC_x with an object x1x\to 1 of C 1C_1 lies in C 1C_1, which is a special case of the condition for our reflective subfibration to be a stable factorization system. In this case, the other inclusion C/xC xC/x \subseteq C_x also follows by a cancellability property of the right class MM in a factorization system. Thus, for any stable factorization system (E,M)(E,M), the underlying reflective subcategory M/1M/1 has stable units.

For the converse, let’s think again in terms of localizations. We saw above that a reflective subcategory is an exponential ideal if and only if it is the localization at some class SS closed under products. I claim that analogously, a reflective subcategory has stable units if and only if it is the localization at some class SS which is stable under pullback.

Suppose first that SS is stable under pullback, let yy and zz be SS-local, and suppose given maps xzx\to z and yzy\to z; we want to show that the domain of the local exponential (yz) (xz)(y\to z)^{(x\to z)} (an object of H/zH/z) is SS-local; call this object ww. Since zz is SS-local, to show this, it will suffice to show that wzw\to z is right orthogonal to SS. However, by definition of ww, a commutative square a w f b z\array{a & \overset{}{\to} & w\\ ^f\downarrow && \downarrow\\ b& \underset{}{\to} & z} (with f:abf\colon a\to b in SS) is equivalent to a commutative square a× zx y b× zx z\array{a\times_z x & \overset{}{\to} & y\\ \downarrow && \downarrow\\ b\times_z x & \underset{}{\to} & z} and likewise a lift in the first square is equivalent to a lift in the second. But since SS is stable under pullback, the map f× zx:a× zxb× zxf\times_z x \colon a\times_z x \to b\times_z x lies in SS, and thus is left orthogonal to yzy\to z (since both yy and zz are SS-local). Thus the second square always has a lift, and hence so does the first. Thus, the SS-local objects have stable units.

Conversely, suppose CHC\subseteq H is a reflective subcategory with stable units, and let T CT_C denote the class of all pullbacks of units xLxx \to L x. Then T CT_C is pullback-stable by construction. Since CC has stable units, we have T CS CT_C\subseteq S_C (with S CS_C the class of all morphisms inverted by LL, as above), so all objects of CC are T CT_C-local. Moreover, CC is also the localization at T CT_C; for if zz is T CT_C-local, then it sees the unit zLzz\to L z as an isomorphism; hence zLzz\cong L z and thus zCz\in C.

Therefore, a reflective subcategory has stable units if and only if it is the localization at some pullback-stable SS. Note, though, that the class S CS_C of all maps inverted by a reflector with stable units need not be pullback-stable. An easy counterexample is the subcategory of subterminal objects in SetSet (or any regular category). Subterminal objects are always an exponential ideal, and pullbacks over a subterminal object coincide with products, so the reflector for this subcategory has stable units. (Alternatively, it underlies the stable factorization system (regular epi, mono), thus has stable units by the argument above.) However, in a classical SetSet, the maps inverted by the reflector consist of all maps between inhabited sets together with the identity map of the empty set, and this class is not stable under pullback (the pullback of 121\to 2 along the other 121\to 2 is 010\to 1).

In fact, S CS_C is pullback-stable precisely when the reflector of CC is left exact. (This fine distinction confused me for quite a while, especially because Prop. 6.2.1.2 in the paper edition of Higher Topos Theory seems to claim that the localization at any pullback-stable class is left exact. That assertion seems to have been removed from the most recent online edition, however.)

With this understanding of stable units in mind, we can address the question of extending a reflective subcategory to a stable factorization system. Suppose SS is pullback-stable and that CC is the localization at SS, hence has stable units. For any aHa\in H, let S aS_a denote the class of morphisms x f y a\array { x & \xrightarrow{f} & y \\ & \searrow & \downarrow\\ & & a} with fSf\in S. Since SS is stable under pullback, the same arguments as in the previous case apply to show that if we take C aC_a to be the localization at S aS_a (again, ignoring size issues), we obtain a reflective subfibration. Moreover, an object xax\to a of H/aH/a lies in C aC_a just when it is right orthogonal to all morphisms of SS, and morphisms with this property are clearly closed under composition. Thus, this reflective subfibration is actually a stable factorization system.

Hence, modulo size considerations, a reflective subcategory underlies a stable factorization system if and only if it has stable units. And to extend a reflective subcategory CC with stable units to a stable factorization system, we just need to pick a suitable pullback-stable SS such that CC is localization at SS.


As a particular case, we can apply these results to the discrete objects in a cohesive topos (or (,1)(\infty,1)-topos). The left adjoint Π\Pi to the “discrete objects” functor makes these into a reflective subcategory, which is assumed to preserve finite products; thus the discrete objects are an exponential ideal. Moreover, it is certainly true in the 1-topos case, and conjecturally so in the (,1)(\infty,1)-topos case, that this reflective subcategory also has stable units. Therefore, it can be extended to some reflective subfibration or stable factorization system, and so axiomatized in the internal type theory directly (without requiring the sharp-escape route).

In other words, sorry Urs, I still can’t seem to make up my mind about the right way to axiomatize cohesion! This argument implies that we can axiomatize Π\Pi as well as \sharp without requiring Type\sharp Type, and we pleasingly get the finite-product-preservation of Π\Pi for free as we remarked earlier. Where I went wrong earlier was focusing on the localization/stabilization factorization system rather than just looking for some stable factorization system. However, I still don’t see any way to describe \flat in this way; I can’t see any reason for the reflective subfibration of discrete objects to also be coreflective, let alone fiberwise equivalent to the reflective subfibration of codiscrete objects. Maybe we should do Π\Pi directly in this way and use sharp-escape for \flat?

Posted at December 6, 2011 7:05 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2469

32 Comments & 0 Trackbacks

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Hi Mike,

first of all sorry for intesecting your post here with my latest. I didn’t see yours while compiling mine.

then: great to see all this stuff! I need some time now to read.

Right now I am a bit confused about this bit here:

In other words, sorry Urs, I still can’t seem to make up my mind about the right way to axiomatize cohesion! This argument implies that we can axiomatize Π\Pi as well as \sharp without requiring Type\sharp Type, and we pleasingly get the finite-product-preservation of Π\Pi for free as we remarked earlier.

(but I haven’t absorbed the details in the paragraphs before yet).

The reason that I am confused is that after longing for precisely this statement I decided here that in my favorite examples of homotopy cohesion, this cannot be true.

I am probably mixed up. Also I keep forgetting the details of these subfibrations after lots of other distractions.

Posted by: Urs Schreiber on December 6, 2011 8:08 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

No need to apologize for anything!

I never quite understood your argument for why this couldn’t work in your favorite examples, but since at the time I was pushing for sharp-escape anyway, I didn’t want to spend the time discussing it. (-: Looking back at it, you seem to conclude that if this works, then we would have a stable factorization system. But a stable factorization system is only a lex-reflective subcategory if it is also a reflective factorization system, and I don’t see why your argument implies this?

Posted by: Mike Shulman on December 6, 2011 8:28 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

But a stable factorization system is only a lex-reflective subcategory if it is also a reflective factorization system, and I don’t see why your argument implies this?

Thanks, you are right, I drew a wrong conclusion there. (I am happy that this conclusion was wrong!)

I never quite understood your argument

Right, what I presented was (only) an argument (as later here) that over \infty-cohesive sites every morphism factors as a Π\Pi-equivalence followed by a map with discrete fibers. I don’t remember why I concluded from this anything about reflective factorization systems. I must have been mixed up.

Posted by: Urs Schreiber on December 6, 2011 8:50 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Hence, modulo size considerations, a reflective subcategory underlies a stable factorization system if and only if it has stable units. And to extend a reflective subcategory CC with stable units to a stable factorization system, we just need to pick a suitable pullback-stable SS such that CC is localization at SS.

Okay, I am following. This is nice.

However, I still don’t see any way to describe \flat in this way;

How about my earlier suggestion: with Π\mathbf{\Pi} and \sharp defined, we next impose the axiom that

| discrete:discretecodiscrete \sharp|_{discrete} : discrete \to codiscrete

is an equivalence. Write ϕ\phi for an inverse equivalence and set

:=ϕ. \flat := \phi \circ \sharp \,.

Posted by: Urs Schreiber on December 7, 2011 12:14 AM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

How about my earlier suggestion: with Π\Pi and \sharp defined, we next impose the axiom that | discrete:discretecodiscrete\sharp|_{discrete}\colon discrete \to codiscrete is an equivalence.

That would be great if it were true. I can’t see any reason for it to be true, though. I mean, it would have to be true locally — is the category of “discrete objects over AA” defined in this way equivalent to the category of “codiscrete objects over AA”, for any AA?

Posted by: Mike Shulman on December 7, 2011 12:18 AM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

When you say ‘discrete objects over AA’, do you mean discrete/Adiscrete/A and similarly for codiscrete objects, or do you mean something like those objects over AA which are fibrewise discrete/codiscrete. In the former case it looks very improbable. In the latter case, we’d have to consider something like the ‘dual’ of an etale map, where the fibres are all codiscrete instead of discrete. The codomain of such a thing would have the smallest topology such that the map was continuous.

Posted by: David Roberts on December 7, 2011 2:49 AM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

do you mean discrete/Adiscrete/A and similarly for codiscrete objects, or do you mean something like those objects over A which are fibrewise discrete/codiscrete.

The latter, but with an emphasis on “something like”.

In the codiscrete case, the definition is that PAP\to A is codiscrete over AA if P P A A\array{P & \overset{}{\to} & \sharp P\\ \downarrow && \downarrow\\ A& \underset{}{\to} & \sharp A} is a pullback. This says equivalently that PP has the initial structure induced from AA, and implies that the category of objects codiscrete over AA is equivalent to the category of codiscrete objects over A\sharp A, i.e. the category Set/ΓASet/\Gamma A (in the 1-category case) or Gpd/ΓA\infty Gpd / \Gamma A (in the (,1)(\infty,1)-category case).

In the discrete case, the definition is a little more up in the air, since there might be multiple stable factorization systems with the same underlying reflective subcategory. If we use the construction I suggested above, then the definition would be that PAP\to A is discrete over AA if it is right orthogonal to all pullbacks of unit maps BΠBB\to \Pi B.

In particular, this means that it has discrete fibers, in the sense that for any global section a:1Aa \colon 1\to A, the pullback a *Pa^\ast P is discrete. It’s not immediately clear to me whether it means more than this; it might not. But it seems unlikely to mean sufficiently more than this that a discrete object over AA would be completely determined by a set or \infty-groupoid over Γ(A)\Gamma(A), which seems to be what would be necessary for the category of objects discrete over AA to be equivalent to that of objects codiscrete over AA.

Posted by: Mike Shulman on December 7, 2011 6:28 AM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

it would have to be true locally — is the category of “discrete objects over AA” defined in this way equivalent to the category of “codiscrete objects over AA”, for any AA?

Grr, right, I don’t know. This continues being more subtle than naively expected (by me, that is).

In this context, let me bounce the following information off you:

This Friday there is a seminar on homotopy type theory at Warsaw University, organized by Chris Kapulkin. I’ll be there, but mainly because the Saturday afterwards I’ll be giving talks to another audience about higher differential geometry and action functionals.

But when we planned this visit, exercise I seemed to have worked out well, and so the idea was that on that Friday I’ll say a bit about homotopy axiomatic cohesion by way of that simple but interesting example for which Guillaume Brunerie kindly had produced some code.

Now, meanwhile you have made all this huge progress on the formulation of the axioms, but the solutions to the original “exercises” broke along the way. Can you see that there is some simple example we could nevertheless easily extract, for the purpose of showing it around?

How about this: the point of exercise I was simply to form the homotopy fiber of BABA\flat B A \to B A and say “this is an internal incarnation of moduli of differential forms”. Now with the new axioms, of all the structures that we have \flat turns out to be the least immediate.

But it would be almost as good or even better to form the homotopy fiber of [ΠX,BA][X,BA][\mathbf{\Pi}X, B A] \to [X, B A]. I wish I had code for this that I could present on Friday. I’ll try it myself, based on your code, but chances are that I will fail. (The least problem being that I can’t manage to patch universe inconsistency on my personal computer.)

I feel bad for asking this after all the effort you have invested: but would this take you more than 5 minutes? :-)

Posted by: Urs Schreiber on December 7, 2011 5:25 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Here is a definition of the homotopy fiber of BGBG\flat B G \to B G, hence I believe a solution to Exercise Ia.

Add LoadPath "..".
Require Import Homotopy Subtopos Codiscrete LocalTopos CohesiveTopos.

Hypothesis BG : Type.
Hypothesis pt : BG.

Definition flat_dR : #Type
  := ipullback ([[fun _:unit => pt]]) (from_flat ([BG])).

Exercise Ib seems to be a lot harder. I haven’t tried the homotopy fiber of [ΠX,BG][X,BG][\Pi X, B G] \to [X, B G] yet, but I expect it won’t be any harder than what I did above; does that alternate Exercise Ia have a corresponding Ib?

Posted by: Mike Shulman on December 7, 2011 8:18 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Here is a definition…

Hah, fantastic!

Let’s see, since by now you also have the code for effective epis, it’s just a few more lines to solutions of II b + II c (plus the “extra credit” there ;-)

(side remark: Eventually I need to better understand conditions for existence and uniqueness of that 0-truncated cover Ω cl n(,A) dRB nA\Omega^n_{cl}(-,A) \to \flat_{dR} \mathbf{B}^n A…)

That’s great. Simple as it may look – I am not sure: does it look simple to anyone? it should, Mike’s ingenuity notwithstanding – simple as it may look, we can now say:

“Starting from simple axioms, we have a computer system that can derive and then reason about moduli nn-stacks for differential cocycles.”

That’s something. Of course the icing on this cake now would be to actually solve II a) and thus by II d) derive the curvature exact sequence. But this can’t be too hard now, can it?

More generally: do you see a quick way to derive from your cohesion axioms that \flat and Π\Pi satisfy the adjunction hom isomorphism in the \sharp-external hom?

Some stupid questions on your code above:

whence the name ipullback? Is this now in Homotopy?

What’s the meaning of the single and double square brackets in your code?

(I guess this just shows that I haven’t read your .v-files in enough detail yet.)

Posted by: Urs Schreiber on December 7, 2011 9:30 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

One more comment: your wrote

Hypothesis BG : Type.
Hypothesis pt : BG.

Is it not easy to add the hypothesis that BG is in fact connected? We just need to say that its 0-truncation / hlevel-2 truncation is equivalent to unit.

This is of course not relevant for “solving” the exercises as stated to far, but it will become relevant once we write Coq-code for the GG-principal \infty-bundles corresponding to terms in X -> BG. And it is of course what only justifies the notation BG.

Posted by: Urs Schreiber on December 7, 2011 9:56 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Single square brackets denote the map to_sharp. So in particular, if X is a type, i.e. X : Type, then [X] : #Type is that same type “viewed from the outside”.

Double square brackets denote the way of viewing a morphism from the outside. Given f : X -> Y, we can first apply to_sharp to obtain [f] : #(X -> Y). Now #(X -> Y) is equivalent to escape ([X] #-> [Y]), where #-> denotes the function-space operation viewed from the outside, i.e. as a map #Type -> #Type -> #Type. So if we transport [f] along this equivalence, we obtain a term in escape ([X] #-> [Y]), which is the external function-space Hom(X,Y)Hom(X,Y) viewed as a codiscrete type, and equivalently denoted X ^-> Y. This composite operation on functions is denoted with double square brackets, so if f : X -> Y, then [[f]] : X ^-> Y is f viewed “from outside”.

Finally, ipullback denotes the pullback operation from the external point of view.

ipullback {A B C : #Type} : (A ^-> C) -> (B ^-> C) -> #Type.

All these notions and notations are defined in Codiscrete.v. There’s certainly room for argument about the notations; in general I tried to use prefixes i and # for “internal” things, and prefixes e and ^ for things that have been escaped.

Is it not easy to add the hypothesis that BG is in fact connected? We just need to say that its 0-truncation / hlevel-2 truncation is equivalent to unit.

Yes (or, perhaps easier, that its 0-truncation is contractible). I omitted that because the HIT directory doesn’t include the 0-truncation yet — although I think I actually have that code sitting around, so I should add it.

Posted by: Mike Shulman on December 7, 2011 10:15 PM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

although I think I actually have that code sitting around, so I should add it.

Done. Now we can say

Hypothesis BG_is_0truncated : is_contr (pi0 BG).

I must say, I continue to get confused about the difference between categorical and geometric homotopy groups and have to straighten myself out again. (-:

Posted by: Mike Shulman on December 7, 2011 11:06 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

While working on the entry cohesive homotopy type theory (still under construction) I noticed:

Hypothesis BG_is_0truncated : is_contr (pi0 BG).

should be named

Hypothesis BG_is_0connected : is_contr (pi0 BG).

I must say, I continue to get confused about the difference between categorical and geometric homotopy groups and have to straighten myself out again. (-:

The categorical homotopy groups are those available in homotopy type theory in general, the geometric ones exist when there is cohesion:

the geometric homotopy groups of XX are the categorical homotopy groups of ΠX\Pi X.

Posted by: Urs Schreiber on December 9, 2011 8:58 AM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

do you see a quick way to derive from your cohesion axioms that ♭ and Π satisfy the adjunction hom isomorphism in the ♯-external hom?

I feel like I’m being stupid, but what isomorphism is that?

it’s just a few more lines to solutions of II b + II c

Hmm. IIb seems to be just “suppose a morphism out of a 0-truncated object”, which is easy:

Hypothesis omclG : Type
Hypothesis omclG_is_set : is_set omclG.
Hypothesis themap : omclG ^-> flat_dR.

and the extra credit is to assume it is effective epi. First we need to externalize epi-ness:

Definition iis_epi {A B} : (A ^-> B) -> #Type.
Proof.
  intros f.
  sharp_induction.
  unsharp_goal.
  exact (is_epi f).
Defined.

Definition eis_epi {A B} (f : A ^-> B) : Type
  := ^(iis_epi f).

(is_epi is defined in HIT/IsInhab.v) and now we can assert what we want:

Hypothesis the_map_is_epi : eis_epi the_map.

But IIc seems to require IIa, which in turn requires Ib, which I haven’t figured out yet. Am I missing something?

Posted by: Mike Shulman on December 7, 2011 10:49 PM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

what isomorphism is that?

Sorry for not expressing myself well. I just mean

Hom(ΠX,A)Hom(X,A). Hom(\mathbf{\Pi} X, A) \simeq Hom(X, \flat A) \,.

Hmm. IIb seems to be just…

Sure, it’s a simple and straightforward definition. Nevertheless, there used to be a time, just a few weeks back, when it seemed to be already a non-trivial accomplishment just to Coq-code this kind of definition. With all the background things like your “^->” it’s all trivial now, but I enjoy seeing this code recorded anyway.

But IIc seems to require IIa, which in turn requires Ib, which I haven’t figured out yet. Am I missing something?

No, you are right, as always. I said this wrong.

Posted by: Urs Schreiber on December 7, 2011 11:03 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

I just mean Hom(ΠX,A)Hom(X,A)Hom(\mathbf{\Pi} X, A) \simeq Hom(X, \flat A)

Under what hypotheses on XX and AA? I only see how to prove it if XX and AA are discrete, but in that case it’s fairly boring, since Π\Pi and \flat are the identity on discrete objects.

Posted by: Mike Shulman on December 7, 2011 11:07 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Under what hypotheses on XX and AA?

Hopefully under no hypothesis. Eventually we want to say that the internal axioms recover the external adjoint triple Π\mathbf{\Pi} \dashv \flat \dashv \sharp.

I was thinking that with the hom-isomorphism for Π\mathbf{\Pi} \dashv \flat there should be a way to Coq-prove that \flat preserves homotopy pullbacks by mimicking the classical proof that right adjoints preserve limits.

Posted by: Urs Schreiber on December 7, 2011 11:24 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Eventually we want to say that the internal axioms recover the external adjoint triple Π⊣♭⊣♯.

Oh, right! I was being stupid after all.

Definition pi_flat_adjunction {A B} : 
  (pi A ^-> B) <~> (A ^-> flat B).
Proof.
  apply @equiv_compose with (B := pi A ^-> flat B).
  apply equiv_inverse, flat_coreflection_equiv; auto.
  apply pi_reflection_equiv; auto.
Defined.

Now in CohesiveTopos.v.

Posted by: Mike Shulman on December 8, 2011 12:32 AM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Thanks for all this code, Mike!

I will try to record and expose this and related things at a new entry cohesive homotopy type theory of which I started creating a skeleton.

But right now I have to run to pick up somebody from the train station…

Posted by: Urs Schreiber on December 7, 2011 11:12 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

I want to state a remark on the factorization systems induced by the Π\mathbf{\Pi}-reflection.

While we are struggling with varying it to make it pullback stable for purposes of internal logic, let’s not forget to record some evident but nice properties that it has in the external logic (that sharp logic ;-).

The ordinary factorization system “Φ(discrete)\Phi (discrete)” in the language of CJKP, is, in their language, “semi-left-exact” or “admissible”, and it continues to be so in homotopy cohesion, at leat over \infty-cohesive sites.

Now, they amplify the relation of this to Galois theory. The right factors in the Φ(discrete)\Phi(discrete)-system for them are the trivial Galois covers.

We had noticed before, in different terms, that every cohesive \infty-topos naturally comes with an internal Galois theory.

But both notions nicely fit together: one finds that the total spaces of the locally constant \infty-stacks in slices of a cohesive \infty-topos are precisely the Π\mathbf{\Pi}-closed morphisms, the right factors in Φ(discrete)\Phi(discrete).

This is easy to see, but nevertheless may provide some insight. For instance it is noteworthy that in the “1-categorical Galois theory” of CJKP only the trivial Galois extensions arise this way as Π\mathbf{\Pi}-closures. Much of the theory there is devoted to working around this problem by considering descent. But passing from cohesive 1-topos to cohesive \infty-toposes this problem just goes away: here the Π\mathbf{\Pi}-closed morphisms already are precisely all the locally constant \infty-stacks, without restriction.

I typed a brief note on this while on the plane to Warsaw today, section 2.3.9.

Posted by: Urs Schreiber on December 8, 2011 7:39 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Very nice! It’s sad that Φ(discrete)\Phi(discrete) is not stable, and thus not internally axiomatizable. I guess we can probably define it externally in the \sharp-logic, though.

Posted by: Mike Shulman on December 8, 2011 9:14 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Here’s another thought in this vein. The map

escape : reflect Type -> Type

which we’ve been using only for \sharp, can be defined for any reflective subfibration. If it is not a lex-reflective subcategory, however, such as Π\Pi, then the composite

TypetoReflectΠ(Type)escapeType Type \xrightarrow{toReflect} \Pi(Type) \xrightarrow{escape} Type

need not be equivalent to Π:TypeType\Pi : Type \to Type. In fact, given a type

x:AB(x):Type x\colon A \vdash B(x) \colon Type

over AA, the type

x:Aescape(toReflect(B(x))):Type x\colon A \vdash escape (toReflect (B(x))) \colon Type

is semantically the pullback of Π(Type^) A [B] Type toReflect Π(Type) \array{ & & & & \Pi(\widehat{Type}) \\ & & & & \downarrow\\ A & \xrightarrow{[B]} & Type & \xrightarrow{toReflect} & \Pi(Type)} This operation gives us a pointed endofunctor of H/A\mathbf{H}/A; is it related to Φ(discrete)\Phi(discrete)?

Posted by: Mike Shulman on December 9, 2011 10:31 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

is it related to Φ(discrete)\Phi(discrete)?

It receives a map from Φ(discrete)\Phi(discrete).

By the naturality of toReflecttoReflect we have that the pullback of

ΠType^ A [B] Type toReflect Π(Type) \array{ && && \Pi \widehat{Type} \\ && && \downarrow \\ A &\stackrel{[B]}{\to}& Type &\stackrel{toReflect}{\to}& \Pi(Type) }

is equivalent to the pullback of

ΠType^ A toReflect ΠA Π[B] Π(Type). \array{ && && \Pi \widehat{Type} \\ && && \downarrow \\ A &\stackrel{toReflect}{\to}& \Pi A &\stackrel{\Pi[B]}{\to}& \Pi(Type) } \,.

So by the commutativity of

ΠB ΠType^ ΠA Π[B] ΠType \array{ \Pi B &\to& \Pi \widehat{Type} \\ \downarrow && \downarrow \\ \Pi A &\stackrel{\Pi[B]}{\to}& \Pi Type }

we have a canonical morphism

ΠBΠA× ΠTypeΠType^ \Pi B \to \Pi A \times_{\Pi Type} \Pi \widehat{Type}

over ΠA\Pi A, which pulls back to a morphism

c ΠBA× ΠTypeΠType^ c_{\Pi} B \to A \times_{\Pi Type} \Pi \widehat{Type}

over AA, with c ΠBc_\Pi B the Π\Pi-closure of BAB \to A in Φ(discrete)\Phi(discrete).

Posted by: Urs Schreiber on December 10, 2011 8:34 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

So if Π\Pi preserved homotopy fibers, then escapetoReflectescape \circ toReflect would act as Π\Pi in the slice over the point.

I know that in many models Π\Pi preserves a large class of homotopy fibers. But I have no idea if it preserves them all.

Posted by: Urs Schreiber on December 12, 2011 10:14 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

I realized that there should actually be a way to talk about Φ(discrete)\Phi(discrete) in the internal type theory (without \sharp). We’ve seen that if we write down axioms that look like they’re talking about a reflective subcategory, then they actually describe a reflective subfibration, and a stable factorization system is a particular case of that.

But if we write down axioms that explicitly look like they’re talking about a factorization system, then I think what we’ll actually be describing is a system of factorization systems, one on each slice category, which are preserved by pullback. If those factorization systems are all induced from the same factorization system on the ambient category, then that factorization system must be stable; but in general they needn’t be. And in fact, we ought to be able to perform the operation Φ\Phi internally, to get from any reflective subfibration to such a system of factorization systems.

What we wouldn’t get this way is a predicate

is_locally_constant : Type -> hProp

such that a dependent type p:BAp\colon B\to A is locally constant (i.e. belongs to the right class of Φ(discrete)\Phi(discrete)) exactly when

forall a, is_locally_constant (B a)

We would instead have only a predicate

is_locally_constant : forall A B, (A -> B) -> hProp

that applies to maps, rather than their fibers.

Posted by: Mike Shulman on December 28, 2011 9:02 PM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Here’s a thought, sort of along the lines we were thinking back here. Suppose we can show that for every object XAX\to A of H/A\mathbf{H}/A, there exists an object AXA\flat_A X \to A of H/A\mathbf{H}/A and a map fromflat X: AXXfromflat_X\colon \flat_A X \to X over AA, such that

  1. the operation \flat and the map fromflatfromflat are preserved by pullback, i.e. given f:ABf\colon A\to B and XBX\to B, we have A(f *X)f *( BX)\flat_A (f^\ast X) \simeq f^\ast (\flat_B X) commuting with f *(fromflat X)f^\ast(fromflat_X) and fromflat f *Xfromflat_{f^\ast X}.

  2. AX\flat_A X is discrete over AA, in whatever sense we are using for Π\Pi.

  3. If A=1A=1, then A\flat_A and fromflatfromflat are the coreflection into discrete objects.

Together, these conditions imply that for every global element a:1Aa\colon 1\to A, the induced map a *( AX)a *Xa^\ast(\flat_A X) \to a^\ast X is discretization (a *X)a *X\flat (a^\ast X) \to a^\ast X.

If we had this, then because of the assumed pullback-stability, we could write down :TypeType\flat\colon Type \to Type and fromFlat:X,XXfromFlat \colon \forall X, \flat X \to X as axioms. Moreover, I think we could also say that for any YY discrete over AA, the induced map on internal-homs [Y, AX] A[Y,X] A[Y,\flat_A X]_A \to [Y,X]_A is a \sharp-equivalence, since \sharp-equivalences are detected on global sections of AA, and on global sections YY is discrete and \flat is discretization. That would give us a sort of hybrid internal/external way to axiomatize \flat, without asking that the objects discrete over AA are actually coreflective for any A1A\neq 1.

Posted by: Mike Shulman on December 8, 2011 1:03 AM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Suppose we can show […] That would give us a sort of hybrid internal/external way to axiomatize \flat, without asking that the objects discrete over AA are actually coreflective for any A1A \neq 1.

I see what you mean. But I can’t seem to think of a A\flat_A-operation that would do the trick. The evident idea to set AXA\flat_A X \to A to be XXA\flat X \to X \to A of course is not pullback stable.

Somehow A\flat_A should be application of \flat fiberwise. So one might try to define it as the pullback of XAX \to A along AA\flat A \to A, followed by applying \flat. But since \flat preserves pullbacks, this would yield trivial A\flat_A.

What else could one try?

Posted by: Urs Schreiber on December 8, 2011 10:09 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Here’s something else I noticed. Suppose our cohesive (,1)(\infty,1)-topos consists of sheaves on some cohesive site. Then there is a stable factorization system such that BAB\to A belongs to the right class exactly when it has discrete fibers (i.e. its pullback along any global element of AA is a discrete object).

The left class of this stable factorization system is generated by the maps U1U \to 1, for all (images of) representables UU. Since the discrete objects are the constant presheaves (which are sheaves), a map is right orthogonal to all these maps precisely when it has discrete fibers. And since any pullback of U1U \to 1 is of the form A×UAA\times U \to A, which is a colimit of copies of U1U \to 1, it follows that any map with discrete fibers is actually right orthogonal to all these pullbacks. Hence the class of all such pullbacks generates the same factorization system, which is therefore stable.

So I guess I’m starting to think that we should axiomatize Π\Pi and the discrete objects as a stable factorization system, and only “go \sharp” to talk about \flat (pending a new insight into a way to avoid that as well).

Posted by: Mike Shulman on December 28, 2011 9:19 PM | Permalink | PGP Sig | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Suppose our cohesive (,1)(\infty,1)-topos consists of sheaves on some cohesive site. Then there is a stable factorization system such that BAB \to A belongs to the right class exactly when it has discrete fibers.

Ah, thanks, good point.

Every Π\Pi-closed/locally constant morphism in particular has discrete fibers over global points, so we have an inclusion of factorization systems Φ(discrete)FiberwiseDiscrete\Phi(discrete) \hookrightarrow FiberwiseDiscrete, I guess.

Is there a universal construction that stabilizes factorization systems? Are stable factorization systems reflective in all factorization systems?

One thing I used to wonder about is how one might deduce an \infty-cohesive site of definition from an abstractly given cohesive \infty-topos (if it exists). This should be related to the question of how to canonically identify a continuum line object in a cohesive \infty-topos, which should be a distinguished object in that site (if it exists).

Your observation indicates that one might want to go for some set of generators of the left class of a pullback stable factorization system for Π\Pi.

Posted by: Urs Schreiber on January 3, 2012 2:31 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Wait a sec, maybe I am not following after all.

In which sense do we want to write A×UAA \times U \to A as a colimit over projections?

We may express any AA as an \infty-colimit over representables

Alim iU i A \simeq {\lim_\to}_i U_i

and then by universality of colimits in the \infty-topos we have that

(A×UA)lim i(U i×UU i). (A \times U \to A) \simeq {\lim_{\to}}_i ( U_i \times U \to U_i) \,.

So it seems we’d need that each U i×UU iU_i \times U \to U_i is left orthogonal to morphisms with discrete fibers over global points. But why is that the case?

Maybe I am mixed up.

Posted by: Urs Schreiber on January 3, 2012 5:41 PM | Permalink | Reply to this

Re: Reflective Subfibrations, Factorization Systems, and Stable Units

Hmm, I guess you’re right, that doesn’t work. Probably I was mixing up my internal and external again.

Posted by: Mike Shulman on January 3, 2012 9:45 PM | Permalink | Reply to this

Post a New Comment