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.
Jacques Carette (Mar 16 2021 at 22:32):I was somewhat surprised to see that even enriched factorization systems are defined using subsets of 'as a whole'. I've rather internalized that is an indexed family of 'things', i.e. taking from the dependently-typed approach the indexed/family idea, and from enrichement, the idea that it doesn't have to be a set at all, i.e. hom-objects.
Similarly, at the level of objects, one does not talk of subset of an object (which makes no sense at all), but rather of subobject which is defined not as an object or collection of objects, but rather as an isomorphism class of monomorphisms. [Is there a notion of V-subobject?]
It similarly feels like one ought to try to liberate the notion of factorization system from the notion of subset by finding a different way to "point out" parts of a family of without treating them as sets.
I have not succeeded in finding such a definition. Has it been done?
John Baez (Mar 16 2021 at 22:38):Jacques Carette said:
I was somewhat surprised to see that even enriched factorization systems are defined using subsets of 'as a whole'. I've rather internalized that is an indexed family of 'things', i.e. taking from the dependently-typed approach the indexed/family idea, and from enrichment, the idea that it doesn't have to be a set at all, i.e. hom-objects.
Yeah, I don't think people seriously work with the "subsets of whole set of morphisms" when using factorization systems. They usually use subcategories. The stuff on the nLab seems easy to translate into those terms.
Reid Barton (Mar 16 2021 at 23:23):Being in the left class (or the right class) is a property that a morphism of the category may or may not have. Constructively, I think it's usually better to allow for it to be structure and not just a property (compare https://ncatlab.org/nlab/show/algebraic+weak+factorization+system).
Reid Barton (Mar 16 2021 at 23:24):The term "enriched" is a bit misleading--it makes sense for an indirect reason, but it is really structure on the underlying ordinary category, that satisfies a certain compatibility with the enrichment.
John Baez (Mar 16 2021 at 23:27):Jacques seemed to be complaining about treating all morphisms in a category as elements of a single set, or class. This is indeed widely deprecated: most experts prefer to treat morphisms as "typed", e.g. elements not of a single class but of many different sets . In this approach, instead of treating composition as a partially defined function we consider it as a whole bunch of totally defined functions
For people who consider these two approaches so similar as to not be worth fussing about, well, such people are welcome to ignore this comment of mine!
Reid Barton (Mar 16 2021 at 23:29):In dependent type theory you could express the notion of "a class of morphisms" as either Pi A B. (Hom A B -> Prop) or (Sigma A B. Hom A B) -> Prop, and there wouldn't be too much difference between them.
John Baez (Mar 16 2021 at 23:29):For people who care, the "typed" approach can be used to say things like: it makes sense to ask if two morphisms in a single homset are equal, but not to ask if two morphisms in different homsets are equal.
Reid Barton (Mar 16 2021 at 23:31):And indeed with the "untyped" approach you could use Mor -> Prop, a subset of all the maps of the category.
Reid Barton (Mar 16 2021 at 23:35):I don't think you should read distinctions about whether the morphisms of a category are indexed on the objects or collected into a single type with maps to the objects from language like "a class of morphisms"--this kind of stuff is way below the level at which mathematicians ordinarily work. It would be like seeing a definition of the derivative of a function and asking whether "the reals" are the Dedekind reals or the Cauchy reals.
Jacques Carette (Mar 16 2021 at 23:36):I was concerned about two things: treating morphisms as a single set, and treating morphisms as a set.
I do agree that treating them as a single set is largely obsolete. Except, in some sense, for the definitions of factorization system that I've seen.
Jacques Carette (Mar 16 2021 at 23:36):Good point about over-reading "class of morphisms".
Nathanael Arkor (Mar 16 2021 at 23:38):(Treating the morphisms as a single class is useful for generalising to internal categories.)
Jacques Carette (Mar 16 2021 at 23:40):I had not encountered algebraic weak factorization systems before, thanks for the pointer.
Having be a structure, rather than a property, makes the most sense to me. It's not immediately clear to me if all factorization systems are AWFS?
Nathanael Arkor (Mar 16 2021 at 23:42):All orthogonal factorisation systems are AWFSs (by uniqueness of the lifts).
Jacques Carette (Mar 16 2021 at 23:47):(I've tried to formalize internal categories before and... failed. All the expositions that I've seen are sufficiently fuzzy on some crucial details that made what the right laws ought to be rather opaque. The construction was straightforward enough, but trying to even state things like associativity was really not at all clear. Also, asking for all pullbacks seems like overkill, but trying to figure out which shape pullbacks must exist seems rather non-trivial).
Reid Barton (Mar 16 2021 at 23:50):By the way, I don't think the definition on enriched factorization system is the standard one. It should be the case that all isomorphisms belong to both classes, but as far as I can see this definition allows, for example, E = all maps, M = identity maps.
John Baez (Mar 16 2021 at 23:56):Jacques Carette said:
(I've tried to formalize internal categories before and... failed. All the expositions that I've seen are sufficiently fuzzy on some crucial details that made what the right laws ought to be rather opaque.
Hmm, it's always seemed clear to me.
It's true that not all pullbacks need to exist; just the pullbacks actually used in the definition need to exist, and this is important when dealing with categories internal to a category that doesn't have all pullbacks, like Diff.
Conor McBride (Mar 17 2021 at 00:14):Time is everything, but often unaccounted. Squeezing the toothpaste out of a tube? Putting the toothpaste back into the tube? What's the difference? There's a hell (and I use that word from experience) of a difference.
Index over the past. Fibre over the future.
Mike Shulman (Mar 17 2021 at 00:41):Reid Barton said:
By the way, I don't think the definition on enriched factorization system is the standard one. It should be the case that all isomorphisms belong to both classes, but as far as I can see this definition allows, for example, E = all maps, M = identity maps.
That's clearly a mistake; someone should fix it! The definition of enriched factorization system should be identical to the definition of orthogonal factorization system only with ordinary orthogonality replaced by enriched orthogonality.
Jacques Carette (Mar 17 2021 at 00:47):Conor McBride said:
Index over the past. Fibre over the future.
Ah, if I unpack that right, I should use a type with 2 distinguished points (for left and right) and a map from (suitably indexed) into that. Some will be in the left, others in the right, and others will simply be elsewhere. We don't necessarily need to know anything at all about elsewhere, so no point being too specific about it (unlike AWFS which seem to specify that elsewhere is contractible).
Something like that?
Jacques Carette (Mar 17 2021 at 01:01):No, that can't quite be right, since for the (epi, mono) system, the isos belong to both. Back to the drawing board.
Joachim Kock (Mar 17 2021 at 14:51):It is sometimes a very good viewpoint to put all the morphisms together in a set (assuming of course the category is small): it's the beginning of the nerve. It brings us into simplicial methods! Most of -category-theory is done in this viewpoint.