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
    • CommentTimeOct 5th 2011
    • (edited Oct 5th 2011)

    Does anyone know if this is a fact or fiction?

    If it is indeed a fact, as I suspect it is, do you know of a reference?

    • CommentRowNumber2.
    • CommentAuthorzskoda
    • CommentTimeOct 5th 2011

    This should not be classified under “latest changes” but under some other category in nnForum. Please reclassify.

    • CommentRowNumber3.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 5th 2011

    Alright, done. Regarding this claim, Crans says in his thesis that Street’s construction of the adjoint in the paper “the algebra of oriented simplices” is incorrect and fails to equip the globular set with the structure of an ω-category.

    Does anyone know of a correct proof?

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeOct 5th 2011

    For any cartesian cosmos VV, the category VV-CatCat is cartesian closed. The category StrωCatStr\omega Cat of strict ω-categories is coinductively defined to be (StrωCat)(Str\omega Cat)-CatCat. By coinduction, we may assume that StrωCatStr\omega Cat is cartesian closed; therefore the general fact cited previously implies that (StrωCat)(Str\omega Cat)-CatCat, i.e. StrωCatStr\omega Cat, is cartesian closed, as desired.

    Now I don’t have time to actually check the guardedness condition for corecursion, so I can’t say positively that this is a valid proof. But maybe someone else can do that, and/or unravel it into a proof that isn’t explicitly coinductive.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 5th 2011
    • (edited Oct 5th 2011)

    I was thinking of something similar: that (Strω)Cat(Str \omega) Cat can be constructed as the terminal coalgebra for the endofunctor on the 2-category of cartesian categories, which takes VV to VV-CatCat (small VV-categories). By an application of Adamek’s theorem, it may be constructed directly as the 2-limit of the sequence

    (Strn+1)Cat(Strn)CatSet1\ldots \to (Str n+1) Cat \to (Str n) Cat \to \ldots \to Set \to 1

    where each arrow is obtained by applying the endofunctor -CatCat to the arrow immediately to the right. Since cartesian closed categories are 2-monadic over cartesian categories, the limit is reflected in the 2-category of cartesian closed categories, hence (Strω)Cat(Str \omega) Cat is cartesian closed.

    (Sorry, this proof is a bit goofed-up, since the arrows don’t preserve closed structure. I’ll try to repair it later.)

    • CommentRowNumber6.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 6th 2011
    • (edited Oct 6th 2011)

    After a lot of torturous axiom-checking, I think I fixed Street’s construction.

    Basically, construct a globular set

    [A,B]n = Hom{ω-cat}(D_n x A,B).

    Then define * j i\ast^i_j, the composition of i-arrows along common j-cells by the following formula:

    given f,g in [A,B]_n, such that s^i_j(f)=t^i_j(g), where i>j0.i\gt j\geq 0.

    We define, for each and every cell aA,a \in A, the composite

    (f* j ig)(a) (f\ast^i_j g)(a)

    by defining it naturally on each source and target as well as the whole object:

    when m<j

    (s m i(f* j ig))(a)=(s m i(f))(a) (s^i_m (f\ast^i_j g))(a) = (s^i_m(f))(a)

    and

    (t m i(f* j ig))(a)=(t m i(f))(a). (t^i_m(f\ast^i_j g))(a) = (t^i_m(f))(a).

    when m=j, we set

    (s m i(f* j ig))(a)=(s m i(g))(a) (s^i_m(f\ast^i_j g))(a)=(s^i_m(g))(a)

    and

    (t m i(f* j ig))(a)=(t m i(f))(a) (t^i_m(f\ast^i_j g))(a)= (t^i_m(f))(a)

    Then for j<mi,j\lt m\leq i, we set it to:

    (s m i(f* j ig)(a))=(s m i(f))(a)* j m(s m i(g))(a)(s^i_m(f\ast^i_j g)(a))=(s^i_m(f))(a) \ast^m_j (s^i_m(g))(a)

    and similarly,

    (t m i(f* j ig))(a)=(t m i(f))(a)* j m(t m i(g))(a).(t^i_m(f\ast^i_j g))(a)=(t^i_m(f))(a) \ast^m_j (t^i_m(g))(a).

    Note that we obtain the identity maps canonically from the degeneracies (which we did not take to be part of our globular set!), so we are actually considering these identities to be additional structure.

    I believe that this construction gives the correct exponential, and I at least sketched a proof that it indeed has associative composition, strict interchange, strict identities, and functorial units.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeOct 6th 2011

    That seems like the obvious thing to do. What did Street get wrong?

    • CommentRowNumber8.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 6th 2011

    I have no idea. Crans claims that it’s wrong though.

    • CommentRowNumber9.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 6th 2011

    What is the page number where he makes the claim?

    • CommentRowNumber10.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 6th 2011

    Chapter III Section 10.2

    (this is in the file thtens.ps, that is, the part of the thesis about the Crans-Gray tensor product on str-omega-cat).

    • CommentRowNumber11.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 6th 2011

    Meanwhile, I think that it suffices to define the composite only with respect to the “full rank” functors.

    That is, given two ω-functors x 1,x 2:D i×ABx_1,x_2:D_i\times A\to B such that s j i(x 1)=t j i(x 2),s^i_j(x_1)=t^i_j(x_2), with i>j0.i\gt j \geq 0.

    Define their composite (x 1* j ix 2)(a)(x_1\ast^i_j x_2)(a) simply by the formula:

    (x 1* j ix 2)(a)=x 1(a)* j ix 2(a), (x_1\ast^i_j x_2)(a) = x_1(a) \ast^i_j x_2(a),

    where x v(a):=x v(i,a).x_v(a):=x_v(i,a). Of course, one might raise the contention that strictly speaking, this does not actually define a strict ω-functor D i×AB,D_i \times A \to B, but we note that such a functor is canonically generated from these data, by the functoriality of x_1, x_2 together with the fact that we can pull the other data out directly from the commutation conditions on B itself.

    • CommentRowNumber12.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 7th 2011
    • (edited Oct 7th 2011)

    Here was the original proof I was talking about, if someone thinks it’s good enough to add to the nLab, then I don’t mind at all. Unfortunately, it’s only half LaTeXed:

    I think that something like this should work for the internal function object. This is basically an attempt at a fix for Street’s proof and construction, together with some of the details that he glossed over. I did get a bit lazy near the end, so I hope it actually works.

    Let A,BA,B be strict ω-categories. Then let ω(A,B) be the globular set defined by the formula

    ω(A,B)_n=Hom(D_n × A,B).

    Then let f and g be any two elements of ω(A,B)_i with s^i_j(f)=t^i_j(g) for i\gt j\geq 0.

    Then we define their composite f \ast^i_j g as the map defined by the conditions:

    s^i_m(f \ast^i_j g)(a) = s^i_m f(a) = s^i_m g(a) t^i_m(f \ast^i_j g)(a) = t^i_m f(a) = t^i_m g(a) for m\lt j

    s^i_m(f \ast^i_j g)(a) = s^i_m g(a) t^i_m(f \ast^i_j g)(a) = t^i_m f(a) for m=j

    and

    s^i_m(f \ast^i_j g)(a) = s^i_m f(a) \ast^m_j s^i_m g(a) t^i_m(f \ast^i_j g)(a) = t^i_m f(a) \ast^m_j t^i_m g(a) for i\geq m\gt j

    We see immediately that for each pair (i\gt j\geq 0), this product satisfies strict associativity.

    For any triple (i\gt j\gt k\geq 0), the strict interchange law can be shown to hold, since given a quadruple x_1,x_2,x_3,x_4 of i-cells such that s^i_j(x_1)=t^i_j(x_2), s^i_k(x_2)=t^i_k(x_3), and s^i_j(x_3)=t^i_j(x_4), we see that

    s m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)s^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a) = s^i_m(x_v)(a) (for vv in {1,2,3,4}\{1,2,3,4\}) when m<km\lt k t m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=t m i(x v)(a)t^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a) = t^i_m(x_v)(a) (for vv in {1,2,3,4}\{1,2,3,4\}) when m<km\lt k

    s m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=s m i(x 3* j ix 4)(a)=s m i(x v)(a)s^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a) = s^i_m(x_3 \ast^i_j x_4)(a) =s^i_m(x_v)(a) (for v in {3,4}\{3,4\}) when m=km=k t m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=t m i(x 1* j ix 2)(a)=t m i(x v)(a)t^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a) = t^i_m(x_1 \ast^i_j x_2)(a) =t^i_m(x_v)(a) (for vv in {1,2}\{1,2\}) when m=km=k

    s m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=s m i(x 1* j ix 2)(a)* k is m i(x 3* j ix 4)(a)=s^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)= s^i_m(x_1 \ast^i_j x_2)(a)\ast^i_k s^i_m (x_3 \ast^i_j x_4)(a) = s m i(x b)(a)* k ms m i(x v)(a),s^i_m(x_b)(a) \ast^m_k s^i_m(x_v)(a), (where bb in {1,2}\{1,2\} and vv in {3,4}\{3,4\}) when k\lt m\lt j

    t m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=t m i(x 1* j ix 2)(a)* k it m i(x 3* j ix 4)(a)=t^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)= t^i_m(x_1 \ast^i_j x_2)(a)\ast^i_k t^i_m (x_3 \ast^i_j x_4)(a) = t m i(x b)(a)* k mt m i(x v)(a),t^i_m(x_b)(a) \ast^m_k t^i_m(x_v)(a), (where b in {1,2}\{1,2\} and vv in {3,4}\{3,4\} ) when k\lt m\lt j

    s m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=s m i(x 2)(a)* k ms m i(x 4)(a)s^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)=s^i_m(x_2)(a)\ast^m_k s^i_m (x_4)(a)
    t m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=t m i(x 1)(a)* k mt m i(x 3)(a)t^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)=t^i_m(x_1)(a)\ast^m_k t^i_m (x_3)(a) when m=jm=j

    s m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=(s m ix 1(a)* j ms m ix 2(a))* k m(s m ix 3(a)* j ms m ix 4(a))s^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)= (s^i_m x_1(a) \ast^m_j s^i_m x_2(a)) \ast^m_k (s^i_m x_3(a) \ast^m_j s^i_m x_4(a))
    t m i((x 1* j ix 2)* k i(x 3* j ix 4))(a)=(t m ix 1(a)* j mt m ix 2(a))* k m(t m ix 3(a)* j mt m ix 4(a))t^i_m((x_1 \ast^i_j x_2)\ast^i_k (x_3 \ast^i_j x_4)) (a)= (t^i_m x_1(a) \ast^m_j t^i_m x_2(a)) \ast^m_k (t^i_m x_3(a) \ast^m_j t^i_m x_4(a)) when im>ji\geq m\gt j

    And the interchanged version:

    s m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=s m i(x v)(a)s^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) = s^i_m(x_v)(a) (for vv in {1,2,3,4}\{1,2,3,4\}) when m<km\lt k t m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=t m i(x v)(a)t^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) = t^i_m(x_v)(a) (for vv in {1,2,3,4}\{1,2,3,4\}) when m<km\lt k

    s^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) =s^i_m(x_v)(a) (for v in {3,4}\{3,4\}) when m=km=k t^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) =t^i_m(x_v)(a) (for v in {1,2}\{1,2\}) when m=km=k

    s m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=s m i(x b)(a)* k ms m i(x v)(a),s^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) = s^i_m(x_b)(a) \ast^m_k s^i_m(x_v)(a), (where bb in {1,2}\{1,2\} and vv in {3,4}\{3,4\}) when k<m<jk\lt m\lt j t m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=t m i(x b)(a)* k mt m i(x v)(a),t^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) = t^i_m(x_b)(a) \ast^m_k t^i_m(x_v)(a), (where bb in {1,2}\{1,2\} and vv in {3,4}\{3,4\} ) when k<m<jk\lt m\lt j

    s m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=s m i(x 2)(a)* k ms m i(x 4)(a)s^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) = s^i_m(x_2)(a)\ast^m_k s^i_m (x_4)(a)
    t m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=t m i(x 1)(a)* k mt m i(x 3)(a)t^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a)= t^i_m(x_1)(a)\ast^m_k t^i_m (x_3)(a) when m=jm=j

    • CommentRowNumber13.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 7th 2011
    • (edited Oct 7th 2011)

    s m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=(s m ix 1(a)* k ms m ix 3(a))* j m(s m ix 2(a)* k ms m ix 4(a))s^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a) =(s^i_m x_1(a) \ast^m_k s^i_m x_3(a))\ast^m_j (s^i_m x_2(a) \ast ^m_k s^i_m x_4(a)) when im>ji\geq m\gt j t m i((x 1* k ix 3)* j i(x 2* k ix 4))(a)=(t m ix 1(a)* k mt m ix 3(a))* j m(t m ix 2(a)* k mt m ix 4(a))t^i_m((x_1 \ast^i_k x_3)\ast^i_j (x_2 \ast^i_k x_4)) (a)=(t^i_m x_1(a) \ast^m_k t^i_m x_3(a))\ast^m_j (t^i_m x_2(a) \ast^m_k t^i_m x_4(a)) when im>ji\geq m \gt j

    Since every case is identical beyond the case i≥m>j, it will suffice to show that this case satisfies strict interchange, but this is clear, since it inherits the strict interchange in B pointwise. This proves strict interchange.

    We also inherit degeneracy maps induced by the codegeneracies D nD n1D_n\to D_{n-1}, which give us the identity-assigning maps in ω(A,B).\omega(A,B).

    We must show that x* j i(k i j(s j i(x)))=x=(k i j(t j i(x)))* j ixx \ast^i_j (k^j_i( s^i_j (x) )) = x = (k^j_i( t^i_j (x) )) \ast^i_j x for any i-cell x.

    This obviously holds for m<jm\lt j or m>jm\gt j, so it suffices to prove it in the case m=j, but s^i_j k^j_i s^i_j(x)(a) = s^i_j (x)(a), and similarly, t^i_j k^j_i t^i_j(x)(a)=t^i_j(x)(a) since k^j_i is induced by the simultaneous retraction of the maps s^i_j and t^i_j in the category of reflexive globular sets.

    Finally, we need to show that units are functorial, that is to say, that for a pair x_1, x_2 of i-cells such that s j i(x 1)=t j i(x 2)s^i_j(x_1)=t^i_j(x_2), so we would like to show that

    k i(x 1* j ix 2)=k i(x 1)* j i+1k i(x 2)k_i(x_1 \ast^i_j x_2)=k_i(x_1) \ast^{i+1}_j k_i(x_2)

    To show this, we return to our usual cases:

    s m i+1(k i(x 1* j ix 2))(a)=s m ix 1(a)=s m ix 2(a)s^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a) = s^i_m x_1(a) = s^i_m x_2(a) t m i+1(k i(x 1* j ix 2))(a)=t m ix 1(a)=t m ix 2(a)t^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a) = t^i_m x_1(a) = t^i_m x_2(a) for m<jm\lt j

    s m i+1(k i(x 1* j ix 2))(a)=s m ix 2(a)s^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a)= s^i_m x_2(a) t m i+1(k i(x 1* j ix 2))(a)=t m ix 1(a)t^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a) = t^i_m x_1(a) for m=jm=j

    s m i+1(k i(x 1* j ix 2))(a)=s m ix 1(a)* j ms m ix 2(a)s^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a) = s^i_m x_1(a) \ast^m_j s^i_m x_2(a) t m i+1(k i(x 1* j ix 2))(a)=t m ix 1(a)* j mt m ix 2(a)t^{i+1}_m(k_i(x_1 \ast^i_j x_2))(a) = t^i_m x_1(a) \ast^m_j t^i_m x_2(a) for im>ji\geq m\gt j

    and

    k i(x 1* j ix 2)(a)k_i(x_1 \ast^i_j x_2)(a) for m=i+1m=i+1

    For the other formula, we have:

    s m i+1(k i(x 1)* j i+1k i(x 2))(a)=s m ix 1(a)=s m ix 2(a)s^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a) = s^i_m x_1(a) = s^i_m x_2(a) t m i+1(k i(x 1)* j i+1k i(x 2))(a)=t m ix 1(a)=t m ix 2(a)t^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a) = t^i_m x_1(a) = t^i_m x_2(a) for m<jm\lt j

    s m i+1(k i(x 1)* j i+1k i(x 2))(a)=s m ix 2(a)s^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a)= s^i_m x_2(a) t m i+1(k i(x 1)* j i+1k i(x 2))(a)=t m ix 1(a)t^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a) = t^i_m x_1(a) for m=jm=j

    s m i+1(k i(x 1)* j i+1k i(x 2))(a)=s m ix 1(a)* j ms m ix 2(a)s^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a) = s^i_m x_1(a) \ast^m_j s^i_m x_2(a) t m i+1(k i(x 1)* j i+1k i(x 2))(a)=t m ix 1(a)* j mt m ix 2(a)t^{i+1}_m(k_i(x_1) \ast^{i+1}_j k_i(x_2))(a) = t^i_m x_1(a) \ast^m_j t^i_m x_2(a) for im>ji\geq m\gt j

    and

    k i(x 1)(a)* j i+1k i(x 2)(a)k_i(x_1)(a) \ast^{i+1}_j k_i(x_2)(a) for m=i+1m=i+1

    Since these are identical away from the i+1 case, it suffices to prove the i+1 case, but this can be deduced pointwise in B due to the functoriality of identities there.

    Finally, we see that ω(A,B) is a strict ω-category.

    However, we must also prove that it is the cartesian internal function object:

    We will exhibit a natural bijection Hom(C × A,B)–>Hom(C,ω(A,B)).

    Given a strict ω-functor f:C × A -> B, every choice of a cell c:D_i -> C determines by precomposition a map f_c:D_i × A -> B, which belongs to ω(A,B)_i. Letting c range over all of the cells of C, we first notice that the induced map of globular sets q:C-> ω(A,B) preserves identities, since it arises from a map of reflexive globular sets. It suffices to show that this new map preserves composition of cells in C. Given two i-cells g,h of C such that s^i_j(g)=t^i_j(h) for some 0≤j<i, we see that

    q(g) ∗^i_j q(h) (p,m,a)=q(g)(p,m,a) ∗^i_j q(h)(p,m,a)=f(g,a)(p,m) ∗^i_j f(h,a)(p,m) = q(g ∗^i_j h)(p,m,a) for i≥m>j

    and

    (q(g) ∗^i_j q(h))(p,m,a) = q(g)(p,m,a) = q(g ∗^i_j h)(p,m,a) for m=j and p=0 (q(g) ∗^i_j q(h))(p,m,a) = q(h)(p,m,a) = q(g ∗^i_j h)(p,m,a) for m=j and p=1

    So this map is indeed a strict ω-functor.

    Conversely, starting with a strict ω-functor f:C -> ω(A,B), we define a new map of globular sets n:C × A-> B where n(c,a)=f(c)(p,i,a), where i is the height of the cell c.

    This map is clearly ω-functorial in a, by the functoriality of the components. Then we show that it is indeed ω-functorial in c. Let g,h be two C-cells of fixed height i such that

    s^i_j(g)=t^i_j(h) for some i>j≥0.

    Then n(g ∗^i_j h, a)=f(g ∗^i_j h)(p,i,a)=(f(g) ∗^i_j f(h))(p,i,a)= f(g)(p,i,a) ∗^i_j f(h)(p,i,a)=n(g,a) ∗^i_j n(h,a). Again, preservation of of units comes from the reflexive structure.

    It is easy to see that these two constructions are mutually inverse, and we obtain the desired natural isomorphism, proving that, indeed, ω-cat is cartesian closed.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 7th 2011

    Let’s wait to get response to your post to the categories list. I actually emailed Ross Street privately, and he acknowledges that there is something wrong with what he wrote in the paper (I’ll have to dig up my copy to see exactly what he was referring to, but from what he wrote, he was working with a single-sorted definition of ω\omega-category, which is probably not what he would do now). But there is no public doubt that strict ω\omega-categories form a cartesian closed category. I think we should see whether people offer up an elegant proof.

    • CommentRowNumber15.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 7th 2011
    • (edited Oct 7th 2011)

    Heheh, yeah, that was the proof that I sent to Cisinski when he asked me if I could find a proof or reference (since I used it in the proof of something). Since the reference was incorrect, I proved it myself…

    but as you can see it was horrible (as I noted upthread).

    Also, Street forwarded the message to me (I guess since he saw that I asked it on the categories mailing list!)

    Also, I would make the argument that Street’s proof is really just a sketch of the argument, so it doesn’t seem like any variation on it will yield a beautiful proof, since the one I just posted here contains the entirety of the work one should do.

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2011

    I think my proof in #4 is pretty elegant… (-:

    • CommentRowNumber17.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 7th 2011

    I mean, I would check it if you told me what needed to be checked.. I tried finding the guardedness criteria in the paper by Adamek, but I couldn’t find such a condition in this generality.

    Also, if it doesn’t satisfy the guardedness criterion… gj with the circular argument =D!

    • CommentRowNumber18.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 7th 2011

    Regarding comment #14, Ross wrote again to say that his earlier email had mistakes and I was to disregard it (it was written early morning Sydney time); therefore what I passed on from him is also to be disregarded. The cartesian closure is still not in doubt; he would like to look some more at TAOS and decide whether there really is a problem with what he wrote.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 7th 2011

    Sorry, Mike – I didn’t mean to imply that it wasn’t! It’s probably both correct and elegant, but I’d have to think hard about it to make sure I understood it 100%.

    • CommentRowNumber20.
    • CommentAuthorMike Shulman
    • CommentTimeOct 7th 2011

    No need to apologize, Todd; my tongue was firmly in my cheek in #16. I’m actually not entirely sure whether there is a succinct “guardedness condition” one could check that would immediately validate that proof. But I sure feel like morally, that’s why it’s true! (-:

    • CommentRowNumber21.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 7th 2011

    Harry has been strangely quiet over the past few hours: in an email exchange which included Harry, Ross proposed a nice proof of cartesian closure, and then Harry had a nice amendment which fits well with nPOV’s which have been developed in the Lab. Harry, why don’t you do the honors of writing this up? (I mean, I could write it up too if you like.)

    • CommentRowNumber22.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 7th 2011
    • (edited Oct 8th 2011)

    Alright, we can sharpen the reflection theorem as follows:

    Suppose L:DC:RL:D\rightleftarrows C:R is an adjunction with fully faithful right adjoint.

    Lemma:

    For an object z in X, TFAE:

    a.) z belongs to the image of R b.) The map Hom(RL z, x) -> Hom(z,x) induced by the unit transformation is injective for every object x of X c.) The unit transformation at z is a split mono d.) The unit transformation at z is an isomorphism e.) The map Hom(RL z, x) -> Hom(z,x) induced by the unit transformation is bijective for every object x of X

    Proof: Exo.

    ======================

    Reflection Theorem [Day]:

    Suppose that X is symmetric monoidal closed.

    Then TFAE:

    1.) The natural transformation η:[x,R(a)]->RL[x,R(a)] is a natural isomorphism 2.) The natural transformation [η, 1]:[RL(x),R(a)] -> [x, R(a)] is a natural isomorphism 3.) The natural transformation L(η ⊗ 1): L(X ⊗ Y) -> L(RLX ⊗ Y) is a natural isomorphism 4.) The natural transformation L(η ⊗ η): L(X ⊗ Y) -> L(RLX ⊗ RLY)

    If in addition, ⊗ = × is the cartesian product, then we may also add to the list a further number,

    5.) The natural transformation (Lπ_1,Lπ_2): L(X × Y) -> L(X) × L(Y) is a natural isomorphism.

    Proof: Exo. (The statements are harder to come up with than the proofs, which are pretty straightforward)

    ========================

    Totally Untrue Theorem

    Let :EC\ell:E\to C be a dense functor such that R:EDR\circ \ell: E\to D is also a dense functor. Then RA BRA^B belongs to the image of RR for any object BB in DD and any object AA in CC.

    Proof: Suppose AA belongs to CC, BB belongs to DD, . Letting XX vary, we see that:

    Hom(RLX,RA B)=Hom(R(L(colim(R(K i)),RA B)=Hom(R(colim(L(R(K i))),RA B)Hom(RLX, RA^B)= Hom(R(L(colim(R(K_i)), RA^B) = Hom(R(colim(L(R(K_i))),RA^B)

    which is

    Hom(RcolimK i,RA B)=Hom(BxRcolimK i,RA)=Hom(B,RA)×Hom(RcolimK i,RA)Hom(R colim K_i,RA^B) = Hom(B x R colim K_i,RA) = Hom(B,RA) \times Hom(R colim K_i,RA)

    which is

    Hom(B,RA)×Hom(colim iK i,A)=Hom(B,RA)×Homlim i(K i,A))=Hom(B,RA)×lim iHom(RK i,RA),Hom(B,RA) \times Hom(colim_i K_i, A) = Hom(B,RA) \times Hom lim_i(K_i,A))=Hom(B,RA) \times lim_i Hom(RK_i,RA),

    which is exactly

    Hom(B,RA)×Hom(colim iRK i,RA)=Hom(B×colim iRK i,RA)=Hom(colim iRK i,RA B)Hom(B,RA)\times Hom(colim_i RK_i,RA) = Hom(B\times colim_i RK_i,RA)= Hom(colim_i RK_i, RA^B)

    which is finally Hom(X,RA B)Hom(X,RA^B).

    In particular, in the case where \ell is a dense functor ACA\to C with AA small, we obtain a functor R:CA^R:C\to \widehat{A} satisfying the correct properties.

    Then the case for strict ω\omega-categories can be dealt with by choosing E=ΘE=\Theta.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 7th 2011
    • (edited Oct 7th 2011)

    This isn’t right, I’m afraid: the places where you’ve used Hom(A×B,C)=Hom(A,C)×Hom(B,C)Hom(A \times B, C) = Hom(A, C) \times Hom(B, C).

    Actually, I’d like to hear back from Ross whether there is in the literature a proof that the reflection L:Set Θ opωL: Set^{\Theta^{op}} \to \omega-CatCat preserves products, which doesn’t already assume the fact that ω\omega-CatCat is cartesian closed.

    • CommentRowNumber24.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 8th 2011
    • (edited Oct 8th 2011)

    Oh yeah, that’s idiotic =X.

    Chalk it up to two days without sleep, I guess.

    Anyway, I’m pretty sure that the long and horrible proof is essentially right.

    Meanwhile, I can’t imagine that there is some hugely obvious proof of this fact using the reflection theorem now that I think about it, since if we just treat omega-cat as a black box, we don’t know more than the hypotheses of the reflection theorem.

    I’m pretty sure that if there is a general proof, you’re going to have to either use the description of omega-cat as the category of algebras for the terminal globular operad, or some other kind of thing along those lines.

    Question: How would you show that Cat is cartesian-closed if you were going to try to do it without an explicit construction of the internal function object? If you have an easy answer to that, then I think that the case for omega-cat will be analogous.

    Every proof that I know for nn-cat with nn-finite is just using induction on the base case, but it’s all based on the explicit construction of the internal function object for 11-cat.

    • CommentRowNumber25.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 8th 2011

    Well, perhaps you should start the induction with 0-Cat, not 1-Cat, but anyway it’s a good question. I do think there’s a shot that a corecursive argument could work after all. But we should still wait to hear if the Australians have more to say at the moment, not to mention somebody here.

    • CommentRowNumber26.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 8th 2011
    • (edited Oct 8th 2011)

    I mean, whether we use Simpson’s Δ 0 ω\Delta^\omega_0 or Joyal’s Θ\Theta, the thing that Street said would work will rely either on Day giving a recognition principle for closure under exponentiation. If there is no really useful one, I would imagine the the only ways to show that this is cartesian-closed are:

    1.) Direct proof
    2.) Proof using some kind of operad (more sophisticated version of 1.) 3.) Coinduction

    I actually sat down and verified Street’s construction again (this time more carefully), and it does indeed work, at least using a version rephrased for globular sets.

    By the way, I just noticed something weird:

    The restriction that Crans is making on the page strict omega-category is the restriction to those ω\omega-categories with no “cells” of infinite dimension, that is, what you and I would call “nondegenerate cells”. It is extremely to important to remember that in the original terminology (which I can now pontificate on!) using the definition as a set with operations, an “nn-cell” is defined to be an element such that nn is the smallest ordinal containing all ordinals jj for which the element’s jj-source and jj-target are equal. Indeed, Batanin’s ω\omega-categories are actually what Verity would call ω +\omega^+-categories.

    In fact, the difference is that Crans is looking at the direct limit of the inclusions 0Cat1Cat2Cat0-Cat\to 1-Cat \to 2-Cat\to \dots, while Batanin, Street, Verity, and the rest of us are looking at the limit 2cat1catSet\dots \to 2-cat\to 1-cat \to Set. The page should probably be changed to make that clear, since, in particular, the assumption of Crans and Steiner yields a category that is neither complete nor cocomplete.

    Apparently someone was confused and thought that “cell” of xx here is meant to mean an element of the category of elements 𝔾x,\mathbb{G}\downarrow x, but it is actually meant as “a nondegenerate element” (since these are the elements of the associated graded set).

    • CommentRowNumber27.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 8th 2011
    • (edited Oct 8th 2011)

    Hey Todd,

    What if you did the original argument in the category where the objects are cartesian/cartesian-closed and the maps are the right adjoint functors whose left adjoints preserve the cartesian closed structure?

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeOct 8th 2011

    In fact, the difference is that Crans is looking at the direct limit of the inclusions 0Cat1Cat2Cat0-Cat\to 1-Cat \to 2-Cat\to \dots, while Batanin, Street, Verity, and the rest of us are looking at the limit 2cat1catSet\dots \to 2-cat\to 1-cat \to Set

    I disagree. Crans’ restriction just means there are no “ω\omega-dimensional” cells, and that is the case for objects of the (inverse) limit—there can still be nondegenerate cells of arbitrarily large finite dimension. Objects of the colimit, on the other hand, have a finite bound on the dimension of all their (nondegenerate) cells; nobody would call those ω\omega-categories (or, rather, nobody would restrict “ω\omega-category” to refer only to that case).

    • CommentRowNumber29.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 8th 2011
    • (edited Oct 8th 2011)

    Edit: Ahh.. I see where the problem is..

    In an ω-category, the ω^+-cells are uniquely determined, whereas in an ω^+-category, you could have two different ω-cells between choices of boundary.

    Then is an ω^+-category just an ω-category with relations?

    I wonder if there’s anything interesting all the way up there, like defining categories of higher order type, etc.

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 8th 2011

    Glad you spoke up, Mike – I was preparing a much longer (or more verbose) comment which amounts to what you said in #28, essentially.

    At first pass, it would be simpler to talk just about ω +\omega^+-globular sets, which are presheaves over the category obtained by adjoining an object ω\omega to 𝔾\mathbb{G}, with maps i 0,i 1:nωi_0, i_1: n \to \omega for each nn, satisfying appropriate equations. The ω\omega would represent the “infinite-dimensional globe”, and the structures Street discusses in The Algebra of Oriented Simplexes could be construed as algebraic over ω +\omega^+-globular sets. But I don’t know that there is much interest in ω +\omega^+-categories these days – I’d be tempted to treat them for now as historical curiosities.

    • CommentRowNumber31.
    • CommentAuthorMike Shulman
    • CommentTimeOct 8th 2011

    In an ω-category, the ω^+-cells are uniquely determined

    I would argue that an ω-category doesn’t actually have ω^+-cells or ω-cells.

    I’d be tempted to treat them for now as historical curiosities.

    Ditto.

    • CommentRowNumber32.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 8th 2011

    I would agree with Mike #31. We don’t talk about simplicial sets with ω\omega-simplices. (generally)

    • CommentRowNumber33.
    • CommentAuthorHarry Gindi
    • CommentTimeOct 8th 2011

    Ugh, stop commenting on a stupid thing that I wrote.. I keep getting excited thinking that someone found a good answer.