Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItex[[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.

   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.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeJul 14th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex"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]].

   “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.

3. • CommentRowNumber3.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexRe #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: * I was modelling "groupoid of subobjects" on your own use of "groupoid of monomorphisms" [in your answer to this MO question](https://mathoverflow.net/questions/184196/concise-definition-of-subobjects); I recognize that said usage of yours is more precise since there, "monomorphism" is unambiguous, while the phrase "groupoid of subobjects" may leave readers wondering what definition of "subobject" is meant; still, 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 * I know and love preorders, but isn't "preorder of subobjects" almost-wrong, at least with the usual definition of [[preorder]]? Reasons: * * The word "preorder" immediately lands one in the land of _sets_, or at least may land many a reader's mind there, but isn't it in general the whole point that this is much more general and flexible than a quasi-ordered _set_? Using a category theoretical term like "groupoid" * * More seriously, some readers will tend to think that "preorder of subobjects" means that there is _at most one arrow_ between any two subobjects, since e.g. in descriptive set theory, "preorder" is used just for "binary relation (on a set) which is reflexive and transitive" (example: A. Louveau, C. Rosendal, Complete Analytic Equivalence Relations, Trans. Amer. Math. Soc. 357 (12) p. 4840 last paragraph) while in your sense of "preorder of subobjects" there are in general many different arrows between two subobjects. 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.

   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:

   • I was modelling “groupoid of subobjects” on your own use of “groupoid of monomorphisms” in your answer to this MO question; I recognize that said usage of yours is more precise since there, “monomorphism” is unambiguous, while the phrase “groupoid of subobjects” may leave readers wondering what definition of “subobject” is meant; still, 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
   • I know and love preorders, but isn’t “preorder of subobjects” almost-wrong, at least with the usual definition of preorder? Reasons:
   • • The word “preorder” immediately lands one in the land of sets, or at least may land many a reader’s mind there, but isn’t it in general the whole point that this is much more general and flexible than a quasi-ordered set? Using a category theoretical term like “groupoid”
   • • More seriously, some readers will tend to think that “preorder of subobjects” means that there is at most one arrow between any two subobjects, since e.g. in descriptive set theory, “preorder” is used just for “binary relation (on a set) which is reflexive and transitive” (example: A. Louveau, C. Rosendal, Complete Analytic Equivalence Relations, Trans. Amer. Math. Soc. 357 (12) p. 4840 last paragraph) while in your sense of “preorder of subobjects” there are in general many different arrows between two subobjects.

   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.

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexIf 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.

   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.

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeJul 14th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI 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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexRe #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.

   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.

7. • CommentRowNumber7.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexRe #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", * the choice of two _isomorphic_ but unequal subobjects $m$ and $m'$ with $cod(m)=cod(m')$ _picks out precisely one isomorphism_ from the in general many isomorphisms between $m$ and $m'$. 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](https://golem.ph.utexas.edu/category/2017/04/elementary_1topoi.html). 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:

   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”,

   • the choice of two isomorphic but unequal subobjects $m$ and $m'$ with $cod(m)=cod(m')$ picks out precisely one isomorphism from the in general many isomorphisms between $m$ and $m'$.

   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. ]

8. • CommentRowNumber8.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 16th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexTo 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](https://mathoverflow.net/questions/184196/concise-definition-of-subobjects) > 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.

   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.

9. • CommentRowNumber9.
   • CommentAuthorPeter Heinig
   • CommentTimeJul 14th 2017
   • (edited Jul 14th 2017)
   • PermaLink
   Author: Peter Heinig
   Format: MarkdownItexAnother 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](https://mathoverflow.net/questions/184196/concise-definition-of-subobjects) is consistent with what I wrote in #7 of this thread.

   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.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeJul 14th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex> 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.

    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.

11. • CommentRowNumber11.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 14th 2017
    • (edited Jul 14th 2017)
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #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.

    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.

12. • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeJul 15th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexYes, I agree that Fetisov is wrong.

    Yes, I agree that Fetisov is wrong.

13. • CommentRowNumber13.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 15th 2017
    • (edited Jul 15th 2017)
    • PermaLink
    Author: Peter Heinig
    Format: MarkdownItexMany 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](https://nforum.ncatlab.org/discussion/1420/inducing-the-structure-of-a-vcategory-on-v-for-v-symmetric-monoidal-closed/): 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](https://nforum.ncatlab.org/discussion/1420/inducing-the-structure-of-a-vcategory-on-v-for-v-symmetric-monoidal-closed/), 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 [[clique|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 [[coherence theorem for monoidal categories|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 <a href="http://ncatlab.org/nlab/show/clique#monoidal_strictifications_6">here</a>, 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.

    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.

14. • CommentRowNumber14.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 15th 2017
    • PermaLink
    Author: DavidRoberts
    Format: MarkdownItexNote 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.

    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.

15. • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 15th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexRe #13: yes! That's certainly one of the contexts I had in mind; good that you picked up on it.

    Re #13: yes! That’s certainly one of the contexts I had in mind; good that you picked up on it.

16. • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 15th 2017
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI added a parenthetical on well-powered categories to [[poset of subobjects]].

    I added a parenthetical on well-powered categories to poset of subobjects.

17. • CommentRowNumber17.
    • CommentAuthorHurkyl
    • CommentTimeMay 4th 2020
    • PermaLink
    Author: Hurkyl
    Format: MarkdownItexAdded paragraphs on the contravariant poset of subobjects functor. <a href="https://ncatlab.org/nlab/revision/diff/poset+of+subobjects/12">diff</a>, <a href="https://ncatlab.org/nlab/revision/poset+of+subobjects/12">v12</a>, <a href="https://ncatlab.org/nlab/show/poset+of+subobjects">current</a>

    Added paragraphs on the contravariant poset of subobjects functor.

    diff, v12, current

18. • CommentRowNumber18.
    • CommentAuthornLab edit announcer
    • CommentTimeNov 14th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadded section on the subobject poset functor and on the relation to hyperdoctrines Anonymous <a href="https://ncatlab.org/nlab/revision/diff/poset+of+subobjects/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/poset+of+subobjects/17">v17</a>, <a href="https://ncatlab.org/nlab/show/poset+of+subobjects">current</a>

    added section on the subobject poset functor and on the relation to hyperdoctrines

    Anonymous

    diff, v17, current