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

Site Tag Cloud

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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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

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.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 7th 2010

    On page 15 of Kelly, he says that we can easily verify axioms 1.3 and 1.4 by the “relation of ee to π\pi” that the “Definition of M is equivalent to e(M1)=e(1e)ae(M \otimes 1)=e(1\otimes e)a. Could someone explain what that means and maybe do a quick example? I’ve got no idea.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2010
    • (edited Jun 7th 2010)

    Sure: it’s just restating how MM is defined by universality, via the counit ee of the hom-tensor adjunction. When we say that f:A[B,C]f: A \to [B, C] is uniquely determined by some map g:ABCg: A \otimes B \to C, we mean precisely that ff is the unique map such that

    g=(ABf1 B[B,C]Be B,CC)g = (A \otimes B \stackrel{f \otimes 1_B}{\to} [B, C] \otimes B \stackrel{e_{B, C}}{\to} C)

    That’s the recipe. Then, applied to page 15, f=Mf = M, and g=e(1e)ag = e(1 \otimes e)a.

    Hopefully that makes sense without an example.

    • CommentRowNumber3.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 7th 2010
    • (edited Jun 7th 2010)

    Okay, so in general, if L is left adjoint to R,

    f:A->R(C) is uniquely determined by a map g:L(A)->C when

    g=L(A)L(f)L(R(C))ε CC.g = L(A) \stackrel{L(f)}{\to} L(R(C)) \stackrel{\varepsilon_C}{\to} C.

    Could you explain the reasoning behind that? I have very little experience with the unit/counit formulations of adjoints. The Hom-set definition has served me well until now.

    Edit: Actually, I’m looking at it, and I just don’t see how to do the computation that we have that equality (in yours).

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2010
    • (edited Jun 7th 2010)

    Heh, probably you should read Mac Lane. :-) Okay, anyway, it’s good you ask.

    You are probably much more familiar with examples coming from the dual direction. Let U:GrpSetU: Grp \to Set from groups to sets be the usual forgetful functor. When we say “F(X)F(X) is the free group generated by a set XX”, we mean there is a function η X:XU(F(X))\eta_X: X \to U(F(X)) which is universal among functions from XX to the underlying set of a group, which means in turn that given a function f:XU(G)f: X \to U(G), there is a unique group homomorphism g:F(X)Gg: F(X) \to G such that

    f=(Xη XU(F(X))U(g)U(G))f = (X \stackrel{\eta_X}{\to} U(F(X)) \stackrel{U(g)}{\to} U(G))

    So here η X\eta_X is a component of the unit of the adjunction FUF \dashv U, and we are giving the dual recipe for the relationship between the map g:F(X)Gg: F(X) \to G and the map f:XU(G)f: X \to U(G) in terms of the unit.

    Now let’s work more generally. Suppose given functors L:CDL: C \to D, R:DCR: D \to C and the structure of an adjunction in the form of a natural isomorphism

    Ψ c,d:hom D(L(c),d)hom C(c,R(d))\Psi_{c, d}: \hom_D(L(c), d) \cong \hom_C(c, R(d))

    Now the idea is that, a la Yoneda, Ψ\Psi should be completely describable in terms of what it does to identity maps. With that in mind, define the unit η:1 CRL\eta : 1_C \to R L by the formula η c=Ψ c,L(c)(1 L(c))\eta_c = \Psi_{c, L(c)}(1_{L(c)}). Dually, define the counit ε:LR1 D\varepsilon : L R \to 1_D by the formula ε d=Ψ R(d),d 1(1 R(d))\varepsilon_d = \Psi^{-1}_{R(d), d}(1_{R(d)}). Then given g:L(c)dg: L(c) \to d, the claim is that

    Ψ c,d(g)=(cη cR(L(c))R(g)R(d))\Psi_{c, d}(g) = (c \stackrel{\eta_c}{\to} R(L(c)) \stackrel{R(g)}{\to} R(d))

    and I’ll leave that as an exercise in Yoneda yoga, applied to hom D(L(c),)hom C(c,R())\hom_D(L(c), -) \to \hom_C(c, R(-)). By duality, given f:cR(d)f: c \to R(d),

    Ψ c,d 1(f)=(L(c)L(f)L(R(d))ε dd)\Psi^{-1}_{c, d}(f) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d)

    Finally, these operations should obviously be mutually inverse, but that can again be entirely encapsulated Yoneda-wise in terms of the effect on identity maps. Thus, if η cΨ c,L(c)(1 L(c))\eta_c \coloneqq \Psi_{c, L(c)}(1_{L(c)}), the recipe just given for Ψ 1\Psi^{-1} yields back

    1 L(c)=(L(c)L(η c)LRL(c)ε L(c)L(c))1_{L(c)} = (L(c) \stackrel{L(\eta_c)}{\to} L R L(c) \stackrel{\varepsilon_{L(c)}}{\to} L(c))

    and this is one of the famous triangular equations: 1 L=(LLηLRLεLL)1_L = (L \stackrel{L \eta}{\to} L R L \stackrel{\varepsilon L}{\to} L). By duality, we have the other triangular equation 1 R=(RηRRLRRεR)1_R = (R \stackrel{\eta R}{\to} R L R \stackrel{R \varepsilon}{\to} R). These two triangular equations are enough to guarantee that the recipes for Ψ\Psi and Ψ 1\Psi^{-1} are indeed mutually inverse.

    One thing that you often hear is that the definition of adjunctions via units and counits is an “elementary” definition (so that by implication, the formulation in terms of hom-functors is not elementary). This means that whereas the hom-functor formulation relies on a background category of sets, the formulation in terms of units and counits is purely in the first-order language of categories and makes no reference to a background model of set theory. Thus, it would be a perfectly serviceable definition of adjunction without assumptions of local smallness.

    Edit: back to your last edit at 3, hopefully this comment will clear everything up, possibly with the aid of pencil and paper in hand.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2010
    • (edited Jun 7th 2010)

    To forestall some possible frustration with my waving a wand of duality in the last comment (which is perfectly legitimate of course, since the principle of duality is an explicit formal statement), I’ll say more explicitly how it works for the equation that seemed to be bothering you in comment #2.

    The claim is that Ψ c,d 1:hom C(c,R(d))hom D(L(c),d)\Psi^{-1}_{c, d}: \hom_C(c, R(d)) \to \hom_D(L(c), d) can be defined by the formula

    Ψ c,d 1(f:cR(d))=(L(c)L(f)L(R(d))ε dd)\Psi^{-1}_{c, d}(f: c \to R(d)) = (L(c) \stackrel{L(f)}{\to} L(R(d)) \stackrel{\varepsilon_d}{\to} d)

    where ε dΨ R(d),d 1(1 R(d))\varepsilon_d \coloneqq \Psi^{-1}_{R(d), d}(1_{R(d)}). This is by appeal to the proof of the Yoneda lemma applied to the transformation

    Ψ ,d 1:hom C(,R(d))hom D(L(),d)\Psi^{-1}_{-, d}: \hom_C(-, R(d)) \to \hom_D(L(-), d)

    For the naturality of Ψ 1\Psi^{-1} in the argument ()(-) would imply that given f:cR(d)f: c \to R(d), we have a commutative square

    hom C(R(d),R(d)) Ψ R(d),d 1 hom D(L(R(d)),d) hom C(f,R(d)) hom D(L(f),d) hom C(c,R(d)) Ψ c,d 1 hom D(L(c),d)\array{ \hom_C(R(d), R(d)) & \stackrel{\Psi^{-1}_{R(d), d}}{\to} & \hom_D(L(R(d)), d) \\ \hom_C(f, R(d)) \downarrow & & \downarrow \hom_D(L(f), d) \\ \hom_C(c, R(d)) & \underset{\Psi^{-1}_{c, d}}{\to} & \hom_D(L(c), d) }

    Chasing the element 1 R(d)1_{R(d)} down and then across, we get f:cR(d)f: c \to R(d) and then Ψ c,d 1(f)\Psi^{-1}_{c, d}(f). Chasing across and then down, we get ε d\varepsilon_d and then ε dL(f)\varepsilon_d \circ L(f). This completes the verification of the claim.

    • CommentRowNumber6.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 7th 2010

    Thanks for the help, Todd! You should add that to the page on adjunctions.

    Also, when I was looking at the computation, in the book, I was getting confused by the suppression of subscripts. I think that we need better notation.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2010

    By the way, something along these lines I had started adding recently to adjoint functor in the section In terms of universal morphisms.

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeJun 7th 2010

    I wrote:

    By the way, something along these lines I had started adding recently to adjoint functor in the section In terms of universal morphisms.

    But I hope Todd finds the time and energy to expand and improve all this. Also it would be great to see the extranatural proof of the co-Yoneda lemma in the relevant nLab entry.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2010

    I just entered the proof of the co-Yoneda lemma I gave above at co-Yoneda lemma. More could be added there (including links), but I did this in a hurry.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2010

    Added content to adjunction based on comments above. Links still needed.

    • CommentRowNumber11.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 7th 2010
    • (edited Jun 7th 2010)

    @Todd: I’m sorry, but I still dont understand how to do the computation

    e(M1)=e(1e)ae(M\otimes 1)=e(1\otimes e)a. I have the diagram drawn out, but it’s the matter of showing that it commutes that I guess I’m not getting.

    Unless… since M is the map ψ(e(1e)a)\psi(e(1\otimes e)a), then psi 1(M)=L([y,z][x,y])L(M)L([x,z])ezpsi^{-1}(M)=L([y,z]\otimes [x,y])\stackrel{L(M)}{\to}L([x,z]) \stackrel{e}{\to} z, but psi 1(M)=e(1e)apsi^{-1}(M)=e(1\otimes e)a?

    Edit: all clear nevermind.

    • CommentRowNumber12.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 8th 2010

    Alright, I’ve gotten all of the above stuff, but now how do we check axiom 1.3? What does that whole thing tell us about 1M1\otimes M?

    We’re trying to show now that M(M1)=M(1M)aM(M\otimes 1)=M(1\otimes M)a.

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2010
    • (edited Jun 8th 2010)

    Right. Here goes.

    Preliminaries: by Mac Lane’s coherence theorem, we may assume the closed symmetric monoidal MM is strict monoidal, to avoid the nuisance of shuffling around associativities. (I am prepared to discuss this point further if needed.) To save typographical space, I’ll denote the internal hom [b,a][b, a] in VV by a ba^b. Thus the composition MM takes the form a bb ca ca^b \otimes b^c \to a^c, and we have an adjunction isomorphism of the form

    Φ ydz:hom V(y,z d)hom V(yd,z).\Phi_{y d z}: \hom_V(y, z^d) \cong \hom_V(y \otimes d, z).

    A handy lemma we will need is that Φ(xfygz d)=(xdfdydΦ(g)z)\Phi(x \stackrel{f}{\to} y \stackrel{g}{\to} z^d) = (x \otimes d \stackrel{f \otimes d}{\to} y \otimes d \stackrel{\Phi(g)}{\to} z). That can be proven using the recipe for Φ\Phi in terms of the counit, that we discussed above.

    We are trying to prove that the following diagram “D” commutes:

    a bb cc d a bM a bb d Mc d M a cc d M a d\array{ a^b \otimes b^c \otimes c^d & \stackrel{a^b \otimes M}{\to} & a^b \otimes b^d \\ M \otimes c^d \downarrow & & \downarrow M \\ a^c \otimes c^d & \underset{M}{\to} & a^d }

    It is enough to check that we get the same result on applying Φ\Phi to both legs of D. First, hit the leg going across and then down with Φ\Phi. By the lemma, this is the composite

    a bb cc dd1Mda bb dd1ea bbea(1)a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes M \otimes d}{\to} a^b \otimes b^d \otimes d \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (1)

    The first two arrows in (1) go across then down in a square:

    a bb cc dd 1M1 a bb dd 11e 1e a bb cc 1e a bb\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes M \otimes 1}{\to} & a^b \otimes b^d \otimes d \\ 1 \otimes 1 \otimes e \downarrow & & \downarrow 1 \otimes e \\ a^b \otimes b^c \otimes c & \underset{1 \otimes e}{\to} & a^b \otimes b }

    which commutes (just hit the equation e(M1)=e(1e)e(M \otimes 1) = e(1 \otimes e) with 11 \otimes -, here a ba^b \otimes -). So we can replace the composite of the first two arrows in (1) with the leg which goes down then across; thus the composite in (1) equals the following composite:

    a bb cc dd11ea bb cc1ea bbea(2)a^b \otimes b^c \otimes c^d \otimes d \stackrel{1 \otimes 1 \otimes e}{\to} a^b \otimes b^c \otimes c \stackrel{1 \otimes e}{\to} a^b \otimes b \stackrel{e}{\to} a \qquad (2)

    Okay, now hit the other leg of D with Φ\Phi. Applying the lemma again, the result is

    a bb cc ddM1da cc dd1ea ccea(3)a^b \otimes b^c \otimes c^d \otimes d \stackrel{M \otimes 1 \otimes d}{\to} a^c \otimes c^d \otimes d \stackrel{1 \otimes e}{\to} a^c \otimes c \stackrel{e}{\to} a \qquad (3)

    Now the composites of (2) and (3) form the outer perimeter of a diagram

    a bb cc dd 11e a bb cc 1e a bb M11 M1 e a cc dd 1e a cc e a\array{ a^b \otimes b^c \otimes c^d \otimes d & \stackrel{1 \otimes 1 \otimes e}{\to} & a^b \otimes b^c \otimes c & \stackrel{1 \otimes e}{\to} & a^b \otimes b \\ M \otimes 1 \otimes 1 \downarrow & & M \otimes 1 \downarrow & & \downarrow e \\ a^c \otimes c^d \otimes d & \underset{1 \otimes e}{\to} & a^c \otimes c & \underset{e}{\to} & a }

    which commutes: the left square commutes by functoriality of \otimes, and the right square is another instance of the all-important equation e(M1)=e(1e)e(M \otimes 1) = e(1 \otimes e). Hence the composites (2) and (3) are equal, and we are done.

    (You owe me one. :-) )

    • CommentRowNumber14.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 8th 2010

    (You owe me one. :-) )

    I owe you a bunch already =p.

    If we didn’t use the coherence theorem, is the proof pretty similar?

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2010

    If we didn’t use the coherence theorem, is the proof pretty similar?

    Very similar, yes. But probably much harder to typeset.

    You probably didn’t know this, but the topic of my dissertation was coherence theorems. Specifically the coherence problem for closed symmetric monoidal categories (which formal diagrams commute?) and related structures like star-autonomous categories.

    • CommentRowNumber16.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 8th 2010
    • (edited Jun 8th 2010)

    So Todd, when you’re working things out when you have coherence diagrams, do you do something like prove the strict version first, then worry about keeping track of coherence afterwards?

    I’m trying to figure out strategies to get the hang of this, and I wonder if it’s possible to do a strict proof, then weaken it.

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2010

    The all-too-brief reply is that you never have to worry or weaken later: if the sentence to be decided is a non-evil sentence in the language of monoidal categories, then the truth value is automatically reflected and preserved by monoidal equivalences. So insofar as any monoidal category is monoidally equivalent to a strictified monoidal category, one may as well assume that the model in which one is working is strict monoidal, and let Mac Lane’s theorem worry about the rest so to speak – you never need to go back and “improve” the proof to take care of weakening. Commutativity of diagrams (i.e., equality of morphisms belonging to the same hom-set) falls under that heading of non-evil sentences.

    I began to write out a longer reply to say this much more convincingly; what is really needed is to develop a clear picture of how monoidal strictifications work, something I learned by reading stuff by Joyal and/or Street (as in Braided Tensor Categories or Geometry of Tensor Calculus I). But I realized I won’t have time to do this now, and it may be a while before I can return to it (very busy day tomorrow). I should have time by Wednesday if not before to explain it further.

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2010

    Okay, I found a bit more time, so let me make some remarks on how monoidal strictification works and how it leads to an elegant resolution of the concerns about reinstating associativities in diagrams.

    Most people, when they first hear about strictifications, imagine that strictifying a monoidal category is like taking a quotient, in order to identify associativities with identities. That’s actually the wrong picture, and it leads to a lot of confusion. The right picture is that a monoidal category MM can be monoidally embedded in a strict monoidal category M stM^{st}, in which associativity and unit isomorphisms of MM are assembled into what Joyal calls “contractible networks”, or cliques (aka anaobjects). The cliques that so arise are then the objects of the strictification.

    So, for example, a 4-fold tensor product like (a b(b cc d))d(a^b \otimes (b^c \otimes c^d)) \otimes d is a vertex in a clique which consists of all five ways of bracketing a bb cc dda^b \otimes b^c \otimes c^d \otimes d and the groupoid of associativities between them. Or more precisely, it consists of the infinitely many such bracketings with units inserted (e.g., ((a bI)(b cc d))(Id)((a^b \otimes I) \otimes (b^c \otimes c^d)) \otimes (I \otimes d)), as objects of the groupoid generated by associativity and unit isomorphisms between them. By Mac Lane’s coherence theorem (“all diagrams commute”), there is exactly one morphism between any two vertices in the clique, meaning that the groupoid is equivalent to a terminal groupoid, and therefore contractible.

    Formally, a clique in a category CC consists of a contractible groupoid GG and a functor F:GCF: G \to C. A morphism between two cliques (G,F:GC)(G, F: G \to C), (G,F:GC)(G', F': G' \to C) is a collection of morphisms F(g)F(g)F(g) \to F'(g'), where (g,g)(g, g') ranges over Ob(G)×Ob(G)Ob(G) \times Ob(G'), making all triangles in sight commute. (In fact, by contractibility, any one of the F(g)F(g)F(g) \to F'(g') uniquely determines all the rest.) To form the monoidal strictification M stM^{st}, we take as objects those cliques in the monoidal category MM 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 stM^{st} are defined to be morphisms of cliques. The precise description is laid out here, where it is indicated that the evident embedding i:MM sti: M \to M^{st} is an equivalence in MonCatMonCat.

    In any case, because MM is embedded in M stM^{st}, any diagram we are trying to prove commutative in MM is physically there in M stM^{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)F(g)F(g) \to F'(g') of, and uniquely determines, an identity morphism of cliques. Therefore any such associativity in MM is reinterpreted as an identity in M stM^{st}, and the diagram we are trying to prove commutative in MM uniquely generates a corresponding “larger” diagram of cliques in the strict monoidal category M stM^{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 stM^{st}, and the original diagram in MM, which is embedded in the clique diagram, is then automatically commutative as well.

    One may have to practice visualizing this before it all sinks in, but it’s a tremendously potent principle.

    • CommentRowNumber19.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 9th 2010

    That’s precisely the way I imagined doing it, believe it or not.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeJun 9th 2010

    That’s a great explanation, Todd; maybe it should go on the nlab at coherence theorem for monoidal categories. It’s not the way I usually think of strictification, though. In my head, the fundamental functor is not the strong monoidal embedding MM stM\to M^{st}, but a strict monoidal functor M stMM^{st} \to M, which happens to have a strong monoidal section forming a monoidal equivalence. From this point of view, the way coherence works with diagrams is that you draw the diagram in the strict world M stM^{st}, where it commutes, and then then map it forward into MM to get a corresponding diagram that also commutes there. Moreover, these two functors are the unit and counit of a strict 2-adjunction

    () st:MonCatStrMonCat:incl(-)^{st} : MonCat \rightleftarrows StrMonCat : incl

    where the left adjoint is strictification and the right adjoint is the inclusion. In particular, the strictification has a universal property: strict monoidal functors out of M stM^{st} are the same as strong monoidal functors out of MM.

    • CommentRowNumber21.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 9th 2010

    Strong monoidal functor = weak monoidal functor?

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeJun 9th 2010

    Yes, “strong” always means up to isomorphism (as opposed to lax/colax). It’s unfortunate that when people say “weak” to mean up to isomorphism (as opposed to strict), then it means that strong=weak. (-:

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 9th 2010
    • (edited Jun 9th 2010)

    @Mike #20: sorry, I’m confused. I think I agree that we have the adjunction you gave at the bottom (so that my explanation involved the unit of the adjunction, Mi(M st)M \to i(M^{st})). So if MM starts out being strict, we have a counit (i(M)) stM(i(M))^{st} \to M which is strict monoidal. But I don’t see a strict monoidal M stMM^{st} \to M for non-strict MM. I do see strong monoidal retractions M stMM^{st} \to M of the unit which are non-canonical.

    • CommentRowNumber24.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 9th 2010

    So is the page on the lab incorrect?

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 9th 2010

    What statement on what page?

    • CommentRowNumber26.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 9th 2010

    Oh, I thought for some reason that your previous post was something along the lines of, “Oh, Mike, I guess I was wrong”, but rereading it now, it appears that you were confused with Mike’s statement, not that you were confused and that he was right.

    • CommentRowNumber27.
    • CommentAuthorMike Shulman
    • CommentTimeJun 9th 2010

    Hmm, sorry, Todd, you’re right and I was wrong. I think what I should have said is that there are two adjunctions:

    MonCatincl()MonCat sinclquotStrMonCat s MonCat\; \underoverset{incl}{(-)'}{\rightleftarrows} \;MonCat_s \;\underoverset{incl}{quot}{\rightleftarrows} \;StrMonCat_s

    where MonCat sMonCat_s denotes non-strict monoidal categories and strict monoidal functors. The left adjoint quotquot is the “wrong way to prove coherence” by taking a quotient, but its composite with the “pseudo morphism classifier” ()(-)' is a correct strictification functor () st(-)^{st}, i.e. M st=quot(M)M^{st} = quot(M'). The strict functor I was thinking of is the counit MMM'\to M, which is a surjective equivalence in MonCatMonCat (but not in MonCat sMonCat_s).

    • CommentRowNumber28.
    • CommentAuthorHarry Gindi
    • CommentTimeJun 9th 2010

    How do you describe the pseudo morphism classifier?

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeJun 9th 2010

    The quick and dirty way is to say that its objects are formal parenthesized strings of objects of M, and the functor MMM' \to M is fully faithful. The elegant way is to say that it’s a codescent object, as described in Steve Lack’s paper “codescent objects and coherence.”

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 10th 2010

    @Mike #27 – thanks; that makes sense.

    I made a little beginning for coherence theorem for monoidal categories. Rather a lot more to be filled in.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeJun 10th 2010

    I think I don’t understand the relationship between the “all diagrams commute” coherence theorem and the strictification theorem as well as I thought I did. A naive version of the “all diagrams commute” theorem of course follows from the strictification theorem since all diagrams commute in a strict monoidal category, while your description shows where the all-diagrams-commute theorem comes into proving the strictification theorem. (In other versions of the strictification theorem, it comes in in other places.) But there’s a more abstract version of the all-diagrams-commute theorem which says that the free strict monoidal category on some data is equivalent to the free non-strict one; how is that related to the string of adjunctions I just wrote down?

    • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 14th 2010
    • (edited Jun 14th 2010)

    Sorry for the delay in responding to your question, Mike. I’m not sure how well the following observations answer it, but here goes.

    Let’s see: the free monoidal category F[C]F[C] generated by a category CC is, in the notation at club, F[1]CF[1] \circ C, where F[1]F[1] is the free monoidal category on one generator. When I say “free monoidal” here, this means the left adjoint to the forgetful functor

    MonCat sCatMonCat_s \to Cat

    It looks like your ():MonCatMonCat s(-)': MonCat \to MonCat_s can be described as taking a monoidal category MM, which has an underlying endospan M 0M 1M 0M_0 \leftarrow M_1 \to M_0, to a monoidal category MM' whose underlying endospan is the span composite

    F[M] 0p 0M 0M 1M 0(p 0) *F[M] 0F[M]_0 \stackrel{p_0}{\to} M_0 \stackrel{M_1}{\to} M_0 \stackrel{(p_0)^*}{\to} F[M]_0

    where p:F[M]Mp: F[M] \to M is the counit at MM of the adjunction for the monadic functor MonCat sCatMonCat_s \to Cat, and p 0p_0 is the underlying function between object-sets. So in other words, this endospan may be equivalently written (M) 1F[m] 0×F[M] 0(M')_1 \to F[m]_0 \times F[M]_0.

    The free strict monoidal category on a category CC would be C\mathbb{N} \circ C. There is a quotient functor q:F[C]=F[1]CCq: F[C] = F[1] \circ C \to \mathbb{N} \circ C (induced from the obvious functor F[1]F[1] \to \mathbb{N}) which is a monoidal equivalence, as you hinted in speaking of the abstract version of the all-diagrams-commute theorem. This induces a quotient function q 0:F[C] 0(C) 0q_0: F[C]_0 \to (\mathbb{N} \circ C)_0. Now if MM is a monoidal category, then according to what you wrote in #27, (M) 0(\mathbb{N} \circ M)_0 is the underlying object-set (M st) 0(M^{st})_0. The underlying morphism-set is quot(M) 1=(M st) 1quot(M')_1 = (M^{st})_1.

    Adopting the clique point of view on the construction of the monoidal category M stM^{st}, one connection between the string of adjunctions you wrote down and the abstract all-diagrams-commute theorem is concentrated in the statement that the following diagram is a pullback:

    (M) 1 dom M,cod M F[m] 0×F[M] 0 π q 0×q 0 (M st) 1 dom,cod (M st) 0×(M st) 0\array{ (M')_1 & \stackrel{\langle dom_{M'}, cod_{M'} \rangle}{\to} & F[m]_0 \times F[M]_0 \\ \pi \downarrow & & \downarrow q_0 \times q_0 \\ (M^{st})_1 & \underset{\langle dom, cod \rangle}{\to} & (M^{st})_0 \times (M^{st})_0 }

    where π\pi is the quotient map (M) 1quot(M) 1(M')_1 \to quot(M')_1, where quotquot is your functor MonCat sStrMonCat sMonCat_s \to StrMonCat_s.

    I think this can be understood by viewing MM' as a monoidal category of pointed cliques. (A pointed clique is exactly what one might think: a triple (g,G,F:GC)(g, G, F: G \to C) where GG is a contractible groupoid and gg is an object of GG. A morphism (g,G,F:GC)(g,G,F:GC)(g, G, F: G \to C) \to (g', G', F': G' \to C) is just the component h g,gh_{g, g'} of a morphism of cliques h:(G,F:GC)(G,F:GC)h: (G, F: G \to C) \to (G', F': G' \to C), or rather the pair (h gg,h)(h_{g g'}, h).)

    Then the functor Mquot(M)M' \to quot(M') can be understood as the process of forgetting the point of the pointed clique.

    • CommentRowNumber33.
    • CommentAuthorMike Shulman
    • CommentTimeJun 15th 2010

    Thanks Todd! Let me rephrase some of that in language more familiar to me. I think what you wrote about span composites is correct, but I’d be more inclined to say the same thing by saying that MM' is the (bo,ff) factorization of the counit p:F[M]Mp\colon F[M] \to M. And similarly, saying that that square is a pullback is just saying that the functor MM stM' \to M^{st} is fully faithful. (In fact, of course, it is an equivalence, since both MM' and M stM^{st} are equivalent to MM.)

    I don’t quite understand the pointed cliques yet. Partly I don’t see why my M stM^{st}, being the left adjoint as above, should necessarily the same as your M stM^{st} constructed using cliques – is it?

    But let me say something different which this triggered in my head, namely how to deduce strictification from coherence. Suppose we know that F[M]F s[M]F[M] \to F_s[M] is an equivalence (where F sF_s denotes the free strict monoidal category). Then from some inverse to it we obtain a map F s[M]F[M]MF_s[M] \to F[M] \to M, and we can define M stM^{st} to be the (bo,ff) factorization of this. It inherits a strict monoidal structure from F s[M]F_s[M], and its map to MM is fully faithful by definition, and surjective on objects since we have MM sitting inside F s[M]F_s[M]; thus every monoidal category MM is equivalent to a strict monoidal category. This is essentially Power’s “general coherence result” for pseudoalgebras over 2-monads, composed with the equivalence FF sF \simeq F_s to turn an FF-algebra (a monoidal category) into a pseudo F sF_s-algebra (an unbiased monoidal category).

    I think a proof of coherence from strictification can also be derived with a little more work. The 2-monad morphism FF sF \to F_s induces a functor StrMonCatMonCatStrMonCat \to MonCat over CatCat, where in both 2-categories we include pseudo morphisms (i.e. strong=weak monoidal functors). This functor is clearly 2-fully-faithful, and assuming strictification, it is also essentially surjective up to equivalence; hence it is a biequivalence. Moreover, each forgetful functor MonCatCatMonCat \to Cat and StrMonCatCatStrMonCat \to Cat has a left biadjoint, namely FF and F sF_s respectively, so the fact of this equivalence over CatCat means that these biadjunctions must induce equivalent (pseudo)monads, i.e. FF sF\simeq F_s. (The proof that FF and F sF_s are left biadjoints landing in the 2-categories of pseudo morphisms, not just strict ones, is in Blackwell-Kelly-Power and uses properties of the pseudo morphism classifier ()(-)'.)