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: What does 'fibrant' mean?


view this post on Zulip Jacques Carette (Feb 23 2024 at 14:32):

The nlab does define [[fibrant+object]] but always in the context of a model category, but I've seen its use where no model structure is ever mentioned. In other words, this word seems to carry a (large?) amount of implicit information around with it, which makes its frequent use rather difficult for non-illuminati to "join in" (as the reference material does not enlighten in the slightest).

Note that I do understand the great power of short notation/words for effective and efficient communication between experts. That is most definitely not the source of my frustration. My frustration seems to arise from the wide gap between the formal definition and the in-practice use of 'fibrant'.

view this post on Zulip Nathanael Arkor (Feb 23 2024 at 14:34):

What are some contexts you've seen the term used in the absence of a model category structure?

view this post on Zulip Jacques Carette (Feb 23 2024 at 14:37):

Well, for one, in your question "Strictification of fibrant double categories"... (which was merely my prompt to ask). And all over material on type theory, especially cubical type theory.

view this post on Zulip Nathanael Arkor (Feb 23 2024 at 14:49):

My impression was that the "fibrant" in "fibrant double category" referred to its characterisation in terms of fibrations (Theorem 4.1 of Framed bicategories and monoidal fibrations), rather than referring to it being a fibrant object in a model structure on double categories.

Edit: confirmed here.

view this post on Zulip Nathanael Arkor (Feb 23 2024 at 14:50):

And all over material on type theory, especially cubical type theory.

In the type theoretic context, people really are talking about fibrant objects in the model category theoretic sense, since the semantics of these type theories is higher categorical.

view this post on Zulip Jacques Carette (Feb 23 2024 at 14:55):

Nathanael Arkor said:

In the type theoretic context, people really are talking about fibrant objects in the model category theoretic sense, since the semantics of these type theories is higher categorical.

And what's the 'Quillen model' involved that is implicitly assumed to be known by the readers?

view this post on Zulip Nathanael Arkor (Feb 23 2024 at 15:03):

Maybe you could point out a specific example to check we're talking about the same thing?

view this post on Zulip Jacques Carette (Feb 23 2024 at 15:23):

Examples: Formalization using two-level type theory and Models of Type Theory Base on Moore Paths, both of which use 'fibrant' without definition.

view this post on Zulip Josselin Poiret (Feb 23 2024 at 15:27):

in the case of cubical type theory, this is outlined in https://www.cse.chalmers.se/~coquand/mod2.pdf i believe

view this post on Zulip Mike Shulman (Feb 23 2024 at 15:57):

Note that there are alsoformal frameworks other than model categories that give a precise general meaning to "fibrant", such as a [[fibration category]].

view this post on Zulip Mike Shulman (Feb 23 2024 at 15:58):

Two-level type theory is another such framework: the "fibrant types" in 2LTT are analogous to those in a model category, and might correspond to them in some semantics, but are a different thing.

view this post on Zulip Mike Shulman (Feb 23 2024 at 16:00):

The fibrant objects in semantics of cubical type theory may be also the fibrant objects in a model category, but one doesn't need the whole model category to talk about them, and in practice the whole model category wasn't constructed at first.

view this post on Zulip Mike Shulman (Feb 23 2024 at 16:01):

The nLab page does mention generalizations beyond model categories in the third paragraph. But it would be great to add some intuitive motivation for what "fibrant" means, to make the connection between the various uses.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:09):

The page for [[fibration+category]] seems to be a stub with no actual information in it?

I think I understand 2LTT, so that would definitely be a good starting point for me. If there's formal material that defines fibrant object (carefully, rather than offhandedly) that would be perfect for me.

view this post on Zulip Mike Shulman (Feb 23 2024 at 16:10):

The thing is that "fibrant object" is really a phrase like "group multiplication" -- it's not defined at all in general, it's postulated as part of an abstract structure, and only defined in specific examples.

view this post on Zulip Mike Shulman (Feb 23 2024 at 16:12):

It so happens that in a Quillen model category, a fibrant object can be defined as an object whose map to the terminal object is a fibration. But the fibrations are also a not-defined-but-postulated thing in general, so this is only one short step from a postulate, like, say, conjugation in a group.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:12):

Well, that at least reassures me that I wasn't just missing something obvious!

view this post on Zulip Reid Barton (Feb 23 2024 at 16:13):

In particular, even for the specific usage in model category theory, there are frequently multiple model structures that may be considered on the same underlying category, which typically have different fibrations and different fibrant objects.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:14):

How does one get initiated into the clan (pun intended) of people who understand what 'fibrant' means? Is this one of those things that remains an oral tradition?

view this post on Zulip Reid Barton (Feb 23 2024 at 16:17):

If you want to understand how the word is used in model category theory then you can read a book on model categories, of which there are several. If you want to understand every possible usage and connotation of the term "fibration" then yes, it might be more complicated.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:20):

I'm actually fine understanding 'fibrant' only in the contexts where it overlaps with type theory, in all its guises. I have not yet seen how "model categories" would be helpful to me (though I certainly don't rule it out as a future thing.)

view this post on Zulip Reid Barton (Feb 23 2024 at 16:36):

As far as the type theory is concerned you could treat "fibrant type" as a second primitive term, like "type" itself.

As for why the word "fibrant" rather than some other word, that has to do with the intended sort of semantics of these type theories, which leads back to model categories and fibration categories and so on, which are in turn abstractions of some specific classes of maps of topological spaces, which were called "fibrations" because of their relationship to fiber bundles.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:46):

Fiber bundles from topology are things that I know (my formal training in pure mathematics leaned heavily on analysis, with the core topic of my PhD being complex dynamical systems, more specifically the geometry of Julia sets). Then I slowly morphed into a computer scientist, via a long stint as a software engineer (of symbolic computation software).

view this post on Zulip Reid Barton (Feb 23 2024 at 16:48):

It's not as remote a relationship as my message makes it sound, because typically in models of type theory, the fibrant types will be interpreted as morphisms with some kind of path lifting property, which fiber bundles also have.

view this post on Zulip Reid Barton (Feb 23 2024 at 16:48):

But this depends on the model.

view this post on Zulip Jacques Carette (Feb 23 2024 at 16:56):

the fibrant types will be interpreted as morphisms with some kind of path lifting property

I had 75% guessed that from usage, but it's nice to have it confirmed. I'd be glad to have some reading that makes this more precise. The note from Thierry that @Josselin Poiret sent is 'packed' much too tightly to enlighten me. Pedagogically, I like material that has (intuition, formal definition, concrete examples).

view this post on Zulip Reid Barton (Feb 23 2024 at 17:01):

Maybe https://arxiv.org/abs/1712.04864 ?

view this post on Zulip Jacques Carette (Feb 23 2024 at 17:14):

That it comes with an Agda formalization is likely to be a huge help for me. Thanks.

view this post on Zulip John Baez (Feb 23 2024 at 18:27):

I visualize a cofibrant object as one that's uncoiled, unwound or puffed up. An object oftens fails to be cofibrant when it's "coiled up too tightly", with a bunch of equations that should be equivalences or paths. Cofibrant objects are better to map out of because they don't have such bad equations. So, we often take an object and form a "cofibrant replacement" or "resolution" of it, systematically replacing all nontrivial equations by equivalences or paths. This amounts to "unwinding" the object, or "puffing it up".

view this post on Zulip John Baez (Feb 23 2024 at 18:31):

Everything about fibrant objects is formally dual to cofibrant objects. Cofibrant objects are nice to map out of; fibrant objects are nice to map into. But I have better intuitions for cofibrant objects.

view this post on Zulip Mike Shulman (Feb 23 2024 at 18:35):

I think of a fibrant object as having "all the operations that it is supposed to". From this perspective, a general object of a model category is a sort of generalized "presentation" of an algebraic gadget, on which some of the intended operations may be defined partially, but not necessarily all. A fibrant object is then one where all the operations are defined.

view this post on Zulip John Baez (Feb 23 2024 at 18:37):

Maybe the old algebra/geometry duality is showing up when I give a geometric intuition for cofibrant objects and you give an algebraic intuition for fibrant ones? I don't know.

view this post on Zulip John Baez (Feb 23 2024 at 18:41):

I could draw a cofibrant replacement of Z/n\mathbb{ Z}/n in the model category of simplicial abelian groups and y'all would see how it's like uncoiling a wound-up thread.

view this post on Zulip John Baez (Feb 23 2024 at 18:45):

But it's a nuisance to draw here so algebraists have an advantage over the geometers. :upside_down:

view this post on Zulip Jacques Carette (Feb 23 2024 at 18:48):

Thanks @Mike Shulman @John Baez those bits of intuition are super useful! That's serious gold right there.

view this post on Zulip Patrick Nicodemus (Feb 23 2024 at 18:59):

@Jacques Carette I just want to express my sympathy and reinforce your comment. I too think that "fibrant" seems to be a useful metaphor for some homotopy theorists which conveys intuition that is associated with fibrant objects in model categories.
Not that anyone else here is dismissing your concerns, but I would like to echo the claim that "it makes it difficult for the non-illuminati to join in." I think that the problem is that mathematical objects are multi-faceted and we can see them from many different perspectives, some of which may/may not be useful for the problem at hand. The student or outsider is generally only aware with one or two perspectives, or only knows the formal definition and some basic theorems, and they don't understand how their limited POV is relevant to the problem (This book uses the word "fibration" - how are Hurewicz fibrations related to this? how are Grothendieck fibrations related to this?). The expert is familiar with very many different perspectives and so when two experts communicate, the precise perspective, the meaning of the metaphor "it is like a fibrant object", does not need to be communicated as it is obvious. I think it is bad writing. _How_ is it like a fibrant object? In what way? What properties specifically, rigorously, does it share with fibrant objects? Otherwise, for the newcomer, it is as bad as saying "Go off and read many books about fibrant objects each offering a complementary viewpoint and eventually you will find a book that covers the perspective I want to communicate. Then it will be obvious how these are like fibrant objects."

view this post on Zulip Patrick Nicodemus (Feb 23 2024 at 19:14):

I have complained before in this Zulip about the use of the term "classifying space" and the notation B(-) to convey some metaphorical similarity which is not explained. For example the nlab says on the page for bicategories:

A monoidal category M may be regarded as a bicategory BM with one object. This is a special instance of delooping.

Here I assume this is rigorous (there's some unspecified but presumably obvious higher category here) and if I knew enough about higher topos theory it would be obvious what it means, and the nlab is an open notebook for higher category theory and explicitly disclaims responsibility for being at all pedagogical, so I cannot be too critical of this. But, personally when explaining what is a bicategory is, I would certainly never use this notation B(M) constantly with the implication to the student that bicategories are somehow like classifying spaces for vector bundles over manifolds.

view this post on Zulip Mike Shulman (Feb 23 2024 at 19:35):

I added my intuition about fibrant object to the nLab page [[fibrant object]], and split off a page about [[cofibrant object]] with some intuition based on what John said.

view this post on Zulip John Baez (Feb 23 2024 at 20:20):

Patrick Nicodemus said:

I have complained before in this Zulip about the use of the term "classifying space" and the notation B(-) to convey some metaphorical similarity which is not explained. For example the nlab says on the page for bicategories:

A monoidal category M may be regarded as a bicategory BM with one object. This is a special instance of delooping.

Here I assume this is rigorous (there's some unspecified but presumably obvious higher category here) and if I knew enough about higher topos theory it would be obvious what it means, and the nlab is an open notebook for higher category theory and explicitly disclaims responsibility for being at all pedagogical, so I cannot be too critical of this. But, personally when explaining what is a bicategory is, I would certainly never use this notation B(M) constantly with the implication to the student that bicategories are somehow like classifying spaces for vector bundles over manifolds.

It would be easy for me to explain - and I don't know anything about higher topos theory, so that's certainly not a prerequisite. Indeed I've explained it in various places already. So the question is just: where would be the most useful place to put the explanation? Maybe the nLab page on [[delooping]]?

view this post on Zulip John Baez (Feb 23 2024 at 20:27):

I would describe the classifying space of a group, and why this is like treating the group as a 1-object groupoid, and also why taking the loop space of the classifyng space gets you back to the group you started with - hence the word "delooping".

view this post on Zulip Mike Shulman (Feb 23 2024 at 20:29):

This is digressing rather from the present topic, so should perhaps be moved. But I may as well add that personally, although I do call this the "delooping" of a monoidal category and write it as BM\mathbf{B}M, I prefer to avoid calling it a "classifying space", because unlike the classical case of groups it is much less clear what, if anything, it "classifies" that's related to MM.

view this post on Zulip John Baez (Feb 23 2024 at 20:32):

Unless it's a group. Indeed, there's a nice paper called "what does the classifying space of a category classify?" It's not obvious unless the category is a groupoid. So while the construction is immensely fruitful, calling it a "classifying space" is confusing.

Btw, in general I think complaining that things are never explained is less effective than asking someone to explain them. A bunch of us love to explain things and have already explained many of those "never explained" things. But we'll happily explain them again, especially if the explanation gets put on the nLab.

view this post on Zulip Brendan Murphy (Feb 24 2024 at 00:12):

I'm curious if the intuition of "fibrant = enough operations" can be stretched to the injective model structure on chain complexes (maybe bounded below for simplicity)

view this post on Zulip Brendan Murphy (Feb 24 2024 at 00:13):

Certainly the intuition "cofibrant = relations spooled out" works when talking about projectives (it's where I personally gained that intuition!)

view this post on Zulip Kevin Arlin (Feb 24 2024 at 00:18):

I suppose if you think of division as an operation an abelian group might have, that kind of works?

view this post on Zulip John Baez (Feb 24 2024 at 00:22):

Can someone give me the simplest example of something that's not fibrant because it doesn't have all the operations it should?

view this post on Zulip John Baez (Feb 24 2024 at 00:23):

I kind of like this idea "you fail to be cofibrant if your operations obey too many equations; you fail to be fibrant if you don't have enough operations" - but I only understand the first part.

view this post on Zulip Kevin Arlin (Feb 24 2024 at 00:24):

Well, a horn isn't fibrant because you can't fill it and......0Z0......0\to\mathbb Z\to0... isn't fibrant because you can't divide by 22?

view this post on Zulip Kevin Arlin (Feb 24 2024 at 00:24):

I'm not really sure these two cases feel similar though.

view this post on Zulip Brendan Murphy (Feb 24 2024 at 00:33):

Kevin Arlin said:

I suppose if you think of division as an operation an abelian group might have, that kind of works?

Oh yeah baer's criterion is a nice way of fitting it into this framework!

view this post on Zulip Brendan Murphy (Feb 24 2024 at 00:35):

Re: John's question, I would use kan complexes as an example. A fibrant object in the quillen model structure is something which has all the necessary composition and inverses operators (which are only "operators" in the sense that they turn inputs into contractible spaces of outputs, although if you work with algebraic fibrant objects it's a little more honest)

view this post on Zulip Mike Shulman (Feb 24 2024 at 00:44):

Those are the only kind of "operations" that ordinary model category theory can enforce in its fibrant objects, since all solutions to lifting problems in a model category are unique up to homotoy.

view this post on Zulip John Baez (Feb 24 2024 at 01:03):

I have a good understanding of fibrancy in the category of simplicial sets as meaning "having all horn-fillers". For some reason that's not what came to mind when I heard "operations", but okay, I can deal with that.

What about in something like chain complexes of abelian groups? I just discovered to my horror that injective resolutions (which I never think about) are fibrant replacements in a different model structure than my favorite model structure. And of course this sort of thing makes getting intuition for what "fibrant" or "cofibrant" means a bit tougher: there are different model structures on the same category, so you first have to get intuition for the model structure.

view this post on Zulip John Baez (Feb 24 2024 at 01:07):

One other thing I should have said: if you want to understand "fibrant" and "cofibrant" objects, it may help to first understand "injective" and "projective" objects, which are a bit similar, but much simpler since these are concepts that make sense in any category.

view this post on Zulip Kevin Arlin (Feb 24 2024 at 02:08):

I was offering division (https://en.m.wikipedia.org/wiki/Divisible_group) as something that would work as an operation in complexes of abelian groups, with the injective structure.

view this post on Zulip Kevin Arlin (Feb 24 2024 at 02:08):

Which is very much in line with your suggestion of understanding injective groups instead.

view this post on Zulip John Baez (Feb 24 2024 at 02:15):

Yes. But people struggling for intuition should know that now we're comparing, not just about cofibrant vs. fibrant objects in the same model category, but in two different model structures. And I guess that's yet another good thing for beginners to learn: in certain modern outlooks the "ultimate goal" of a model structure is to create an (,1)(\infty,1)-category, but different model structures on the same category will give the same (,1)(\infty,1)-category if they have the same weak equivalences, so one can argue the concepts of fibration and cofibration are "just technical tools".

view this post on Zulip John Baez (Feb 24 2024 at 02:16):

This is a rather high-flown philosophical view that somewhat neglects how important technical tools can be.

view this post on Zulip Mike Shulman (Feb 24 2024 at 02:22):

I actually find that very mysterious from this perspective. On the one hand, we consider chain complexes but expect the maps between them to be only "weak homomorphisms" so that in order to represent any such weak homomorphism by a strict one we need the domain to be so "puffed up" that most of its strict equalities are replaced by homotopies. On the other hand, we consider chain complexes but require them to be equipped with additional "division"-type operations. Why on earth should those two ideas give rise to the same (,1)(\infty,1)-category? Except that somehow they both accidentally (?) induce the same notion of "weak equivalence".

view this post on Zulip Kevin Arlin (Feb 24 2024 at 02:39):

Wait, do they really induce that notion though?

view this post on Zulip Brendan Murphy (Feb 24 2024 at 05:13):

Well we can define a map to be a quasi isomorphism iff its lift to a projective resolution (or injective resolution) is a chain homotopy equivalence

view this post on Zulip Brendan Murphy (Feb 24 2024 at 05:14):

But that's not just the notion of projective/injective objects, it's the operation of resolution and its functorality (either strictly or as a "functor up to chain htpy equivalence")

view this post on Zulip Brendan Murphy (Feb 24 2024 at 05:15):

Or I guess a better thing to say is (K-)projective complexes localized at chain homotopy equivalences are equivalent to (K-)injective complexes localized at chain homotopy equivalence

view this post on Zulip Mike Shulman (Feb 24 2024 at 16:29):

It's true, as Brendan says, the weak equivalences are only determined by the functor of (co)fibrant replacement together with the notion of chain homotopy equivalence. But I still find it surprising -- from the perspective of "cofibrancy as uncoiling, fibrancy as having operations" that projective resolution + chain homotopy equivalence induces the same notion of quasi-isomorphism as injective resolution + chain homotopy equivalence.

view this post on Zulip Jacques Carette (Feb 24 2024 at 17:34):

So if I understand correctly, from a type-theoretic point of view, the 'fibrant' types are the ones that can participate in all type formation operations (like Π,Σ,Id\Pi, \Sigma, \mathsf{Id}) and the non-fibrant ones are the special ones (such as interval types). Is that right?

view this post on Zulip Mike Shulman (Feb 24 2024 at 17:34):

Well, in general (such as in 2LTT), the non-fibrant types can have their own type-forming operations.

view this post on Zulip Mike Shulman (Feb 24 2024 at 17:35):

Maybe in Orton-Pitts they don't?

view this post on Zulip Jacques Carette (Feb 24 2024 at 17:37):

I have not had the time to properly read Orton-Pitts -- I was trying to extrapolate from the intuitions given above.

I do see that non-fibrant types can have their own special operators.

view this post on Zulip Mike Shulman (Feb 24 2024 at 17:38):

E.g. for any types A,BA,B, fibrant or not, there are types such as A×BA\times B, ABA\to B, and so on. And if AA and BB are fibrant, then so are A×BA\times B, ABA\to B, and so on.

view this post on Zulip Jacques Carette (Feb 24 2024 at 17:40):

Ok, but now I don't see the point in segregating them into different classes?

view this post on Zulip Mike Shulman (Feb 24 2024 at 18:19):

The difference is that the "positive/inductive" fibrant-type formers aren't just special cases of the non-fibrant ones, and their elimination rules only apply to other fibrant types. So for instance if AA and BB are fibrant you have both a non-fibrant type A+eBA+^e B and a fibrant type A+BA+B, and you can only define a map A+BCA+B \to C by reduction to cases if CC is also fibrant.

view this post on Zulip Mike Shulman (Feb 24 2024 at 18:20):

And most importantly, there is both a non-fibrant equality type x=eyx=^e y and a fibrant identity type x=yx=y, and you can only transport across the fibrant identity type in a fibrant motive.

view this post on Zulip Josselin Poiret (Feb 26 2024 at 09:50):

Jacques Carette said:

So if I understand correctly, from a type-theoretic point of view, the 'fibrant' types are the ones that can participate in all type formation operations (like Π,Σ,Id\Pi, \Sigma, \mathsf{Id}) and the non-fibrant ones are the special ones (such as interval types). Is that right?

my understanding of Orton-Pitts is that fibrant types are types which have a Kan composition operation, ie. can hcomp! Thus the inner type theory of fibrant types would be a cubical type theory.