Added paragraphs on the contravariant poset of subobjects functor.
]]>I added a parenthetical on well-powered categories to poset of subobjects.
]]>Re #13: yes! That’s certainly one of the contexts I had in mind; good that you picked up on it.
]]>Note that there is a notion of well-powered category for a reason: some categories have partially ordered sets of subobjects and some don’t (here subobject=equivalence class of monos). So talking about the poset (qua set) of subobjects of an arbitrary category is a mistake.
In case one has an M-category with the tight morphisms forming a partial order, such as the category of material sets with subset inclusions, then it makes sense to consider the given partial order rather than the partial order reflection of the preorder of monos.
]]>Many thanks for the responses. They gave me a new perspective on monoidal categories and new impetus to continue learning and writing about related more modern developments on monoidal categories.
Incidentally, I had so far thought of the pursuit of “strictification” more or less in the way that Todd tried to preempt here: that is, I unthinkingly thought of strictificationas more or less nothing else than “well, equivalence-of-categories is an equivalence-relation on the class of all categories, strictification is nothing but trying to find a existence-proof to the effect that within the..err…equivalence-class of some specified weak category $\mathcal{C}$ there somewhere exists some strict category $\mathcal{C}^{\mathrm{st}}$, with $\mathcal{C}^{\mathrm{st}}$ being of less interest than $\mathcal{C}$ itself”. The point of strictification, however, seems to be that the strict equivalent category is at least as nice as the weak category in question, and there are many concrete constructive algorithmic aspects to building the strict “equivalent machine” $\mathcal{C}^{\mathrm{st}}$. Incidentally, when I read about the lore about “Gordon-Power-Street could not strictify the weak category they had constructed” I more or less thought “So what? Why did they want to squash the beautiful machine they had built?”.
To add relevant context, I include here a citation of Todd’s above-cited explanation, redacted and modified for brevity and my own education; to repeat, the original currently can be found in #18 of this thread, the use of the citation-functionality is, strictly speaking, not quite correct here:
]]>Strictification can be viewed as reconstructing associativities. Some mistake strictifying a monoidal category for quotienting (identifying associativities with identities). That’s a misleading point of view: the right one is that strictifying means constructing a monoidal embedding of a monoidal category $M$ into a strict monoidal category $M^{st}$, with the embedding re-assembling the associativity- and unit-isomorphisms of $M$ into cliques.
For example, a 4-fold tensor product like $(a^b \otimes (b^c \otimes c^d)) \otimes d$ is a vertex in a clique which in particular contains of all five ways of bracketing $a^b \otimes b^c \otimes c^d \otimes d$ and the groupoid of associativities between them. More precisely, the clique consists of the infinitely many such finite formulas with (finitely-many) units inserted (e.g., $((a^b \otimes I) \otimes (b^c \otimes c^d)) \otimes (I\otimes I \otimes d)$), these formulas being the objects of the groupoid generated by associativity and unit isomorphisms. By Mac Lane’s coherence theorem (often referred to by “all diagrams commute”), there is exactly one morphism between any two vertices in this clique, so the groupoid is equivalent to a terminal groupoid, hence contractible.
Formally, a clique in a category $C$ is a pair consisting of a contractible groupoid $G$ and a functor $F: G \to C$. A morphism between two cliques $(G, F: G \to C)$, $(G', F': G' \to C)$ is a family of $C$-morphisms $F(g) \to F'(g')$, with $(g, g')$ ranging over $Ob(G) \times Ob(G')$, making all triangles in sight commute. (In fact, by contractibility, any one of the $F(g) \to F'(g')$ uniquely determines all others.) The monoidal strictification $M^{st}$ has objects precisely those cliques in the monoidal category $M$ which arise by application of the “all diagrams commute” formulation of Mac Lane’s coherence theorem (which specifies the structure of the free monoidal category on one generator as a disjoint sum of contractible groupoids), and the morphisms in $M^{st}$ are defined to be morphisms of cliques. The precise description is in here, where it is indicated that the evident embedding $i: M \to M^{st}$ is an equivalence in $MonCat$.
In any case, because $M$ is embedded in $M^{st}$, any diagram we are trying to prove commutative in $M$ physically exists in $M^{st}$, but any associativities and units in the diagram get absorbed into cliques, or rather: any such associativity is one of the components $F(g) \to F'(g')$ of the above morphism-family, and uniquely determines, an identity morphism of cliques. Therefore any such associativity morphism in $M$ is reinterpreted as an identity morphism in $M^{st}$, and the diagram we are trying to prove commutative in $M$ uniquely generates a corresponding “larger” diagram of cliques in the strict monoidal category $M^{st}$. So it is enough to prove the diagram commutes when interpreted in a strict monoidal category: we can then interpret the result in $M^{st}$, and the corresponding diagram in $M$, which is embedded in the clique diagram, is then automatically commutative as well.
Yes, I agree that Fetisov is wrong.
]]>Re #8: I might be misunderstanding what Fetisov is trying to say, but the equivalence between contractible groupoids (connected groupoidal preorders) and the terminal category, and more generally between groupoidal preorders and discrete categories, has surely been known and appreciated for a very long time (long, long before HoTT). I consider it a useful guiding principle in general category theory.
]]>isomorphisms-are-all-alike-and-even-thinking-about-one-of-them-individually-is-beside-the-point-in-category-theory philosophy
I don’t know where you picked that up, but it is definitely not the philosophy of category theory. On the contrary, it is crucial in category theory to talk about individual isomorphisms. For instance, the constraint isomorphisms of a monoidal category or bicategory are individual particular isomorphisms, and it matters a lot that we use those particular isomorphisms and not some other random isomorphisms between the same objects.
]]>Another relevant piece of context: now that my eyes were opened to this, I suddenly saw that the comment
the main thing is that the groupoid core of the the category of subobjects is essentially discrete, and so we are quotienting by unique isomorphisms, which is generally well-behaved. – Peter LeFanu Lumsdaine Oct 12 ’14 at 0:09
to the above mentioned MO discussion
is consistent with what I wrote in #7 of this thread.
]]>To add more context and material for future readers of this thread (I am still not sure whether one should mention developments as recent and changing as homotopy type theory in an encyclopedia article as basic as poset of subobjects, only adding context here), I point out that the following sentence of A. Fetisov in the above-mentioned MO discussion
Distinguishing groupoids that are literally discrete from homotopy equivalent to discrete ones is a matter of taste which no one cared about before HoTT came.
is something in the direction of what I had in mind when writing
Since I do not have much experience in this debate, I shy away from trying to connect isomorphic-types-are-equal with poset of subobjects, but it seems to me that something relevant could be said in this regard in poset of subobjects by someone more experienced.
in #1.
EDIT: to add relevant context and make this discussion more self-contained for future readers, I here add two comments of Mike Shulman on the above cited MO-comment “Distinguishing groupoids […] came.” I simply cite the two comments verbatim here:
]]>@AntonFetisov I think your last sentence is wrong in two ways. Firstly, distinguishing discrete groupoids from homotopy discrete groupoids has a long history and many applications. For instance, the coherence theorem of monoidal categories says that certain groupoids are homotopy discrete; but they are certainly not discrete. And the Barratt-Eccles operad is the nerve of an operad in Gpd consisting of homotopy-discrete (indeed, contractible) but not discrete groupoids; if they were replaced by discrete ones then the whole point would be lost.
Secondly, the whole point of HoTT is that it syntactically enforces homotopy invariance, and thus in particular is unable to distinguish internally between discrete and homotopy-discrete groupoids.
Re #4:
Nonsense. $Mono(X)$ is the full subcategory of the slice $C/X$ whose objects are monic arrows with codomain $X$. This is a preorder.
I agree that writing
there are in general many different arrows between two subobjects
was careless and wrong (though not technically nonsense); thanks for pointing out; while I knew the evident argument that uses the monicity to show that two proposed arrows between two subobjects are exactly equal in the language of category theory, I mean, the obvious ( $fg = h$, $fg'=h$ ) $\Rightarrow$transitivity$\Rightarrow$($fg=fg'$)$\Rightarrow$monicity$\Rightarrow$($g=g'$) argument, I had not realized that this means that for both versions of the definition of “subobject”,
When writing the rash claim about “many arrows”, I fleetingly thought of isomorphic subobjects and the in general many arrows witnessing said isomorphism. Possibly influenced by the isomorphisms-are-all-alike-and-even-thinking-about-one-of-them-individually-is-beside-the-point-in-category-theory philosophy, I had never stopped to make this clear to myself. Thanks for pointing out. Learned something new.
Non-class meaning?
With
to me “groupoid of subobjects” actually seems more precise: doesn’t it remind the reader that in this case, then, the non-class-meaning is meant
and in particular “non-class-meaning” I meant: if one writes “groupoid of subobjects”, the category-theoretic term “groupoid” tends to remind readers that it is likely the we-do-not-take-isomorphism-classes-version that is meant. “Non-class-meaning” was meant as a shorthand for “we-do-not-take-isomorphism-classes-version”.
Incidentally, the (of course still unusual) usage “groupoid of subobjects” is used in the third bullet of the third paragraph of current version of this nCafe post. I seem to recall that this was a contributing factor to my adopting this.
I recognize that in the above nCafe link, the reason for using “groupoid” is probably mainly that this term occurs as part of the composite “$\infty$-groupoid”, rather than that using “groupoid” is generally advisable in the context of subobjects.
[ Grammatical note: The “read” in ” If you read my words in that answer, I was […] ” in #4 is an interestingly ambiguous use of a non-homophone-homograph in written English, impossible to simulate e.g. in German. I saw more red than reed in the sentence, but probably you just meant the non-subjunctive mood. ]
]]>Re #4: many thanks for the detailed responses. There are a few things that do not sit right with me, most of this is linguistic though. I may clarify later.
But one small thing right away: the singling out of one person in the references I added was more or less an accident of my mechanically imitating Todd’s method of giving citations in unnatural isomorphism. Not that I had anything against that in principle, but in poset of subobjects I found it to look too odd and changed the author to “mathoverflow”, while retaining the automatially-generated link copied from the MO-site.
]]>I agree that it’s fine to talk about a preordered class, but it’s also worth a remark at poset of subobjects that in general it may be a proper class, so I added one.
]]>If you read my words in that answer, I was explicitly referring to the underlying set of the poset of subobjects, where I say “discrete category of subobjects”. One context where this consideration comes up is the question of representability of the composite
$C^{op} \stackrel{Sub}{\to} Pos \stackrel{U}{\to} Set$where representability amounts to having a subobject classifier. (Sometimes this composite is denoted as $Sub: C^{op} \to Set$; the receiving category, $Pos$ or $Set$, makes clear which sense is meant.)
to me “groupoid of subobjects” actually seems more precise: doesn’t it remind the reader that in this case, then, the non-class-meaning is meant
Non-class meaning? Anyway, choosing the word “preorder” as opposed to the word “poset” seems to indicates the distinction just as well. If anything it’s the word “subobject” with now two senses that is introducing potential confusion. Martin would be much better off just writing $Mono(X)$, if that is what he means or wants. “Subobject” has a pretty established meaning, as recorded in the nLab.
The word “preorder” immediately lands one in the land of sets
Meh. I’m totally fine with referring to a class as being preordered, but if this is really a bother to fastidious people, we could substitute “thin category” (I think we can safely allow the objects of a thin category to form a proper class, although the nLab doesn’t quite say so, yet). Seems a rather pedantic point to me.
while in your sense of “preorder of subobjects” there are in general many different arrows between two subobjects.
Nonsense. $Mono(X)$ is the full subcategory of the slice $C/X$ whose objects are monic arrows with codomain $X$. This is a preorder.
]]>Re #2: many thanks for the response.
You may have a better feel and understanding of this, but, actually, I had opted for “groupoid of subobjects” after weighing my words carefully, and consciously deciding against “preorder”, for the following reasons:
These are rather terminological and imprecise matters. I am not asking for many justifications or a debate, and will myself not harp on about it, let alone change it back.
]]>“Groupoid of subobjects” is not a very accurate way of putting it; I changed it to “preorder”. The main point of course is that the preorder of monomorphisms into $X$ is equivalent to its posetal reflection which is the poset of subobjects in the sense of subobject.
]]>poset of subobjects did not yet have a remark on the frequently occurring question whether to define subobjects as morphisms or as isomorphism classes thereof, nor did it yet (seem) to have a thread. Added both. In particular, added the phrase “groupoid of subobjects”. Added two reference where the morphism-versus-class-of-morphisms issue is discussed. Refrained from making any recommendations or comparisions, only writing “alternative definition”.
Whenever I see this topic coming up, I am reminded of the “Isomorphic types are equal?!” debate.
Since I do not have much experience in this debate, I shy away from trying to connect isomorphic-types-are-equal with poset of subobjects, but it seems to me that something relevant could be said in this regard in poset of subobjects by someone more experienced.
]]>