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: theory: category theory

Topic: 'free fibrations' of subobjects

Matteo Capucci (he/him) (Jun 26 2023 at 13:38):

I think this might be a cool thing to write somewhere, also to check whether I'm making sense or not.

Any category with pullbacks $\cal C$ admits a fibration of subobjects $\cal C^\subseteq \to C$. When $\cal C$ has a subobject classifier, however, we can say more. In that case we know there is a 'generic subobject' $\top : 1 \to \Omega$ such that every subobject $A \subseteq X$ is given by pullback of $\top$ along a map $\chi_A : X \to \Omega$.
This means, that the fibration $\cal C^\subseteq \to C$ is 'freely generated by' the data of the functor $\mathbf\Omega : 1 \to \cal C$ picking out the subobject classifier $\Omega$. You can see this functor as specifying generators for all the fibers of $\cal C^\subseteq \to C$. In this case it gives us no generator whatsoever in any fiber, except for one in the fiber over $\Omega$. When we 'freely generate' a fibration starting from this data, we start populating the fibers with the objects that ought to be there because are reindexings of the generators we specified. In our case, we only have one generator $\star \in \mathbf\Omega^{-1}(\Omega)$ (I hope notation here is clear: $\mathbf \Omega$ is the functor picking out $\Omega : \cal C$, while $\star:1$ is the only object of the terminal category $1$), so the only stuff we have to add are all the reindexings of $\star$ along every possible morphism into $\Omega$. But by definition every subobject in $\cal C$ is so generated. So we established:

Theorem Let $\cal C$ be finitely complete and have a subobject classifier $^1$. Then its fibration of subobject is freely generated by its subobject classifier, i.e.

$$\cal C^\subseteq \to C \quad \cong \quad C/\Omega \to C$$

(Indeed, for the record, the free fibration over a functor $p:\cal E \to C$ is given by the projection $\cal C/p \to \cal C$, where $\cal C/p$ denotes the comma category)

Is this folklore? I've never seen it anywhere. Looking at it again, it's basically a restatement of the definition of subobject classifier, that says ${\bf Sub}(X) \cong {\cal C}(X, \Omega)$ naturally in $X$: this is roughly what the above isomorphism of fibrations entails, since ${\bf Sub}(X)$ and $\mathcal C(X,\Omega)$ are the set of objects of the fibers of those fibrations. Indeed, the above theorem simply makes this an isomorphism of categories instead of just sets. In other words, it's a representability statement but for fibrations instead of presheaves (i.e. discrete fibrations).

(1) $\cal C$ is not necessarily a topos, we need cartesian closure for that.

John Baez (Jun 26 2023 at 15:32):

Nice! I've never seen someone talk about "freely generated" here, but as you note the isomorphism you give is essentially the definition of a subobject classifier, so it's more a matter of a new attitude than a "result", right? But maybe you could find interesting situations where a fibration is freely generated by more complicated data, thus seeing this as a special case of a pattern.

Mike Shulman (Jun 26 2023 at 16:18):

I don't think this is quite true: the fibers of $\mathcal{C}^{\subseteq}$ are posets, while the fibers of $\mathcal{C}/\Omega$ are discrete sets.

Morgan Rogers (he/him) (Jun 26 2023 at 20:10):

You can view it as an internal poset and that would recover the structure on the fibers, right?

Mike Shulman (Jun 26 2023 at 20:11):

Yep. But then I don't know what "freely generated" means any more.

Josselin Poiret (Jun 27 2023 at 07:47):

Well, you could generalize this to fibrations with posetal fibers, and this would give you the result I assume. Also note that the "free generation" part is really the idea behind Yoneda.

Josselin Poiret (Jun 27 2023 at 07:48):

ie. any internal poset $P$ in $C$ gives you a fibration with posetal fibers $C/P$

Matteo Capucci (he/him) (Jun 27 2023 at 08:08):

Mike Shulman said:

I don't think this is quite true: the fibers of $\mathcal{C}^{\subseteq}$ are posets, while the fibers of $\mathcal{C}/\Omega$ are discrete sets.

Uhm, right... where did I go wrong then?

Josselin Poiret (Jun 27 2023 at 08:08):

I'd expect the same to be true for any Lawvere theory or even essentially algebraic theories

Matteo Capucci (he/him) (Jun 27 2023 at 08:09):

Josselin Poiret said:

I'd expect the same to be true for any Lawvere theory or even essentially algebraic theories

Yeah

Matteo Capucci (he/him) (Jun 27 2023 at 08:33):

It seems one needs $\bf\Omega$ to have the fiber over $\Omega$ be much larger than I say above... In particular $\cal C/\Omega \to C$ has discrete fibers because there are no morphisms in the only non-empty fiber of $\bf\Omega$. I'd suspect one would need the entire subobject poset of $\Omega$ to appear in this generating fiber. In other words, replace $\bf\Omega$ with the diagonal filling this pullback square:
image.png

Matteo Capucci (he/him) (Jun 27 2023 at 08:35):

Though I wonder if the inclusion $\top : \downarrow \to \cal C$, where $\downarrow$ is the walking arrow and $\top$ picks out the whole subobject classifier (i.e., the arrow $\top : 1 \to \Omega$), would suffice... it's appealing but prima facie it doesn't seem to work

Josselin Poiret (Jun 27 2023 at 10:21):

Matteo Capucci (he/him) said:

It seems one needs $\bf\Omega$ to have the fiber over $\Omega$ be much larger than I say above... In particular $\cal C/\Omega \to C$ has discrete fibers because there are no morphisms in the only non-empty fiber of $\bf\Omega$. I'd suspect one would need the entire subobject poset of $\Omega$ to appear in this generating fiber. [...]
image.png

If you have a subobject of $\Omega$, then transporting the generator along its characteristic morphism should give you the corresponding subobject, no?

Matteo Capucci (he/him) (Jun 27 2023 at 12:51):

Yeah the objects are fine but one doest get the inclusions

Mike Shulman (Jun 27 2023 at 14:08):

It's not the subobjects of $\Omega$ that you need, but the ordering relation on morphisms into $\Omega$ induced by its internal poset structure, as Morgan said.

Mike Shulman (Jun 27 2023 at 14:09):

Josselin Poiret said:

Well, you could generalize this to fibrations with posetal fibers, and this would give you the result I assume. Also note that the "free generation" part is really the idea behind Yoneda.

Exactly, but once you're talking about incorporating a specified order relation on an object, there isn't a Yoneda lemma any more, which is why I'm unsure of what the statement would be.

Josselin Poiret (Jun 27 2023 at 15:37):

Mike Shulman said:

Exactly, but once you're talking about incorporating a specified order relation on an object, there isn't a Yoneda lemma any more, which is why I'm unsure of what the statement would be.

Oh, you're right, let me add some emphasis for other readers: a Yoneda-like lemma would work if you freely generated both the presheaf and poset parts of the posetal fibration, which isn't the case here since we only generate the presheaf part, the preorder part is fixed ahead of time!
I guess we don't want $Sub(C)$ to be too freely generated, only its presheaf part.

Josselin Poiret (Jun 27 2023 at 15:50):

Mike Shulman said:

I don't think this is quite true: the fibers of $\mathcal{C}^{\subseteq}$ are posets, while the fibers of $\mathcal{C}/\Omega$ are discrete sets.

instead of the bare $C/Ω$, you probably want the externalisation of the internal category $Ω$, as described in Categorical Logic and Type Theory's 7.3, and that should all work out.

Josselin Poiret (Jun 27 2023 at 15:55):

it might just be the right way to talk about subobject classifiers in a category with chosen pullbacks, since otherwise you sweep all the 2-details under the rug

Josselin Poiret (Jun 27 2023 at 15:58):

(and very importantly, we have an equivalence $\mathrm{Extern}_\mathcal{C}(\Omega) \simeq \mathcal{C}^\subseteq$ and not just an isomorphism)

Josselin Poiret (Jun 27 2023 at 16:02):

additionally, for any object $c \in \mathcal{C}$, you can form the internal discrete category with both $C_0, C_1 = c$, and externalizing it recovers $\mathcal{C}/c$.