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: co/limit when diagram has initial/terminal objects

Matteo Capucci (he/him) (Nov 23 2020 at 19:27):

I can't believe I'm asking a question about conical co/limits, but here we go.
Suppose I'm computing the colimit of a diagram indexed by a lattice. This means I have all sorts of amenities, included a top and bottom elements.
If the ambient category is co/complete, is it true than $\lim F = F(\bot)$ and $\mathrm{colim} F = F(\top)$?
This seems easily provable by checking the universal property: if I have a cone $\{L \to F(i)\}_{i \in I}$, for example, then there's in particular an arrow $L \to F(\bot)$, and by initiality of $\bot$ in $I$, then every other arrow $L \to F(i)$ factors through $F(\bot) \to F(i)$. Voilà.
Dually, we prove $\mathrm{colim} F = F(\top)$.
Actually, the proof only required that $I$ was a bounded category, i.e. that we have a terminal $\top$ and an initial $\bot$ object.
But now...
A continuous map $f:X \to Y$ induces a functor $f^!:Psh X \to Psh Y$, the 'inverse image' functor, which is given by

$$f^!(G)(V) = \mathrm{colim}_{U \subset f^{-1} V} G(U)$$

Look at the indexing of the colimit: it's the downset of $f^{-1}(V)$ in the frame $\mathcal O(X)$. It is not a lattice, but it surely is bounded: below, by $\varnothing$, above, by $\mathrm{int} f^{-1}V = \bigcup_{U \subset f^{-1} V} U$. Remember now that presheaves are contravariant, hence the colimit we want to compute is indexed by the opposite of this order, with the effect that $\top = \varnothing$ and $\bot = \mathrm{int}f^{-1}V$.
Hence by the above reasoning, we should have $f^!(G)(V) = G(\top) = G(\varnothing)$, which is... absurd?

Tim Hosgood (Nov 24 2020 at 08:53):

isn't the inverse image given by a limit, not a colimit?

Tim Hosgood (Nov 24 2020 at 08:54):

$\lim_{V\supseteq f(U)}$

Morgan Rogers (he/him) (Nov 24 2020 at 10:10):

I started answering your question, but then realised how much your notation is confusing:
Matteo Capucci said:

A continuous map $f:X \to Y$ induces a functor $f^!:Psh X \to Psh Y$

What are $X$ and $Y$ here? Topological spaces? If so, are you writing $\mathbf{PSh}(X)$ for the presheaves on the frame of opens $\mathcal{O}(X)$?

Morgan Rogers (he/him) (Nov 24 2020 at 10:30):

Assuming that my interpretations above are correct, the continuous map induces a frame hom/functor $f^{\#}: \mathcal{O}(Y) \to \mathcal{O}(X)$, and it is this in turn which induces an essential geometric morphism, which I'll call $g:\mathbf{PSh}(Y) \to \mathbf{PSh}(X)$ to avoid confusion. The inverse image functor of this geometric morphism is the functor $g^*: \mathbf{PSh}(X) \to \mathbf{PSh}(Y)$ which restricts along $f^{\#}$. This has a left adjoint $g_!:\mathbf{PSh}(Y) \to \mathbf{PSh}(X)$ which is given by a formula a lot like what you wrote,
$G \mapsto \left( U \mapsto \mathrm{colim}_{\left(U \subseteq f^{\#}(V)\right)^{\mathrm{op}}} G(V) \right),$
but notice that the variable in the colimit is $V$ rather than $U$ (I included the op to indicate that the ordering is reversed, as you also noted). The problem that you described evaporates immediately.

Morgan Rogers (he/him) (Nov 24 2020 at 10:31):

That said... why are you looking at presheaves on these things rather than sheaves? :joy:

Matteo Capucci (he/him) (Nov 24 2020 at 10:45):

[Mod] Morgan Rogers said:

I started answering your question, but then realised how much your notation is confusing:
Matteo Capucci said:

A continuous map $f:X \to Y$ induces a functor $f^!:Psh X \to Psh Y$

What are $X$ and $Y$ here? Topological spaces? If so, are you writing $\mathbf{PSh}(X)$ for the presheaves on the frame of opens $\mathcal{O}(X)$?

Yes, isn't this the standard notation for presheaves on topological spaces?

Matteo Capucci (he/him) (Nov 24 2020 at 10:46):

[Mod] Morgan Rogers said:

Assuming that my interpretations above are correct, the continuous map induces a frame hom/functor $f^{\#}: \mathcal{O}(Y) \to \mathcal{O}(X)$, and it is this in turn which induces an essential geometric morphism, which I'll call $g:\mathbf{PSh}(Y) \to \mathbf{PSh}(X)$ to avoid confusion. The inverse image functor of this geometric morphism is the functor $g^*: \mathbf{PSh}(X) \to \mathbf{PSh}(Y)$ which restricts along $f^{\#}$. This has a left adjoint $g_!:\mathbf{PSh}(Y) \to \mathbf{PSh}(X)$ which is given by a formula a lot like what you wrote,
$G \mapsto \left( U \mapsto \mathrm{colim}_{\left(U \subseteq f^{\#}(V)\right)^{\mathrm{op}}} G(V) \right),$
but notice that the variable in the colimit is $V$ rather than $U$ (I included the op to indicate that the ordering is reversed, as you also noted). The problem that you described evaporates immediately.

:face_palm: How foolish!! It never occured to me I was using the wrong variable

Matteo Capucci (he/him) (Nov 24 2020 at 10:46):

Of course, it makes much more sense now

Matteo Capucci (he/him) (Nov 24 2020 at 10:46):

[Mod] Morgan Rogers said:

That said... why are you looking at presheaves on these things rather than sheaves? :joy:

Hahaha one thing at a time

Matteo Capucci (he/him) (Nov 24 2020 at 10:47):

Now that I straightened this out, I can flood you with the sheaf (of) questions

Morgan Rogers (he/him) (Nov 24 2020 at 10:50):

Hahaha sure! But beware that on toposes of sheaves, the continuous maps induce ordinary geometric morphisms, so the left adjoint $g_!$ doesn't typically exist.

Matteo Capucci (he/him) (Nov 24 2020 at 10:51):

Yeah this I know. You can sheafify the inverse image, though, right? Then you get the geometric morphism $Sh X \to Sh Y$ induced by $f: X \to Y$

sarahzrf (Nov 25 2020 at 07:04):

Tim Hosgood said:

isn't the inverse image given by a limit, not a colimit?

probably you have been misled by the notation where people write "lim" for both colimits and limits

Tim Hosgood (Nov 25 2020 at 08:33):

sarahzrf said:

Tim Hosgood said:

isn't the inverse image given by a limit, not a colimit?

probably you have been misled by the notation where people write "lim" for both colimits and limits

...this is probably entirely true :upside_down:

Matteo Capucci (he/him) (Nov 25 2020 at 10:35):

Very subtle. I usually read them by remembering that limits have an arrow in the opposite direction of the one used by analysts

Morgan Rogers (he/him) (Nov 25 2020 at 11:31):

$\mathrm{colim}$ all the way. lim underlined with an arrow in one direction or the other is an arbitrary convention which is not immediately decipherable to someone encountering it for the first time.

Nathanael Arkor (Nov 25 2020 at 11:40):

Or after the twentieth time, for some of us :upside_down:

Reid Barton (Nov 25 2020 at 12:17):

It's also more visually cluttered since there's usually other stuff written under the $\lim$. I think the notation with the arrow made more sense back when it was mainly used for sequential (co)limits.

Jens Hemelaer (Nov 25 2020 at 13:08):

I still use $\stackrel{\lim}{\to}$, it helps to remind myself that it is a filtered colimit and not just any colimit.

sarahzrf (Nov 25 2020 at 14:33):

Tim Hosgood said:

sarahzrf said:

Tim Hosgood said:

isn't the inverse image given by a limit, not a colimit?

probably you have been misled by the notation where people write "lim" for both colimits and limits

...this is probably entirely true :upside_down:

possibly mnemonic: inverse image is left adjoint to direct image, so it's a colimit thing

sarahzrf (Nov 25 2020 at 14:34):

...this is slightly bullshit, since the formula for left adjoints given by the AFT is a limit... but on the other hand, inverse image is also [sheafification of] a left kan extension, and that is a colimit!

Todd Trimble (Nov 29 2020 at 18:23):

Direct image $\exists_f: PX \to PY$ is left adjoint to inverse image $f^\ast: PY \to PX$. It's true that $f^\ast$ has a right adjoint $\forall_f: PX \to PY$ as well, taking $U \subseteq X$ to $\{y: Y| \forall_{x: X}\; f(x) = y \Rightarrow x \in U\}$. I don't know what people call that, but it's not "coimage".

Dan Doel (Nov 29 2020 at 18:29):

Dependent product. :)

Todd Trimble (Nov 29 2020 at 18:31):

That's true! But there should be a home-y term that refers to the posetal or propositional case like this.

John Baez (Nov 29 2020 at 23:04):

@Christian Williams has been looking around for a name for

$\forall_f (U) = \{y: Y| \forall_{x: X}\; f(x) = y \Rightarrow x \in U\} \subseteq Y$

when $f: X \to Y$ is a function and $U \subseteq X$.

I think he's calling it the "saturated image", but he doesn't love that term. It's weird that there isn't a well-established "homey" name for it.

Fawzi Hreiki (Nov 29 2020 at 23:16):

Well at the ‘untruncated’ level of slice categories, it corresponds to the dependent product which in turn corresponds to the exponential in the slice

Fawzi Hreiki (Nov 29 2020 at 23:17):

So maybe ‘implicational image’ if you don’t want to call it the universal quantifier

Fawzi Hreiki (Nov 29 2020 at 23:21):

Or ‘constrained image’ since it selects the largest subset of Y which still fits within the stated requirement

John Baez (Nov 29 2020 at 23:29):

I like the name 'constrained image'. Anyone who has never thought about it before should find examples where the constrained image properly contains the usual image.

Dan Doel (Nov 30 2020 at 00:12):

I don't know if any name involving "image" is really going to be great. If $X = 0$, $f$ is the empty function, and $∀_f(U) = Y$, no?

John Baez (Nov 30 2020 at 00:16):

Right. You gave away the answer to my puzzle.

Dan Doel (Nov 30 2020 at 00:16):

Sorry. :smile:

Dan Doel (Nov 30 2020 at 00:18):

Anyhow, it's a little odd to call something an 'image' when it contains things that aren't involved in the $f$ mapping.

John Baez (Nov 30 2020 at 00:20):

Yes, this happens rather rarely... but I think the main problem is that nobody has thought of a better word yet!

Fawzi Hreiki (Nov 30 2020 at 01:28):

What about 'essentialization'? For any map $f: X \rightarrow Y$ in a topos $\mathscr{E}$ we have an essential geometric morphism $(\sum_f \dashv f^* \dashv \prod_f) : \mathscr{E}/X \rightarrow \mathscr{E}/Y$. The dependent product extracts the space of sections which, when truncated down to logic, corresponds to the 'space of implications' - i.e. the universal quantifier.

sarahzrf (Nov 30 2020 at 05:29):

it's the far left adjoint that makes it essential, tho

sarahzrf (Nov 30 2020 at 05:29):

if anything, ∀_f should be called "direct image"

sarahzrf (Nov 30 2020 at 05:30):

unfortunate conventions...

Dan Doel (Nov 30 2020 at 05:39):

But it's not the direct image, as my spoiler shows.

Dan Doel (Nov 30 2020 at 05:51):

It's like the base of the fibers of $f$ covered by $U$.

sarahzrf (Nov 30 2020 at 05:52):

no, the problem is that "direct image" is not very much like "image"

sarahzrf (Nov 30 2020 at 05:52):

it's right adjoint to inverse image

sarahzrf (Nov 30 2020 at 05:53):

whoever coined the term in the early days of sheaf theory doomed us all

Dan Doel (Nov 30 2020 at 05:53):

I thought the "image" was the direct image.

sarahzrf (Nov 30 2020 at 05:53):

i'm talking about "direct image" of sheaves, or more generally the "direct image" part of a geometric morphism

sarahzrf (Nov 30 2020 at 05:55):

example: if you have a space X and a sheaf F on X, then taking the direct image of F along the terminal map X → 1 gives you a sheaf on 1—a set. and that set is the set of global sections of F

Dan Doel (Nov 30 2020 at 05:57):

Okay, so someone just called the dependent product the "direct image" for some reason?

sarahzrf (Nov 30 2020 at 05:57):

yup!

sarahzrf (Nov 30 2020 at 05:57):

it's cursed

sarahzrf (Nov 30 2020 at 05:57):

indeed, what you wrote is quite literally true

sarahzrf (Nov 30 2020 at 05:58):

in a base change geometric morphism, the direct image functor is literally dependent product

sarahzrf (Nov 30 2020 at 05:58):

why is this name used? i do not know

sarahzrf (Nov 30 2020 at 05:58):

blame the french, probably

sarahzrf (Nov 30 2020 at 06:03):

ive been confused by this rather badly myself before

Dan Doel (Nov 30 2020 at 06:03):

I don't know much sheaf stuff, but I can't really think of an explanation given the stuff I do know. Like, you might think that it has to do with just adjoining the X → 1 in the same direction, but that would also give you Σ.

sarahzrf (Nov 30 2020 at 06:05):

i think it's just that a map f : X → Y induces functors Sh(Y) → Sh(X) and Sh(X) → Sh(Y), so logically we should call them "inverse image" and "direct image" because you are moving sheaves along f and you want to indicate the direction

sarahzrf (Nov 30 2020 at 06:05):

unfortunately it just so happens that the manner in which you are moving it along f is entirely different from the usual connotation of "image"

Dan Doel (Nov 30 2020 at 06:06):

I guess it might have helped if $∀_f$ already had a name.

sarahzrf (Nov 30 2020 at 06:06):

yeah

sarahzrf (Nov 30 2020 at 06:07):

for sheaves, maybe if there were in general two functors Sh(X) → Sh(Y) like there are for slice categories, then "direct image" maybe wouldve gotten applied to the left adjoint of inverse image instead of the right adjoint

sarahzrf (Nov 30 2020 at 06:07):

but you generally have a right adjoint to inverse image, and you dont always have a left adjoint

sarahzrf (Nov 30 2020 at 06:07):

so

sarahzrf (Nov 30 2020 at 06:08):

actually, do you know much about locales

Dan Doel (Nov 30 2020 at 06:08):

Just vague stuff.

sarahzrf (Nov 30 2020 at 06:09):

ah

sarahzrf (Nov 30 2020 at 06:09):

(if you did, i was gonna encourage you to attack grothendieck topos & sheafy stuff as an immediate categorification of locale stuff)

John Baez (Nov 30 2020 at 07:09):

I too was confused for a while, thinking "direct image" should be like the usual "image" of a function.

Matteo Capucci (he/him) (Nov 30 2020 at 10:36):

+1 to 'direct image' is very bad terminology

Matteo Capucci (he/him) (Nov 30 2020 at 10:37):

John Baez said:

Christian Williams has been looking around for a name for

$\forall_f (U) = \{y: Y| \forall_{x: X}\; f(x) = y \Rightarrow x \in U\} \subseteq Y$

when $f: X \to Y$ is a function and $U \subseteq X$.

I think he's calling it the "saturated image", but he doesn't love that term. It's weird that there isn't a well-established "homey" name for it.

'coinverse image'? :laughing:

Matteo Capucci (he/him) (Nov 30 2020 at 10:39):

Or 'coconstrained image' since you are constraining in the domain. You are looking for those $y \in Y$ whose fiber lies in $U$.

Dan Doel (Nov 30 2020 at 15:15):

'Coinverse' doesn't really tell you whether the left or right adjoint is meant.

Fawzi Hreiki (Nov 30 2020 at 15:22):

Truth be told, I don't see what's wrong with just 'universal quantification'

Fawzi Hreiki (Nov 30 2020 at 15:23):

People don't call the existential quantifier the direct image just because they wanted to give it a new name, but because it turned out that two seemingly different things coincided

sarahzrf (Nov 30 2020 at 15:34):

they don't call it the direct image at all, they just call it the image

sarahzrf (Nov 30 2020 at 15:34):

"direct image" is something totally different

sarahzrf (Nov 30 2020 at 15:34):

\>_<

Dan Doel (Nov 30 2020 at 15:35):

No, people do call it the direct image.

sarahzrf (Nov 30 2020 at 15:36):

really?

sarahzrf (Nov 30 2020 at 15:36):

huh, i'm not sure i've seen that

Dan Doel (Nov 30 2020 at 15:46):

I imagine many more people than the ones that are using the sheaf terminology, because there are a lot more people who know basic set theory, and might want extra disambiguation between 'image' and 'inverse image'. Maybe it's outdated if you ask practicing mathematicians, but I doubt it's really uncommon.

sarahzrf (Nov 30 2020 at 15:48):

i dunno about "outdated", i'm just not sure it would've ever occurred to me to say "direct image" to disambiguate if i'd never seen the sheaf term

sarahzrf (Nov 30 2020 at 15:48):

it doesnt seem like a blatantly obvious term

sarahzrf (Nov 30 2020 at 15:48):

fair enough though

Dan Doel (Nov 30 2020 at 16:55):

Personally I kind of think 'image' is a better name than 'existential quantifier', for this specific thing, too, and therefore don't love 'universal quantifier' either. Going along arbitrary functions mixes in stuff that would be orthogonal in the logic. It kind of feels coincidental, like particular constructions of things in 'material' set theory.

Todd Trimble (Nov 30 2020 at 17:12):

Confirming what Dan said about the set-theoretic image being commonly called "direct image". Anyway, image is a pretty good word for it; it's like a shadow from a light projection.

John Baez (Nov 30 2020 at 17:31):

The word "image" is great. It couldn't be replaced by "existential quantifier", since although the image is defined using an existential quantifier, people use "existential quantifier" to mean this:

$\exists$

Fawzi Hreiki (Nov 30 2020 at 17:52):

Sure that's true, but in what context does universal quantification $\forall_f: \mathcal{P}X \rightarrow \mathcal{P}Y$ along a map $f: X \rightarrow Y$ arise where we aren't thinking of it from a logical point of view?

Fawzi Hreiki (Nov 30 2020 at 17:54):

Also, the idea that the image is defined using an existential quantifier depends on the perspective you're taking. Working in a category, we only get the existential quantifier in the internal language once we have the image operator.

John Baez (Nov 30 2020 at 17:55):

It arises in computer security - that's why @Christian Williams cares about it. Sometimes you want to know that the only way you could have gotten something is from a safe source. That is, the only way we can write some $y \in Y$ as $f(x)$ is for $x$ in some chosen subset $U \subseteq X$.

John Baez (Nov 30 2020 at 17:56):

So it's like the "safe image" or "secure image"... but maybe we should throw out the word "image" and come up with some better metaphor.

Jules Hedges (Nov 30 2020 at 18:03):

It's sometimes called "demonic nondeterminism" where you assume the worst possible thing happens (in contrast to "angelic nondeterminism")

John Baez (Nov 30 2020 at 18:04):

Okay, I'm happy with "demonic image". :smiling_devil:

Fawzi Hreiki (Nov 30 2020 at 18:05):

I still think that if you want a 'geometric' word for the universal quantifier, something involving sections would make sense

John Baez (Nov 30 2020 at 18:05):

I was joking about "demonic image". I'd be happy with some sort of geometric metaphor. Something about sections might make sense.

Todd Trimble (Nov 30 2020 at 18:24):

I'm somewhat reluctant to say this, but here goes: if you take ordinary projections $\pi: X \times Y \to Y$ is the "ur-examples" of functions that you quantify with respect to (e.g., John's $\exists_{x: X}$ applied to predicates $P(x, y)$ corresponds to $\pi(U)$ where $U = [P(x, y)]$ is the extension of $P$ as a subset of $X \times Y$), then $\forall_{x: X}$ corresponds to the operation taking $U$ to the greatest $V \subset Y$ such that the "tube" through $V$, namely $X \times V$, is completely contained in $U$. Unfortunately, I can't seem to think of anything except "intubation" (which is horrible). Anyway, we could use some imagery here, rather than just some technical-sounding term.

Fawzi Hreiki (Nov 30 2020 at 18:29):

The idea makes sense but 'intubation' sounds like a medical term I probably wouldn't want to look up

Fawzi Hreiki (Nov 30 2020 at 18:30):

Ok so I looked it up and apparently it actually is a technical term for a medical procedure

Dan Doel (Nov 30 2020 at 18:30):

Yeah, it's when they put a tube into your lungs to help you breathe.

Dan Doel (Nov 30 2020 at 18:33):

My complaint was that those are the cases where it makes sense to say 'universal/existential quantification,' but then generalizing those phrases to arbitrary functions rather than π makes less sense. So trying to come up with a different name based on the special case doesn't seem like an optimal strategy. (And same with 'dependent product/sum' really.)

Fawzi Hreiki (Nov 30 2020 at 18:37):

I don't see why quantification along a general map (as opposed to a projection or a diagonal) should have a different name

Fawzi Hreiki (Nov 30 2020 at 18:38):

Likewise, not all bundles are trivial bundles, so not all dependent sum and products are along projections either

Dan Doel (Nov 30 2020 at 18:39):

Logic doesn't have quantification along general maps. It's just what category theorists decided to use to interpret the cases that are actually in logic.

Fawzi Hreiki (Nov 30 2020 at 18:41):

Well now it depends what you mean by 'logic'. From the narrower syntactic point of view, sure, but logic is not constrained to what can be presented via generators and relations the same way group theory isn't just about group presentations

Fawzi Hreiki (Nov 30 2020 at 18:43):

Also, I can't remember what reference this is from, but if you have quantification along projections and diagonals in a given hyperdoctrine, you have quantification along all maps.

Dan Doel (Nov 30 2020 at 18:46):

Then hyperdoctrine's can't faithfully handle logics where 'existential quantification' isn't conflated with other things.

Todd Trimble (Nov 30 2020 at 18:46):

I agree with Fawzi here. There is a particular way of reducing the categorical logician's $\forall_f$ to constructions familiar to traditional logicians, but following Lawvere's "quantifiers are adjoints", I think we should treat $\forall_f$ as having logical status. Quantifying along the diagonal for example is bound up with equality as a logical notion.

Dan Doel (Nov 30 2020 at 18:47):

And which may lack those other things but have existential quantification.

Fawzi Hreiki (Nov 30 2020 at 18:48):

I think you're taking an unnecessarily narrow view of quantification here. What you call conflation isn't in itself a bad thing - its often how new connections are made in mathematics.

Fawzi Hreiki (Nov 30 2020 at 18:49):

So long as something still satisfies the required formal properties (which quantification along a general map does) conflation actually just means more generality (and thus applicability).

Fawzi Hreiki (Nov 30 2020 at 18:53):

The same way it was good when were finally able to identify the square root of 2 with the notion of number (which until then meant just rational number). What is a fraction anyway if not a presentation of a complex number via two integers?

Jonas Frey (Dec 03 2020 at 15:39):

John Baez said:

Christian Williams has been looking around for a name for

$\forall_f (U) = \{y: Y| \forall_{x: X}\; f(x) = y \Rightarrow x \in U\} \subseteq Y$

when $f: X \to Y$ is a function and $U \subseteq X$.

I think he's calling it the "saturated image", but he doesn't love that term. It's weird that there isn't a well-established "homey" name for it.

pushforward? I think that's used in geometry as an alternative to "direct image"

Jonas Frey (Dec 03 2020 at 15:58):

sarahzrf said:

no, the problem is that "direct image" is not very much like "image"

it's right adjoint to inverse image

It becomes left adjoint if you consider as ambient 2-category $\mathrm{TopLex}^{\mathsf{co}}$, the co-dual of the 2-category of toposes and lex functors. I know it sounds ridiculous, but that's how you can think about geometric morphisms as "maps" in a proarrow equipment, see [1,2].

I'm not saying that that's the justification for the term "direct image", or that it's good terminology.

[1] Wood, R. J. (1985). Proarrows ii. Cahiers de topologie et géométrie différentielle catégoriques, 26(2), 135-168.
[2] Rosebrugh, R., & Wood, R. J. (1984). Cofibrations in the bicategory of topoi. Journal of Pure and Applied Algebra, 32(1), 71-94.