## 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 $H$, we are led to axiomatize instead the following notions:

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

2. A stable factorization system is an orthogonal factorization system $(E,M)$ for which $E$-maps (and hence, the factorizations) are stable under pullback. Given such, we define $C_x = M/x$, the category of maps $y\to x$ lying in $M$. The factorizations make $C_x \subseteq H/x$ reflective, and stability of $E$ 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 $x\to y$ is an object of $C_y$ and $y\to z$ is an object of $C_z$, then the composite $x\to y\to z$ is also an object of $C_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/1$, the category of all $x$ such that $x\to 1$ is in $M$.

3. A lex-reflective subcategory is, of course, a reflective subcategory whose reflector preserves finite limits. Given such a subcategory $C\subseteq H$, we define $E$ to be the class of maps inverted by the reflector $L$, and $M$ the class of maps right orthogonal to $E$. Then $(E,M)$ is a stable factorization system whose underlying reflective subcategory is $C$. Conversely, a stable factorization system arises from a lex-reflective subcategory in this way exactly when $E$ 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 $(\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 $H$ 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_x\subseteq H/x$.) To see why, let $C_x \subseteq H/x$ be a system of reflective subcategories, with the reflector $L_x\colon H/x \to C_x$ commuting with pullback $f^\ast$ along any $f\colon x\to y$. This implies that the right adjoint of $L_x$, namely the inclusion $C_x \hookrightarrow H/x$, commutes with the right adjoint of $f^\ast$, namely dependent product $\Pi_f$. Since the exponential $y^x$ can be computed by pulling $y$ back to $H/x$, then applying $\Pi_x\colon H/x \to H$, this implies that if $y\in C_1$, then so is $y^x$; thus $C_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 $S$ of morphisms in $H$, an object of $H$ is $S$-local if $(-\circ f)\colon H(y,z) \to H(x,z)$ is an equivalence for all $f\colon x\to y$ in $S$. Under suitable conditions on $S$ and $H$ (such as if $H$ is locally presentable and $S$ is small-generated), the $S$-local objects form a reflective subcategory, called the localization of $H$ at $S$ (the reflector also happens to be the universal functor inverting all maps in $S$). Conversely, any reflective subcategory $C\subseteq H$ is the localization at some $S$; we may take $S$ to be the class $S_C$ of all morphisms inverted by the reflector.

Now we observed that $C\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_C$ is closed under finite products — in other words, if $f\colon x\to y$ lies in $S_C$, then for any $a\in H$ we have that also $a\times f\colon a\times x\to a\times y$ lies in $S_C$. Conversely, by the opposite argument, if $S$ is a class of morphisms which is closed under finite products in this sense, then the $S$-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 $S$, say that $z$ is internally $S$-local if for any $f\colon x\to y$ in $S$, the induced map $z^y \to z^x$ is an equivalence in $H$. By the Yoneda lemma, this is equivalent to saying that $H(a,z^y) \to H(a,z^x)$ is an equivalence for all $a$, and therefore also equivalent to saying that $z$ is $\overline{S}$-local in the usual sense, where $\overline{S} = \{ a\times f \;|\; f\in S \}$. Of course, if $S$ is closed under products, then $\overline{S}=S$. Thus, just as every reflective subcategory is a localization, every reflective exponential ideal is an internal localization.

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

Moreover, for any morphism $g\colon a\to b$, the pullback functor $g^\ast\colon H/b \to H/a$ takes $b^\ast(S)$ into $a^\ast(S)$, while its left adjoint $\Sigma_g\colon H/a \to H/b$ takes $a^\ast(S)$ into $b^\ast(S)$. By adjunction, the first property implies that if $z\in H/a$ is $a^\ast(S)$-local, then $\Pi_g(z) \in H/b$ is $b^\ast(S)$-local, while the second property implies that if $x\in H/b$ is $b^\ast(S)$-local, then $g^\ast x$ is $a^\ast(S)$-local.

Suppose $H$ and $S$ are such that the localization of $H/a$ at $a^\ast(S)$ exists, for all $a$; call it $C_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_a \subseteq H/a$ — commute with the right adjoints of pullback — namely the dependent product functors $\Pi_g$ — and this follows from the above observation that $\Pi_g$ preserves local objects. Finally, $C_1 = C$ is the localization at $S$, since $1^\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 $C$ to a reflective subfibration, we just need to pick a suitable $S$, closed under finite products, such that $C$ is localization at $S$. (I presume that in general, different choices of $S$ for the same $C$ 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 $C\subseteq H$ was first isolated by Cassidy, Hébert, and Kelly; it has the following equivalent characterizations:

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

The second condition says exactly that the reflector of $C/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 $1\in C$ always, having stable units implies that $L$ preserves products, while of course if $L$ 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_x \subseteq H/x$ is an exponential ideal. Thus, if it happens that $C_x = C/x$, then the reflector for $C = C_1$ has stable units. However, asking for the inclusion $C_x \subseteq C/x$ means asking that the composite of an object $y\to x$ of $C_x$ with an object $x\to 1$ of $C_1$ lies in $C_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/x \subseteq C_x$ also follows by a cancellability property of the right class $M$ in a factorization system. Thus, for any stable factorization system $(E,M)$, the underlying reflective subcategory $M/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 $S$ closed under products. I claim that analogously, a reflective subcategory has stable units if and only if it is the localization at some class $S$ which is stable under pullback.

Suppose first that $S$ is stable under pullback, let $y$ and $z$ be $S$-local, and suppose given maps $x\to z$ and $y\to z$; we want to show that the domain of the local exponential $(y\to z)^{(x\to z)}$ (an object of $H/z$) is $S$-local; call this object $w$. Since $z$ is $S$-local, to show this, it will suffice to show that $w\to z$ is right orthogonal to $S$. However, by definition of $w$, a commutative square $\array{a & \overset{}{\to} & w\\ ^f\downarrow && \downarrow\\ b& \underset{}{\to} & z}$ (with $f\colon a\to b$ in $S$) is equivalent to a commutative square $\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 $S$ is stable under pullback, the map $f\times_z x \colon a\times_z x \to b\times_z x$ lies in $S$, and thus is left orthogonal to $y\to z$ (since both $y$ and $z$ are $S$-local). Thus the second square always has a lift, and hence so does the first. Thus, the $S$-local objects have stable units.

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

Therefore, a reflective subcategory has stable units if and only if it is the localization at some pullback-stable $S$. Note, though, that the class $S_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 $Set$ (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 $Set$, 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 $1\to 2$ along the other $1\to 2$ is $0\to 1$).

In fact, $S_C$ is pullback-stable precisely when the reflector of $C$ 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 $S$ is pullback-stable and that $C$ is the localization at $S$, hence has stable units. For any $a\in H$, let $S_a$ denote the class of morphisms $\array { x & \xrightarrow{f} & y \\ & \searrow & \downarrow\\ & & a}$ with $f\in S$. Since $S$ is stable under pullback, the same arguments as in the previous case apply to show that if we take $C_a$ to be the localization at $S_a$ (again, ignoring size issues), we obtain a reflective subfibration. Moreover, an object $x\to a$ of $H/a$ lies in $C_a$ just when it is right orthogonal to all morphisms of $S$, 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 $C$ with stable units to a stable factorization system, we just need to pick a suitable pullback-stable $S$ such that $C$ is localization at $S$.

As a particular case, we can apply these results to the discrete objects in a cohesive topos (or $(\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 $(\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 $\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:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2469

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

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 $\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 $C$ with stable units to a stable factorization system, we just need to pick a suitable pullback-stable $S$ such that $C$ is localization at $S$.

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

$\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 $\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 $A$” defined in this way equivalent to the category of “codiscrete objects over $A$”, for any $A$?

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 $A$’, do you mean $discrete/A$ and similarly for codiscrete objects, or do you mean something like those objects over $A$ 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/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 $P\to A$ is codiscrete over $A$ if $\array{P & \overset{}{\to} & \sharp P\\ \downarrow && \downarrow\\ A& \underset{}{\to} & \sharp A}$ is a pullback. This says equivalently that $P$ has the initial structure induced from $A$, and implies that the category of objects codiscrete over $A$ is equivalent to the category of codiscrete objects over $\sharp A$, i.e. the category $Set/\Gamma A$ (in the 1-category case) or $\infty Gpd / \Gamma A$ (in the $(\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 $P\to A$ is discrete over $A$ if it is right orthogonal to all pullbacks of unit maps $B\to \Pi B$.

In particular, this means that it has discrete fibers, in the sense that for any global section $a \colon 1\to A$, the pullback $a^\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 $A$ would be completely determined by a set or $\infty$-groupoid over $\Gamma(A)$, which seems to be what would be necessary for the category of objects discrete over $A$ to be equivalent to that of objects codiscrete over $A$.

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 $A$” defined in this way equivalent to the category of “codiscrete objects over $A$”, for any $A$?

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 $\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 $[\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 $\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 $[\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 $\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 $n$-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

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 $G$-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)$ 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 $X$ are the categorical homotopy groups of $\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(\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(\mathbf{\Pi} X, A) \simeq Hom(X, \flat A)$

Under what hypotheses on $X$ and $A$? I only see how to prove it if $X$ and $A$ 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 $X$ and $A$?

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 “$\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 $\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 $\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 $\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

$Type \xrightarrow{toReflect} \Pi(Type) \xrightarrow{escape} Type$

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

$x\colon A \vdash B(x) \colon Type$

over $A$, the type

$x\colon A \vdash escape (toReflect (B(x))) \colon Type$

is semantically the pullback of $\array{ & & & & \Pi(\widehat{Type}) \\ & & & & \downarrow\\ A & \xrightarrow{[B]} & Type & \xrightarrow{toReflect} & \Pi(Type)}$ This operation gives us a pointed endofunctor of $\mathbf{H}/A$; is it related to $\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 $\Phi(discrete)$?

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

By the naturality of $toReflect$ we have that the pullback of

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

is equivalent to the pullback of

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

So by the commutativity of

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

we have a canonical morphism

$\Pi B \to \Pi A \times_{\Pi Type} \Pi \widehat{Type}$

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

$c_{\Pi} B \to A \times_{\Pi Type} \Pi \widehat{Type}$

over $A$, with $c_\Pi B$ the $\Pi$-closure of $B \to A$ in $\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 $escape \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 $\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\colon B\to A$ is locally constant (i.e. belongs to the right class of $\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 $X\to A$ of $\mathbf{H}/A$, there exists an object $\flat_A X \to A$ of $\mathbf{H}/A$ and a map $fromflat_X\colon \flat_A X \to X$ over $A$, such that

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

2. $\flat_A X$ is discrete over $A$, in whatever sense we are using for $\Pi$.

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

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

If we had this, then because of the assumed pullback-stability, we could write down $\flat\colon Type \to Type$ and $fromFlat \colon \forall X, \flat X \to X$ as axioms. Moreover, I think we could also say that for any $Y$ discrete over $A$, the induced map on internal-homs $[Y,\flat_A X]_A \to [Y,X]_A$ is a $\sharp$-equivalence, since $\sharp$-equivalences are detected on global sections of $A$, and on global sections $Y$ 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 $A$ are actually coreflective for any $A\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 $A$ are actually coreflective for any $A \neq 1$.

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

Somehow $\flat_A$ should be application of $\flat$ fiberwise. So one might try to define it as the pullback of $X \to A$ along $\flat A \to A$, followed by applying $\flat$. But since $\flat$ preserves pullbacks, this would yield trivial $\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 $(\infty,1)$-topos consists of sheaves on some cohesive site. Then there is a stable factorization system such that $B\to A$ belongs to the right class exactly when it has discrete fibers (i.e. its pullback along any global element of $A$ is a discrete object).

The left class of this stable factorization system is generated by the maps $U \to 1$, for all (images of) representables $U$. 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 $U \to 1$ is of the form $A\times U \to A$, which is a colimit of copies of $U \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 $(\infty,1)$-topos consists of sheaves on some cohesive site. Then there is a stable factorization system such that $B \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 $\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 \times U \to A$ as a colimit over projections?

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

$A \simeq {\lim_\to}_i U_i$

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

$(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 \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