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: inverse image

Christian Williams (Dec 12 2022 at 21:38):

We normally think of transformation as going "forward": we plug in a domain pair $x:X, y:Y$ to get a map $Q(x,y)\to R(fx,gy)$ inf-fro.png

Christian Williams (Dec 12 2022 at 21:40):

Yet by inverse image, we can also think of them flowing backward: inf-inv.png

Christian Williams (Dec 12 2022 at 21:41):

Over each codomain pair $a:A, b:B$ there are categories $f^\ast a$ and $g^\ast b$.

Christian Williams (Dec 12 2022 at 21:43):

Over each relation (profunctor) element $s:S(a,b)$, a relation $\gamma^\ast(s)$ from $f^\ast a$ to $g^\ast b$, defined $\gamma^\ast s(r) = [\gamma(r)=s]$.

Christian Williams (Dec 12 2022 at 21:45):

This forms a "mirror world": transformations are equivalent to diagrams of relations in Cat. inv-equiv.png

Christian Williams (Dec 12 2022 at 21:48):

I'm gonna pause here.

Christian Williams (Dec 12 2022 at 21:57):

This "mirror" is functorial: a commutative square of transformations is equivalent to an indexed transformation in Cat.
arr-cat.png ind-cat.png

Christian Williams (Dec 12 2022 at 21:59):

The first picture is a square in the arrow double category of Cat:

• objects are functors ($X\to X_0$ etc)
• tight/verticals are commuting squares $(f,f_0)$;
• loose/horizontals are transformations ($Q\Rightarrow Q_0$), and
• squares are commutative squares of transformations (whole picture).

Christian Williams (Dec 12 2022 at 22:04):

In the second picture:

• an object is an "indexed category" (a lax functor from a category into Cat, $X:X_0\to \mathrm{Cat}$);
• a tight/vertical is an indexed functor (a lax transformation $f:f_0\to \mathrm{Cat}_{fun}$);
• a loose/horizontal is an indexed profunctor (a "bimodule" of lax functors $Q:Q_0\to \mathrm{Cat}_{prof}$)
• a square is an indexed transformation (a transformation of bimodules, the whole picture)

Christian Williams (Dec 12 2022 at 22:19):

An indexed category is equivalent to a functor via collage: connecting two categories (fibers) by a profunctor, by turning elements into morphisms. collage-0.png

Christian Williams (Dec 12 2022 at 22:23):

Any way, I guess I'll pause. I just want to talk to anyone about this stuff.

Christian Williams (Dec 12 2022 at 22:55):

In this double category, fibrations are the indexed conjoints: a representation is a choice of cartesian morphisms. fib-conj.png

Christian Williams (Dec 12 2022 at 22:55):

Dually, an opfibration is an indexed companion. opfib-comp.png

Christian Williams (Dec 13 2022 at 01:20):

So we can draw an opfibration (and a relation thereof) as a big companion: for each base object a fiber category, and for each base morphism a companion.
opfib-bigcomp.png opfib-bigcomp-1.png

Christian Williams (Dec 13 2022 at 01:26):

I think opfibrations are big companions in a way like how existentials are big disjunctions.

Christian Williams (Dec 13 2022 at 01:34):

Dually, we can draw fibrations as big conjoints.
fib-bigconj.png

Christian Williams (Dec 13 2022 at 18:09):

I know many here care about indexed categories; so I'm proposing a perspective of them.
What do you think about this idea? : Fibrations are indexed conjoints.
fib-conj.png

Christian Williams (Dec 13 2022 at 18:10):

(If anything above is not clear, I'm happy to discuss.)

Morgan Rogers (he/him) (Dec 13 2022 at 18:47):

Without having examined it especially closely, I'll just say it seems credible. There is an implicit "but so what?" in that response which I suspect is why I'm the first one to reply. You've given no examples or consequences of this perspective, and hence there's not much to engage with here. Don't take that too critically; rather, I wonder what you're expecting people to respond to "what do you think about this idea?"

Christian Williams (Dec 13 2022 at 18:55):

I mean first I just want to see if people understand the idea. I think it is a clear "global view" of fibrations; rather than defining in terms of individual cartesian morphisms, we can zoom out and see that they all together form a representation of a profunctor.

Christian Williams (Dec 13 2022 at 19:02):

There are many reasons this is a very useful perspective, which I was posting here but then deleted --- if I just go on ahead, then people don't want to read a big thread and then I'm talking to myself. So I at least need to know if some people are understanding.

Mike Shulman (Dec 13 2022 at 19:12):

If you're giving a talk (especially an in-person one), then your audience is more or less captive, so it can sometimes work out to first describe something, make sure everyone understands it, and then afterwards talk about why it's interesting. But in this format, I think if people see a long description of some structure without any motivation or examples, they're likely to just go away.

Mike Shulman (Dec 13 2022 at 19:12):

(It's usually a better idea to lead with examples and motivation in a talk, too, but you're more likely to get away with postponing them in that format.)

Christian Williams (Dec 13 2022 at 19:18):

The whole idea is summarized in the one picture above. That is all I'm proposing.

Christian Williams (Dec 13 2022 at 20:26):

The motivation/application:

• Fib is a double category, not just a 2-category. I am introducing the concept of fibered profunctor.
• Because fibrations and their profunctors are "indexed conjoints", Fib only has conjoints and not companions. That is a serious limitation to their formal theory. So the question is "How do opfibrations and fibrations fit together, to form a complete logic of indexed categories?"

Christian Williams (Dec 13 2022 at 20:28):

In most of mathematics, we are reasoning inside of one indexed category, such as the subobject fibration of a topos. I am talking about constructing a logic in which we can reason across all indexed categories at once.

Christian Williams (Dec 13 2022 at 20:36):

(If you're thinking "but we already knew about Fib", I am saying that profunctors are essential, the same way that they're essential to ordinary category theory.)

Mike Shulman (Dec 13 2022 at 20:40):

I'm looking forward to talking more about mathematics with you in January; here I was just replying briefly to the meta-discussion about the usefulness of examples to convince people to engage with an idea. In this case, it might be useful to have specific examples of arguments (at the level of concreteness like "consider the fibration of modules over rings of characteristic zero") where it's essential to use the full double category structure of Fib.

Christian Williams (Dec 13 2022 at 21:00):

Yes, I am as well. And yes that would be ideal, but I'm just one person; all my energy so far has been toward theory and general exposition. So right now this "retelling the story of a concept" is what I can offer, which I think is still valuable for some people.

Christian Williams (Dec 13 2022 at 21:01):

But yes, it will be great to start thinking of good examples of "inter-universal reasoning".

Matteo Capucci (he/him) (Dec 13 2022 at 22:24):

Christian Williams said:

I know many here care about indexed categories; so I'm proposing a perspective of them.
What do you think about this idea? : Fibrations are indexed conjoints.
fib-conj.png

That's a cool way to put it!
I'm used to think of fibrations as coming from 'especially nice' functors $\bf A \to Prof$ nowadays, to this perspective resonates with me (and it's somewhat known): when your reindexing profunctors have conjoints (= come from reindexing functors), then you get fibrations.

Matteo Capucci (he/him) (Dec 13 2022 at 22:25):

Re the rest, I'm personally not extremely at ease with the diagrams you post so it's hard to follow the reasoning.

Matteo Capucci (he/him) (Dec 13 2022 at 22:26):

Christian Williams said:

We normally think of transformation as going "forward": we plug in a domain pair $x:X, y:Y$ to get a map $Q(x,y)\to R(fx,gy)$ inf-fro.png

I'm basically stuck here already. I'm sure at gunpoint I could find how to read it, but as Mike pointed out, the format is such after a few seconds of staring I move to something else :/ this does not imply a judgment on your research, of course

Christian Williams (Dec 13 2022 at 23:17):

Great! I'm glad you think so too.

Christian Williams (Dec 13 2022 at 23:22):

The diagram is a transformation of profunctors $\gamma: R\Rightarrow S(f,g)$.

A profunctor is a matrix of sets, which we can draw as a string: writing indices $x:X, y:Y$ on each side determines the set $R(x,y)$.
mat.png mat-ij.png

In the same way, the transformation is a matrix of functions, so once we write $x,y$ on top, the diagram represents the function $\gamma(x,y):R(x,y)\to S(fx,gy)$.

Then last, we can plug in a specific $r:R(x,y)$ by writing on the top string $R$, and it is then transformed into $\gamma(r):S(fx,gy)$ on bottom.
inf0.png inf1.png inf-fro.png

Matteo Capucci (he/him) (Dec 14 2022 at 11:24):

I see

Matteo Capucci (he/him) (Dec 14 2022 at 11:24):

Is this a diagram in $\bf Set$-$\bf Mat$?

Christian Williams (Dec 14 2022 at 18:35):

no, it's a transformation. a square in Cat = Mnd(Mat(Set)).

Jean-Baptiste Vienney (Dec 14 2022 at 21:57):

This formula looks interesting but I'm completely lost. So could you really decipher everything? I'd say intuitively that Mat(Set) is the category with objects the nonnegative integers and morphisms $n \rightarrow p$ the matrices $n\times p$ of sets but you can't compose them so what is it? Is it a monoidal category and when you take the category of monoids in this category it gives you the category of categories and functors?

Christian Williams (Dec 14 2022 at 22:44):

Mat(Set) is a double category.

The "category of objects" is that of sets and functions - the left and right halves of the picture, $f:X\to A$ and $g:Y\to B$.

The "category of morphisms" is that of matrices of sets and matrices of functions - the middle of the picture, $\gamma: Q\Rightarrow R$.

Christian Williams (Dec 14 2022 at 22:45):

Vertical composition is function composition. Horizontal composition is matrix composition.

Christian Williams (Dec 14 2022 at 22:48):

A monad in Mat(Set) is a category: a set of objects indexing a matrix of hom-sets. I was drawing a square in Cat=Mnd(Mat(Set)) to think about "inverse image of a transformation".

Martti Karvonen (Dec 15 2022 at 01:45):

Christian Williams said:

Vertical composition is function composition. Horizontal composition is matrix composition.

How are the sums in matrix multiplication interpreted?

Christian Williams (Dec 15 2022 at 04:53):

coproduct of sets.

Matteo Capucci (he/him) (Dec 15 2022 at 10:56):

Christian Williams said:

no, it's a transformation. a square in Cat = Mnd(Mat(Set)).

yeah a square, but why Cat?

Matteo Capucci (he/him) (Dec 15 2022 at 10:57):

mmh I see, I was confused by terminology

Matteo Capucci (he/him) (Dec 15 2022 at 10:57):

Christian Williams said:

Yet by inverse image, we can also think of them flowing backward: inf-inv.png

Ok now unpack this :laughing: what is 'inverse image' here?

Christian Williams (Dec 15 2022 at 16:30):

It's the theorem you already know about - inverse image of a functor determines a lax functor to Cat. The new aspect here is that we can do the same for transformations, because they're essentially just "functors of heteromorphisms".

Inverse image of each heteromorphism gives a profunctor from its domain fiber to its codomain fiber $\gamma^\ast(s): f^\ast(a)\to g^\ast(b)$. This indexed profunctor forms a "lax bimodule" $\gamma^\ast$ between lax functors $f^\ast$ and $g^\ast$.

Martti Karvonen (Dec 15 2022 at 20:51):

Christian Williams said:

coproduct of sets.

I'm still a bit confused. Usually I expect biproducts in order to represent morphisms as matrices (so this would work with matrices of relations).

Christian Williams (Dec 15 2022 at 21:07):

To define matrix composition, we only need a tensor that distributes over sums, such as $\mathrm{Set}$ product and coproduct. Let $P:A\times B\to \mathrm{Set}$ and $Q:B\times C\to \mathrm{Set}$. Then we can define $P\circ Q:A\times C\to \mathrm{Set}$ by $(P\circ Q)(a,c) = \sum b\in B.\; P(a,b)\times Q(b,c)$.

Mike Shulman (Dec 15 2022 at 21:24):

And the bicategory of matrices of sets does have biproducts, as a bicategory! (Unfortunate clash of terminology here: "biproduct" = "both product and coproduct", not "bicategorical product".)

Mike Shulman (Dec 15 2022 at 21:38):

If a category or bicategory has biproducts, then you can derive a representation of morphisms as matrices. But here, we're defining the morphisms of a (bi)category to consist of matrices, in which case it follows that the (bi)category indeed has biproducts.

Martti Karvonen (Dec 15 2022 at 21:53):

Is this something like the free cat with biproducts? Like given a cat with coproducts, can you always do the same trick?

Martti Karvonen (Dec 15 2022 at 21:55):

Christian Williams said:

To define matrix composition, we only need a tensor that distributes over sums, such as $\mathrm{Set}$ product and coproduct. Let $P:A\times B\to \mathrm{Set}$ and $Q:B\times C\to \mathrm{Set}$. Then we can define $P\circ Q:A\times C\to \mathrm{Set}$ by $(P\circ Q)(a,c) = \sum b\in B.\; P(a,b)\times Q(b,c)$.

This looks like a matrix of sets rather than like a matrix of functions between sets. It's the latter part that I've been confused about

Mike Shulman (Dec 15 2022 at 21:57):

Yep, it's a matrix of sets.

Mike Shulman (Dec 15 2022 at 21:57):

Did someone mention a matrix of functions?

Mike Shulman (Dec 15 2022 at 21:57):

Oh, the matrices of functions are the 2-cells.

Martti Karvonen (Dec 15 2022 at 21:58):

Christian Williams said:

Mat(Set) is a double category.

The "category of objects" is that of sets and functions - the left and right halves of the picture, $f:X\to A$ and $g:Y\to B$.

The "category of morphisms" is that of matrices of sets and matrices of functions - the middle of the picture, $\gamma: Q\Rightarrow R$.

Martti Karvonen (Dec 15 2022 at 21:58):

So
Mike Shulman said:

Oh, the matrices of functions are the 2-cells.

So how does that part work?

Mike Shulman (Dec 15 2022 at 21:58):

But the domain and codomain of the functions in the matrix are the entries in the matrix of sets.

Mike Shulman (Dec 15 2022 at 21:58):

A 2-cell from $P:A\times B \to \rm Set$ to $Q : A\times B \to \rm Set$ consists of a family of functions $f_{a,b} : P(a,b) \to Q(a,b)$.

Martti Karvonen (Dec 15 2022 at 22:24):

Fair enough. How do these 2-cells compose? I guess just by matrix multiplication?

Christian Williams (Dec 15 2022 at 22:35):

yes, $\sum b\in B.\; f_{a,b}\times g_{b,c}$.

Martti Karvonen (Dec 16 2022 at 00:11):

This uses cartesian product. So I guess $C\mapsto Mat(C)$ is some general way of constructing a double category from a category $C$ that has products and coproducts (+ distributivity)?

Martti Karvonen (Dec 16 2022 at 00:12):

Does it have an universal property?

Christian Williams (Dec 16 2022 at 01:17):

That's a great question, which I hope to explore.

Mat(-) as on construction on double categories is sum completion.

But as a construction on monoidal fibrations with sums, which here is Fam(Set) over Set, I don't think it has yet been characterized universally. I'm very interested in that question.

Christian Williams (Dec 16 2022 at 01:37):

One way to recognize them: for each monoidal sum fibration V, the double category Mat(V) is self-dual compact closed, as a V-matrix is always some kind of generalized co/relation (co/span).