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.
There are a collection of definitions around bundles that I seem able to relate correctly with my intuition. However, I'm pretty sure there is an abstract principle governing everything, but I'm struggling to smoke it out.
I'll attempt a question, but if someone can see I'm circling a big idea I'd appreciate it if they pointed it out.
Subobject classifiers are special, because maps into them correspond to subobjects. You can expand the congruence into the pullback diagram:
In Set, is just the boolean set.
In type theory, it's useful to imagine , or even to think of our classifying function, or predicate, as a map into Set that returns the inputs wrapped in a set if they're in the subset, and empty otherwise.
With that change, then our subset is given by the category of elements . It's just the union of all the preimages.
This seems to be a kind of special case of the universal construction relating set valued functions, and bundles. Given by the following diagram:
It's harder to write the natural congruence here in a way that captures the use of the category of elements, in a sort of fake math notation, it'd look something like .
There's some story here involving "Stuff, Structure, and properties" and categorification. I'm not sure why the category of elements is involved beyond it "unions the sets". In this diagram it's describing a limit, but unions are usually colimits, like coends.
To ground this with a definite question though, is there a way to indicate what properties the fibers should satisfy by modifying the diagram? It's clear the subobject classifier classifies injective maps, because the fibers have at most one element - If they also had at least one element they'd be isomorphisms. Is there a way to take the pullback defining Set, and tweak it to require the output sets are at best singletons, and then see the new diagram must be the pullback of ?
And again if there is some more abstract idea that explains how everything is related, like maybe grothendieck constructions, I'm open to any explanation or pointers to places to learn more.
...And now that I just wrote that out, it occurs to me that in the diagram for the subobject classifier, with being the simple minded bool, the predicate has the features of a bundle, with its preimage giving , an object which then embeds into via the monomorphism . This monomorphism has the character of a generalized element.
But when we step up from arrows to functors when looking at the pullback describing Set, their roles are reversed. The indexing functor looks like a generalized element picking out sets from Set, with it being wrapped into a bundle into B from .
Is there something mathematical going on here, or are "generalized elements" and "bundles" just points of view?
Just as the subobject classifier classifies subobjects via pullback, the forgetful functor from pointed sets to sets classifies [[discrete opfibrations]]. The idea that Set plays the role of a categorified subobject classifier is explored in detail in Weber's paper Yoneda structures from 2-toposes.
The pattern you're noticing, @Alex Kreitzberg, is very broad. I wrote about some examples in week223 of This Week's Finds, and in a more formal way in the start of Lectures on n-categories and cohomology.
Here are some stuff quoted from week223, given examples of the principle you're noticing:
n-GROUPOIDS FIBERED OVER AN n-GROUPOID B ARE "THE SAME" AS
WEAK (n+1)-FUNCTORS FROM B TO THE (n+1)-GROUPOID nGpdGrothendieck also studied this kind of thing with categories replacing groupoids, so there should also be an n-category version, I think... but it's more delicate to define "fibrations" for categories than for groupoids, so I'm a bit scared to state a slogan suitable for n-categories.
However, I'm not scared to go from n-groupoids to ω-groupoids, which are basically the same as spaces. In terms of spaces, the slogan goes like this:
SPACES FIBERED OVER THE SPACE B ARE "THE SAME" AS MAPS FROM B TO THE SPACE OF ALL SPACES
This is how James Dolan taught it to me. Most mortals are scared of "the space of all spaces" - both for fear of Russell's paradox, and because we really need a space of all spaces, not just a mere set of them. To avoid these terrors, you can water down Jim's slogan by choosing a specific space F to be the fiber:
FIBRATIONS WITH FIBER F OVER THE SPACE B ARE "THE SAME" AS MAPS FROM B TO THE CLASSIFYING SPACE OF AUT(F)
where AUT(F) is the topological group of homotopy self-equivalences of F. The fearsome "space of all spaces" is then the disjoint union of the classifying spaces of all these topological groups AUT(F). It's too large to be a space unless you pass to a larger universe of sets, but otherwise it's perfectly fine. Grothendieck invented the notion of a "Grothendieck universe" for precisely this purpose.
This was written before homotopy type theory came into being. These ideas can be stated more cleanly in that framework.
It sounds like a vast generalisation of what I was talking about in my “Indexed-Fibred Duality” article…
I'm still processing the answers, but I do want to acknowledge Ruby's questions and articles around similar (the same?) topic have been helpful. My accordion post from even earlier touched on similar ideas from a much more confused perspective. In retrospect I see you can lift abstract intervals to concrete intervals on the accordion layout, which I believe means an accordion is an example of a fibration. With the projection sending pitches to their letter names, and physical intervals to their musical intervals.
But I still felt something was missing, so I wanted to start a thread to see if the way I phrased my confusion would invite answers relevant to my confusion.
I guess to apply Baez's slogan to accordion layouts - a specific accordion layout is "the same" as all of the possible transpositions of melodies expressed in terms of intervals. If I'm understanding all the moving parts of the above correctly.
I think that's even the same as the groupoid version of the statement, because the layout is even a torsor (if you pretend the accordion is infinite).
It's good to know homotopy type theory is a nice way to think about this.
Lets see if I can say something interesting, or have questions, about Weber's paper.
John Baez said:
The pattern you're noticing, @Alex Kreitzberg, is very broad. I wrote about some examples in week223 of This Week's Finds, and in a more formal way in the start of Lectures on n-categories and cohomology.
I had seen this some time ago but had forgotten about it. In this perspective, what does one make of, more generally, sequences? What I have in mind are, for example, those four-term sequences appearing in the construction of the Toda bracket.
I don't know.
Maybe this is a more simple minded question in that vein.
The exact sequences are a nice way to specify the fibers are all isomorphic.
I took this as an answer to my question of "how do you specify the fibers of a bundle in a category?" But as an exercise I was going to try to see if I could expand the exact sequence definition into a more abstract diagram or leave it to a future HoTT proof (for example, I remember there it's important to show all types in a family are contractible if you want a proposition).
Maybe more experienced folks have suggestions for how to approach this as an exercise, or if it is a good exercise?
I got a ping that has me worried I asked the question poorly.
I know I can find the fibers with pullbacks:
I made up the exercises:
My question to the room is, are these good solvable exercises?
I wouldn't have asked but given Alonso's question, I thought maybe asking would help open the door to talk about exact sequences for a bit.
Alex Kreitzberg said:
I got a ping that has me worried I asked the question poorly.
Yes, I had no idea what the earlier question meant, and got worn out trying to decipher it. This one looks much clearer, thanks - though still very open-ended.
Maybe they're too open ended because my real goal is broader than exact sequences. I'm trying to understand arrows via fibers.
If I restrict my attention to Set, and look at a type family defined by , then I know the associated projection is surjective, because each set of the family has at least one element.
I know many properties about functions can be defined in terms of properties of their fibers.
I'd like to be able to classify morphisms in terms of their fibers in more categories than just set. Which means I need to be able to say stuff about the fibers in categories other than set.
The way this relates back to my original question, is I think the classifiers can be thought of as structurally encoding requirements on the fibers.
These are all technically subcategories of , so in particular maybe I can find a strategy for relating and .
I'm actually optimistic I'll get more ideas for how to formalize this if I keep reading Weber's paper. So if that's still too open ended, hopefully I'll have a chance to fix it.
Alex Kreitzberg said:
Maybe they're too open ended because my real goal is broader than exact sequences.
I still think that mathematicians respond best to narrowly defined questions, especially those of the form "can you prove X?", or "is X true?" Even when I have broader goals - and I always do - I try to create narrowly defined questions that will shed a lot of light on whether I can achieve those goals, and how. I put a lot of work into crafting those questions. Then I broadcast those questions and mathematicians are happy.
I may or may not broadcast my broader goals. Sometimes I explain a bit about them after broadcast my precise question. But the precise question is very attractive to mathematician. It lets them know that I'm not asking them to do the very difficult work of making my vaguely stated goals precise - I'm not putting that heavy burden on them. I'm simply asking them if they know a fact: something mathematicians love.
You can ignore all this if you want. These are just my thoughts on how to get mathematicians to eagerly answer your questions.
Alright, how about this for a precise question -
An injective function corresponds to a set family valued in sets with at most one element
A surjective function corresponds to a set family valued in sets with at least one element
A trivial bundle corresponds to a constant set family (This reminds me of exact sequences).
The contravariant power set functor of , , is just the monomorphisms into up to unique isomorphism. is representable in Set, which defines the subobject classifier : . After noting , we see this representability condition corresponds to the equivalence between injective functions and set families with at most one element.
In Set, can one define a representable contravariant functor valued in epimorphisms - with "sets with at least one element" as the representing object? What about proving representability for a contravariant functor valued in trivial bundles?
I need to keep reading Weber's paper, but after writing that out - I believe It's necessary to distinguish the singleton set from a set of one set for working with trivial bundles, and one needs to clarify "set in set" issues to work with surjections.
Therefore tracking only bijections isn't good enough to solve the above questions? We need at least a 2 category?
I guess that was precise enough for me to start to sense the issues, and that my definitions and questions need even more work.
Are you asking whether there exists a quotient object classifier in Set, i.e. an object such that set functions are naturally identified with isomorphism classes of epimorphisms out of If I've just pushed that over the line from almost-precise to precise in the correct direction, you might like to think about it yourself before I say anything else.
It would be an object such that set functions are naturally identified with isomorphism classes of epimorphisms into . Not out of.
Just like the subobject classifier is an object such that set functions are naturally identified with isomorphism classes of monomorphisms into .
It seems like a good thing for me to do, is try to define functors taking values in isomorphism classes of epimorphisms. For a given inputted X, One functor should take arrows into X, and the other should take arrows out of X.
I think you are going to run into some fairly severe size issues here - there will be a proper class of epimorphisms into X, even after modding out by isomorphism. I believe this follows from the collection of all cardinal numbers forming a proper class…
I suppose if you take to be the category of nonempty sets and functions between them, then the category of epimorphisms into should be equivalent to the functor category . But the issue is that the skeleton of is not small!
Per Baez's quote I think [[grothendieck universes]] resolve that issue.
Definition 2.1 A Grothendieck universe is a pure set such that:
1.) (transitivity) for all and , we have ;
2.) (power set) for all , we have ;
3.) (empty set) ;
4.) (unions) for all and functions , we have .
I'm not good at set theory proper, so forgive me if I mess this up.
We can form subsets, because they're members of a powerset of a set, and because we can form members of a set by transitivity.
We can form finite unions, because iterating power sets on the empty set twice , So maps from picks out any two sets which we can take the union of by axiom four.
This lets us take make with your favorite encoding. We have any subset of the powerset of by what I said above. Let be the subset (This is a critical step that I think is legal, but it's also subtle in a way I'm not sure I understand).
The nlab page notes the usual encodings in set theory work for all of the major constructions. Which includes the functions defined as a certain subset of , which in particular allows the functions .
Again I'm not used to this style of thinking, so I might've messed something up, but my understanding is the point of grothendieck universes is to just let us do this sort of stuff.
But, what I really want to get a handle on with is, assuming size issues are resolved, how it tracks the difference between sets like and .
Yes, you can take a Grothendieck universe and for any fixed set there will be a set of epimorphisms with . This is good enough because the Grothendieck universe will act a lot like the class of all sets "for most practical purposes". So I don't think size issues are the main issues to be dealt with in trying to work out your idea.
Right, but I think you may still run into the issue of finding a representing object. It would need to be some “set of cardinal numbers within the grothendieck universe”, and I don’t believe this will actually be an element of U. So, within a given universe, I don’t see how you’ll get a representing object…
The whole point of using a universe U is that it allows you to do constructions with sets in U that give you set that's not in U. This is how we use universes to dodge various problems. As long as we're only doing constructions on sets in U that give sets in U, there's no point in using U.
Right, so the point is we might want a "function" between "sets" in different universes of the heirarchy, but it doesn't matter how far apart they are, because you can imagine a bigger universe they both live in.
So you can even have a plain old normal category of SETS++++, if you really wanted to. This is just another take on the usual set theory.
But that's orthogonal to what I'm trying to understand I think. Even if size issues aren't a problem, classifying certain arrows in the one dimensional part of my category still requires something from the two dimensional part.
Indeed, I would forget about these size issues until everything else seems to be working.
Ok, so again, you want to know whether the functor of isomorphism classes of epimorphisms into a fixed is representable. It does at least form a contravariant functor, since pullbacks of epis are epi. As Ruby mentioned, it can only be valued in sets of a universe level up from the size of , but OK, you can still ask the question. So, then, how can one represent a surjection into via a function out of ?
So we have our universe U, our set S of inhabited cardinals inside U (which is too big to fit inside U), and the set S' of "elements of S", meaning pairs of an inhabited cardinal and an element of . The surjection S'-->>S which forgets the elements classifies surjections whose fibers are U-small. Note that this is very close to the classifier of all arrows: we only need to add the empty set into S to get the classifier for all maps with U-small fibers!
Hopefully you got far enough that this wasn't a big spoiler @Alex Kreitzberg ...
So, at least in SET, the pullback diagram is the same as for Set, except and Set, are replaced with your definitions for and respectively?
Like in this?
So then for the subobject classifier , its analog for would consist of the single pair consequently the truth arrow is implied by the same forgetful functor construction.