Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: externalizing internal discrete fibrations

James Deikun (May 05 2025 at 22:22):

According to this MathOverflow answer, an internal discrete fibration should externalize to a fiberwise discrete fibration, i.e., arrows that are vertical wrt $\mathit{fam}(\mathcal D)$ should have unique lifts while the Cartesian ones don't. But, however much I stare at the diagram of how you externalize a functor:

$$\begin{CD} \Delta @= \Delta @>u>> \Gamma \\ @VxVV @V{f}VV @VV{y}V \\ (\smallint F)_0 @<<{d_F}< (\smallint F)_1 @>>{c_F}> (\smallint F)_0 \\ @V{(\pi_F)_0}VV @V{(\pi_F)_1}VV \textit{pb} @VV{(\pi_F)_0}V \\ \mathcal{D}_0 @<<{d_\mathcal{D}}< \mathcal{D}_1 @>>{c_\mathcal{D}}> \mathcal{D}_0 \\ \end{CD}$$

It still looks like all the morphisms get unique lifts! Which of us is right and why?

Mike Shulman (May 06 2025 at 00:29):

Hmm, at first I think I agree with you. Discreteness of a fibration is equivalently the statement that all of its fibers are discrete sets, and surely that property can be checked fiberwise.

James Deikun (May 06 2025 at 01:29):

I have another line of reasoning that says I'm wrong, though: discrete fibrations with a generic object are slice projections, and a generic object over $\mathbb C$ should lift to $\mathit{Fam}(\mathcal D)$, in which case $\mathit{Fam}(\pi_F)$ is the projection from a slice over an object of $\mathit{Fam}(\mathcal D)$. But in the case $\mathbb C$ is $\mathsf{Set}$, one of those objects is a small formal coproduct of objects of $\mathcal D$, but $\pi_F$ in general should represent any small colimit of objects of $\mathcal D$.

James Deikun (May 06 2025 at 01:30):

So I want to understand which of these lines of reasoning goes wrong, and where.

Mike Shulman (May 06 2025 at 01:49):

What is $\pi_F$?

James Deikun (May 06 2025 at 01:58):

$\pi_F$ is the projection of $\smallint F$ to $\mathcal D$, where $F$ is an internal presheaf. I've edited the diagram where I accidentally referred to it as just $F$. I've edited my response to add a $\mathit{Fam}$ where it was needed too.

Mike Shulman (May 06 2025 at 03:58):

Okay, now what is "the projection to a slice"? Which object is a formal coproduct of which objects? And what do you mean by "should represent any small colimit"?

James Deikun (May 06 2025 at 07:30):

Sorry, should have been projection from a slice. Basically, if a discrete fibration has a generic object, then because lifts are unique the generic object is actually a terminal object in the total category, and the discrete fibration is equivalent to the projection from the slice over the image of the generic object, corresponding to a representable presheaf.

James Deikun (May 06 2025 at 07:32):

Meanwhile, the externalization of an internal category in $\mathsf{Set}$, i.e. an ordinary category, is the ordinary families construction, which doubles as the free coproduct completion for ordinary categories. Therefore an object of the total category of the externalization is a formal coproduct of objects of the "internal" ordinary category.

James Deikun (May 06 2025 at 07:37):

However, an "internal" (i.e. ordinary) discrete fibration with small fibers corresponds to a presheaf on the base, and presheaves on the base are the free small colimit completion of the base, so an ordinary discrete fibration with small fibers should correspond to a formal small colimit of objects in the base, and so therefore should its externalization. So by one argument externalizations of internal discrete fibrations should be formal small coproducts of objects in the ("internal") base, and by another they should be formal small colimits. These things are different, though, so one of the arguments must be wrong.

Mike Shulman (May 06 2025 at 16:28):

I see three different conditions you can impose on an internal discrete fibration over $D$ in Set:

1. It has a generic object internally in Set. In this case it corresponds to an object of $D$.
2. Its externalization has a generic object. In this case it corresponds to a formal coproduct of objects of $D$.
3. No condition at all. In this case it is just a presheaf on $D$, i.e. a formal colimit of objects of $D$.

I don't see any contradiction because these are all different conditions.

James Deikun (May 06 2025 at 16:38):

But it seems to me "its externalization has a generic object" comes automatically, because that happens whenever the domain of the discrete fibration is a small category.

Mike Shulman (May 06 2025 at 16:47):

Why?

James Deikun (May 06 2025 at 18:27):

Well, a generic object $G$ for the domain's own externalization is an set-indexed family $G_i : I_G \to \smallint F$ so that you can obtain any set-indexed family of objects of the domain by reindexing it. This is given by taking $I_G$ to be the set of objects of $\smallint F$ and $G_i$ to be the identity.

A generic object $G'$ for the externalized fibration is a set-indexed family $G'_i : I_{G'} \to \smallint F$ so that you can obtain any set-indexed family of objects of the domain $\smallint F$ as the domain of a (necessarily Cartesian) lift of a map of set-indexed families of objects of $D$. But all the reindexing maps into $G$ as above are (Cartesian) lifts of their images in $\mathit{Fam}(D)$, so $G' = G$ is a generic object of $\mathit{Fam}(\pi_F)$.

Mike Shulman (May 06 2025 at 18:32):

Generic objects are always relative to a particular fibration, not to a particular category. Are you saying that $G$ is a generic object for $\int F \to C$, or for $\int F \to D$, or for $\int F \to \int F$?

James Deikun (May 06 2025 at 18:38):

$G$ is originally a generic object for $\mathit{Fam}(\smallint F) \to C$, but becomes one for $\mathit{Fam}(\smallint F) \to \mathit{Fam}(D)$ as well.

James Deikun (May 06 2025 at 18:43):

In general generic objects ascend along a composition of fibrations: a generic object for a composite fibration is also a generic object for the first (domainward) fibration in the composite, because the Cartesian morphisms of the composite fibration are both Cartesian in the domainward fibration as well as lying over a Cartesian morphism of the codomainward fibration.

Mike Shulman (May 06 2025 at 18:57):

I think an externalization $\mathrm{Fam}(E) \to C$ only has a generic object if it corresponds to a presheaf of sets on $C$, which is to say $E$ is a discrete internal category.

James Deikun (May 06 2025 at 19:09):

The externalization of an internal category is always globally and locally small, and the former means it has a generic object (weak generic object, per Jacobs).

Mike Shulman (May 06 2025 at 19:29):

But a weak generic object doesn't suffice to make a fibration representable unless you already know it's discrete.

James Deikun (May 06 2025 at 19:44):

But you said earlier that you believed that $\pi_F : \mathit{Fam}(\smallint F) \to \mathit{Fam}(D)$ was discrete. Did something change your mind?

James Deikun (May 06 2025 at 19:56):

Maybe representability of a discrete fibration actually requires that it is both globally and locally small, and local smallness does not ascend the same way that global smallness does?

Mike Shulman (May 06 2025 at 20:38):

$\pi_F : \mathrm{Fam}(\int F) \to \mathrm{Fam(D)}$ is discrete, but $\mathrm{Fam}(\int F) \to C$ is not.

James Deikun (May 06 2025 at 21:00):

But I never said or assumed anywhere that $\mathrm{fam}(\smallint F) : \mathrm{Fam}(\smallint F) \to C$ is representable!

Mike Shulman (May 06 2025 at 21:34):

James Deikun said:

$G$ is originally a generic object for $\mathit{Fam}(\smallint F) \to C$

Mike Shulman (May 06 2025 at 21:44):

If what you meant there is a weak generic object, then okay, but in that case it's not true that

James Deikun said:

discrete fibrations with a [weak] generic object are slice projections

James Deikun (May 06 2025 at 21:51):

Ah, so is this then correct?

James Deikun said:

Maybe representability of a discrete fibration actually requires that it is both globally and locally small, and local smallness does not ascend the same way that global smallness does?

Mike Shulman (May 06 2025 at 22:00):

If "globally small" means there exists a weak generic object, then I don't think even global+local smallness is sufficient for representability; that should just imply that it's represented by an internal category rather than an object (= an internal discrete category).

James Deikun (May 06 2025 at 22:49):

Streicher states this without proof at the end of this section.

Mike Shulman (May 06 2025 at 23:00):

States what? The only thing I see at the end of section 9 is a definition of "representable" fibration.

James Deikun (May 06 2025 at 23:03):

One of the four definitions claimed to be equivalent is that the representable fibration is equivalent to a slice projection; another is that it is equivalent to a small (presumably in the "globally small and locally small" sense since it makes no sense if it's the "small fibers" sense) discrete fibration.

Mike Shulman (May 06 2025 at 23:30):

Oh, yes. Sorry, I missed that your statement was assuming discreteness separately. Yes, given a discrete fibration, global+local smallness will ensure that it's representable.

Mike Shulman (May 06 2025 at 23:36):

So I guess you are right, given that $\mathrm{Fam}(\int F) \to \mathrm{Fam}(D)$ is discrete, and globally small because $\mathrm{Fam}(\int F) \to C$ is, it must not be locally small.

James Deikun (May 06 2025 at 23:41):

Are there any general conditions similar to global+local smallness of a fibration that characterize when a map of fibrations over the identity is externalized from an internal functor?

Mike Shulman (May 06 2025 at 23:50):

If its domain and codomain are known to be externalized from internal categories, then every map of fibrations over $C$ is (isomorphic to one) externalized from an internal functor. This is kind of a fancy form of the Yoneda lemma.