Not signed in (Sign In)

Not signed in

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

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorziggurism
    • CommentTimeMar 10th 2020
    • (edited Mar 10th 2020)

    In the discussion at the bottom of monoidal category, we read:

    In fact a strict monoidal category is just a monoid internal to the category Cat. Unfortunately this definition is circular, since to define a monoid internal to Cat, we need to use the fact that Cat is a monoidal category!

    And then later

    For example, you can define a monoidal category to be a pseudomonoid internal to the 2-category Cat — but nobody knew how to define these concepts until they knew what a monoidal category is!

    Doesn’t the same circularity afflict the definition of monoidal category that’s on the page? For example, the associator is given as

    a:(()())()()(()()) a \;\colon\; ((-)\otimes (-)) \otimes (-) \overset{\simeq}{\longrightarrow} (-) \otimes ((-)\otimes(-))

    But this doesn’t make sense if taken literally. You cannot have a natural transformation between functors on different domains, and the domain of these functors are not the same. The domain of the left functor is (𝒞×𝒞)×𝒞(\mathcal{C}\times \mathcal{C})\times\mathcal{C} whereas the domain of the right functor is 𝒞×(𝒞×𝒞)\mathcal{C}\times (\mathcal{C}\times\mathcal{C}). Of course those two categories are isomorphic, and using that isomorphism, we can make sense of the definition. But that’s using the monoidal structure of Cat\text{Cat}! We’re being circular in exactly the same way as we would if we defined a monoidal category as a (pseudo)monoid in the monoidal (2-)category Cat\text{Cat}!

    I guess it’s not circular in any formal sense, since we can just observe that any cartesian category has canonical isomorphisms (𝒞×𝒞)×𝒞𝒞×(𝒞×𝒞)(\mathcal{C}\times \mathcal{C})\times\mathcal{C}\cong \mathcal{C}\times (\mathcal{C}\times\mathcal{C}) and we can just insert that into the definition as needed, without commenting that it is part of a monoidal structure on the ambient category. The same applies to any monoid in any cartesian category. In particular, I think it’s not formally circular to define a (weak/strict) monoidal category as a (pseudo) monoid in Cat\text{Cat}.

    Shouldn’t that equivalent definition be mentioned higher in the article, since it’s valid and not really circular?

    And shouldn’t the article be more explicit about this, about using the cartesian associator and unitors of Cat\text{Cat}, given that it’s basically an article about the need to be careful and rigorous about the axioms of associators and monoidal structures?

    Also, is there some more coherent, higher categorical way out of this circularity, other than than just capping it with a cartesian structure at some level of the higher categorical ladder?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMar 12th 2020

    In particular, I think it’s not formally circular to define a (weak/strict) monoidal category as a (pseudo) monoid in Cat.

    Yes, I agree.

    Shouldn’t that equivalent definition be mentioned higher in the article, since it’s valid and not really circular?

    Well, it is! You just pointed out where it’s mentioned. But yes, I think it would be fine to mention it higher up on the page too.

    And shouldn’t the article be more explicit about this, about using the cartesian associator and unitors of Cat\text{Cat}, given that it’s basically an article about the need to be careful and rigorous about the axioms of associators and monoidal structures?

    No, I don’t think so, just as a definition of monoid (an ordinary monoid in Set, not a monoid in an arbitrary monoidal category) doesn’t generally mention using the associator in Set. That would be just overcomplicating things and making the definition hard to read, especially for a newcomer who has never seen a notion of monoidal category (or perhaps even of “monoid in a monoidal category”) before.

    Also, is there some more coherent, higher categorical way out of this circularity, other than than just capping it with a cartesian structure at some level of the higher categorical ladder?

    I don’t think so.

    • CommentRowNumber3.
    • CommentAuthorziggurism
    • CommentTimeMar 13th 2020
    • (edited Mar 13th 2020)

    And shouldn’t the article be more explicit about this, about using the cartesian associator and unitors of Cat\text{Cat}, given that it’s basically an article about the need to be careful and rigorous about the axioms of associators and monoidal structures?

    No, I don’t think so, just as a definition of monoid (an ordinary monoid in Set, not a monoid in an arbitrary monoidal category) doesn’t generally mention using the associator in Set. That would be just overcomplicating things and making the definition hard to read, especially for a newcomer who has never seen a notion of monoidal category (or perhaps even of “monoid in a monoidal category”) before.

    Ok sure, I can appreciate that we don’t want to muddy up a definition and make it hard to understand. As you say, the article on monoids doesn’t mention the associator, and it would be very confusing if it did. But then the article monoid in a monoidal category does, for those who want it. The problem arises because we don’t have (and probably don’t want) separate articles for monoidal category and monoidal category in a monoidal bicategory. If we did, such technicalities could go in that latter article.

    I guess I’m not suggesting to rewrite the definition of monoidal category, but instead maybe a paragraph disclaimer somewhere below the definition, saying something about this. Because as it stands now, this issue isn’t mentioned anywhere on nLab about monoidal categories! A confused learner who can’t understand the domains of these maps literally cannot find a correct answer anywhere on nLab.

    This isn’t some purely academic concern over excess rigor. I came to this forum to talk about this issue specifically because a colleague was trying to understand the definition of monoidal category. He came to me when it didn’t make sense. I was surprised to find it really doesn’t make sense, and I had never noticed. When I told him what the resolution must be, he was actually angry that this source that purports to be careful about domains, and constantly harps on the difference between equality and isomorphism and the need to keep track of isomorphisms, is just completely sweeping this isomorphism under the rug.

    You can also see confusion over this issue at this m.se post and this one. I don’t think the answers there have fully captured the cool idea that’s to be found here on nLab, about microcosm principle where the little associator is only defined up to the big associator. They just say in handwavy fashion “they’re isomorphic, treat them the same”.

    So I think we should give a carefully cloistered parenthetical remark well-below the definition of a monoidal structure. Perhaps with a link to pseudomonoid (actually, pseudomonoid is the “monoidal category in a monoidal bicategory” article, isn’t it?), where more detail could be given.

    Just to have a concrete idea of what that might look like so we can better decide how much it detracts from the readability and accessibility of the article, I have gone ahead and edited a version with the two changes discussed (mention earlier in the definition section that a monoidal category is just a monoid, and then a paragraph about the reliance on the parent 2-category’s monoidal structure). If it looks terrible we can always revert.

    • CommentRowNumber4.
    • CommentAuthorvarkor
    • CommentTimeMar 13th 2020
    • (edited Mar 13th 2020)

    If I understand correctly, there’s a misunderstanding here that I don’t think has been addressed (here, or in the similar MathOverflow questions), which is this: the structure of the objects in the image of a functor does not need to be the same as the structure of the domain of the functor. That is, there is no reason why F:(𝒞×𝒞)×𝒞𝒞F : (\mathcal{C} \times \mathcal{C}) \times \mathcal{C} \to \mathcal{C} should not send ((a,b),c)((a, b), c) to a(bc)a \otimes (b \otimes c) (we can certainly show this defines a functor explicitly, albeit not quite as conveniently as defining the functor as a composite). In the same way, it’s not true that the LHS and RHS of the associator are defined on two different domain categories; rather, there is an ambiguity when we don’t state what the domains are. We could pick any of (𝒞×𝒞)×𝒞(\mathcal{C} \times \mathcal{C}) \times \mathcal{C}, 𝒞×(𝒞×𝒞)\mathcal{C} \times (\mathcal{C} \times \mathcal{C}) or (if we choose unbiased products) 𝒞×𝒞×𝒞\mathcal{C} \times \mathcal{C} \times \mathcal{C} for both sides of the associator. Thinking there is a canonical choice is getting confused about the structure of the categories versus structure of the objects (though if you want to define the functors as composites of the tensor product bifunctor and the identity functor, there are “obvious” choices for each side that do not coincide).

    In this sense, I don’t think the structure of the cartesian product of categories is really relevant to the coherence of monoidal categories: we just need to pick a choice of domain and stick to it. However, it would be helpful to state exactly which functors the associator (and friends) defines a natural transformation between.

    • CommentRowNumber5.
    • CommentAuthorziggurism
    • CommentTimeMar 13th 2020

    That is, there is no reason why F:(𝒞×𝒞)×𝒞𝒞F : (\mathcal{C} \times \mathcal{C}) \times \mathcal{C} \to \mathcal{C} should not send ((a,b),c)((a, b), c) to a(bc)a \otimes (b \otimes c) (we can certainly show this defines a functor explicitly, albeit not quite as conveniently as defining the functor as a composite).

    Sure, the issue only arises if we want to define the functor as a composite of the functor

    :𝒞×𝒞𝒞 \otimes \;\colon\; \mathcal{C} \times \mathcal{C} \longrightarrow \mathcal{C}

    But we do want to define it that way, so it is an issue.

    • CommentRowNumber6.
    • CommentAuthorvarkor
    • CommentTimeMar 13th 2020

    But we do want to define it that way, so it is an issue.

    I don’t agree. The definition as given gives the associator in terms of its image. This is imprecise, so we have to choose how to interpret it (though the imprecision might be excused as the sensible choices are all equivalent anyway). You’ve picked one definition, which is perfectly fine, but does require one to resolve the issue of cartesian products of categories, as you point out. However, if you pick a different definition of the associator (still subject to the given image), then we don’t have the same issue. For instance, if we define it concretely, rather than as a composite, then there is no issue: we can just use the universal property of the cartesian product. If this avoids the issues you mentioned, it seems like a natural choice to me, so I think the assumption that the definition as composites is the one we want is questionable.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeMar 13th 2020

    I don’t think it makes sense to talk about the “image” of a functor or natural transformation, not in this sense. It’s true that we can consider ()- \otimes (- \otimes -) as a functor defined on (C×C)×C(C\times C)\times C, but the way we do that is by composing the obvious functor defined on C×(C×C)C\times (C\times C) with the associator. It’s true that we could explicitly define the entire functor ()- \otimes (- \otimes -) on (C×C)×C(C\times C)\times C without referring explicitly to C×(C×C)C\times (C\times C), but in practice we still need to know that it is obtained by composing the functor \otimes with itself, so I don’t really think that buys us anything.

    pseudomonoid is the “monoidal category in a monoidal bicategory” article, isn’t it?

    Yep!

    • CommentRowNumber8.
    • CommentAuthorvarkor
    • CommentTimeMar 14th 2020
    • (edited Mar 14th 2020)

    Okay, I accept that explicitly defining the functor is unhelpful. However, it does seem reasonable to define the the associator using the universal property of the product (using simply the projections), which avoids necessitating the formalism of “associator” or “monoidal (2-)category” at all. This seems like it would let us get around any circularity or recourse to “the same definition, one level higher” (assuming one is willing to accept cartesian structure)?

    (Apologies if I seem contrary: I want to make sure I understand the subtleties, so I can be precise when thinking about these sorts of issue myself.)

    • CommentRowNumber9.
    • CommentAuthorziggurism
    • CommentTimeMar 14th 2020

    One can choose whether or not to mention the “macrocosm” monoidal structure or not. Whether you use it implicitly or explicitly, you do have to use it though. I think we are all in agreement (meaning you varkor, me, Mike) that it is more intuitive and a gentler introduction to make it implicit. To only mention that (𝒞×𝒞)×𝒞𝒞×(𝒞×𝒞)(\mathcal{C}\times \mathcal{C})\times\mathcal{C} \cong \mathcal{C}\times (\mathcal{C}\times\mathcal{C}) and not mention “associators” or “monoidal 2-structures”.

    My complaint was that we didn’t even do that much. The issue went totally unremarked on nLab. That seemed bad to me.

    Eventually, in preparation for pseudomonoids or monoidal objects in a generic monoidal 2-category, I think you do need to be explicit those topics. Exactly the best place to do that is something to discuss. It could be near the top of this article, lower down this article, or only in the pseudomonoid article.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeMar 14th 2020

    Re #8, yes, I think that’s the point made in #1, that cartesian structure “at the top” is the way out of the circularity.

    • CommentRowNumber11.
    • CommentAuthorvarkor
    • CommentTimeMar 14th 2020

    Okay, in that case, I think I slightly misunderstood the emphasis in the original discussion. It does seem like we’re on the same page — sorry if I came across belligerently!