Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
1 to 33 of 33
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?
This should not be classified under “latest changes” but under some other category in nForum. Please reclassify.
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?
For any cartesian cosmos V, the category V-Cat is cartesian closed. The category StrωCat of strict ω-categories is coinductively defined to be (StrωCat)-Cat. By coinduction, we may assume that StrωCat is cartesian closed; therefore the general fact cited previously implies that (StrωCat)-Cat, i.e. Strω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.
I was thinking of something similar: that (Strω)Cat can be constructed as the terminal coalgebra for the endofunctor on the 2-category of cartesian categories, which takes V to V-Cat (small V-categories). By an application of Adamek’s theorem, it may be constructed directly as the 2-limit of the sequence
…→(Strn+1)Cat→(Strn)Cat→…→Set→1where each arrow is obtained by applying the endofunctor -Cat 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 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.)
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 *ij, 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>j≥0.
We define, for each and every cell a∈A, the composite
(f*ijg)(a)by defining it naturally on each source and target as well as the whole object:
when m<j
(sim(f*ijg))(a)=(sim(f))(a)and
(tim(f*ijg))(a)=(tim(f))(a).when m=j, we set
(sim(f*ijg))(a)=(sim(g))(a)and
(tim(f*ijg))(a)=(tim(f))(a)Then for j<m≤i, we set it to:
(sim(f*ijg)(a))=(sim(f))(a)*mj(sim(g))(a)and similarly,
(tim(f*ijg))(a)=(tim(f))(a)*mj(tim(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.
That seems like the obvious thing to do. What did Street get wrong?
I have no idea. Crans claims that it’s wrong though.
What is the page number where he makes the claim?
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).
Meanwhile, I think that it suffices to define the composite only with respect to the “full rank” functors.
That is, given two ω-functors x1,x2:Di×A→B such that sij(x1)=tij(x2), with i>j≥0.
Define their composite (x1*ijx2)(a) simply by the formula:
(x1*ijx2)(a)=x1(a)*ijx2(a),where xv(a):=xv(i,a). Of course, one might raise the contention that strictly speaking, this does not actually define a strict ω-functor Di×A→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.
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,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
sim((x1*ijx2)*ik(x3*ijx4))(a) = s^i_m(x_v)(a) (for v in {1,2,3,4}) when m<k tim((x1*ijx2)*ik(x3*ijx4))(a)=tim(xv)(a) (for v in {1,2,3,4}) when m<k
sim((x1*ijx2)*ik(x3*ijx4))(a)=sim(x3*ijx4)(a)=sim(xv)(a) (for v in {3,4}) when m=k tim((x1*ijx2)*ik(x3*ijx4))(a)=tim(x1*ijx2)(a)=tim(xv)(a) (for v in {1,2}) when m=k
sim((x1*ijx2)*ik(x3*ijx4))(a)=sim(x1*ijx2)(a)*iksim(x3*ijx4)(a)= sim(xb)(a)*mksim(xv)(a), (where b in {1,2} and v in {3,4}) when k\lt m\lt j
tim((x1*ijx2)*ik(x3*ijx4))(a)=tim(x1*ijx2)(a)*iktim(x3*ijx4)(a)= tim(xb)(a)*mktim(xv)(a), (where b in {1,2} and v in {3,4} ) when k\lt m\lt j
sim((x1*ijx2)*ik(x3*ijx4))(a)=sim(x2)(a)*mksim(x4)(a)
tim((x1*ijx2)*ik(x3*ijx4))(a)=tim(x1)(a)*mktim(x3)(a) when m=j
sim((x1*ijx2)*ik(x3*ijx4))(a)=(simx1(a)*mjsimx2(a))*mk(simx3(a)*mjsimx4(a))
tim((x1*ijx2)*ik(x3*ijx4))(a)=(timx1(a)*mjtimx2(a))*mk(timx3(a)*mjtimx4(a)) when i≥m>j
And the interchanged version:
sim((x1*ikx3)*ij(x2*ikx4))(a)=sim(xv)(a) (for v in {1,2,3,4}) when m<k tim((x1*ikx3)*ij(x2*ikx4))(a)=tim(xv)(a) (for v in {1,2,3,4}) when m<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}) when m=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}) when m=k
sim((x1*ikx3)*ij(x2*ikx4))(a)=sim(xb)(a)*mksim(xv)(a), (where b in {1,2} and v in {3,4}) when k<m<j tim((x1*ikx3)*ij(x2*ikx4))(a)=tim(xb)(a)*mktim(xv)(a), (where b in {1,2} and v in {3,4} ) when k<m<j
sim((x1*ikx3)*ij(x2*ikx4))(a)=sim(x2)(a)*mksim(x4)(a)
tim((x1*ikx3)*ij(x2*ikx4))(a)=tim(x1)(a)*mktim(x3)(a) when m=j
sim((x1*ikx3)*ij(x2*ikx4))(a)=(simx1(a)*mksimx3(a))*mj(simx2(a)*mksimx4(a)) when i≥m>j tim((x1*ikx3)*ij(x2*ikx4))(a)=(timx1(a)*mktimx3(a))*mj(timx2(a)*mktimx4(a)) when i≥m>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 Dn→Dn−1, which give us the identity-assigning maps in ω(A,B).
We must show that x*ij(kji(sij(x)))=x=(kji(tij(x)))*ijx for any i-cell x.
This obviously holds for m<j or m>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 sij(x1)=tij(x2), so we would like to show that
ki(x1*ijx2)=ki(x1)*i+1jki(x2)
To show this, we return to our usual cases:
si+1m(ki(x1*ijx2))(a)=simx1(a)=simx2(a) ti+1m(ki(x1*ijx2))(a)=timx1(a)=timx2(a) for m<j
si+1m(ki(x1*ijx2))(a)=simx2(a) ti+1m(ki(x1*ijx2))(a)=timx1(a) for m=j
si+1m(ki(x1*ijx2))(a)=simx1(a)*mjsimx2(a) ti+1m(ki(x1*ijx2))(a)=timx1(a)*mjtimx2(a) for i≥m>j
and
ki(x1*ijx2)(a) for m=i+1
For the other formula, we have:
si+1m(ki(x1)*i+1jki(x2))(a)=simx1(a)=simx2(a) ti+1m(ki(x1)*i+1jki(x2))(a)=timx1(a)=timx2(a) for m<j
si+1m(ki(x1)*i+1jki(x2))(a)=simx2(a) ti+1m(ki(x1)*i+1jki(x2))(a)=timx1(a) for m=j
si+1m(ki(x1)*i+1jki(x2))(a)=simx1(a)*mjsimx2(a) ti+1m(ki(x1)*i+1jki(x2))(a)=timx1(a)*mjtimx2(a) for i≥m>j
and
ki(x1)(a)*i+1jki(x2)(a) for m=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.
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 ω-category, which is probably not what he would do now). But there is no public doubt that strict ω-categories form a cartesian closed category. I think we should see whether people offer up an elegant proof.
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.
I think my proof in #4 is pretty elegant… (-:
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!
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.
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%.
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! (-:
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.)
Alright, we can sharpen the reflection theorem as follows:
Suppose L:D⇄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 ℓ:E→C be a dense functor such that R∘ℓ:E→D is also a dense functor. Then RAB belongs to the image of R for any object B in D and any object A in C.
Proof: Suppose A belongs to C, B belongs to D, . Letting X vary, we see that:
Hom(RLX,RAB)=Hom(R(L(colim(R(Ki)),RAB)=Hom(R(colim(L(R(Ki))),RAB)which is
Hom(RcolimKi,RAB)=Hom(BxRcolimKi,RA)=Hom(B,RA)×Hom(RcolimKi,RA)which is
Hom(B,RA)×Hom(colimiKi,A)=Hom(B,RA)×Homlimi(Ki,A))=Hom(B,RA)×limiHom(RKi,RA),which is exactly
Hom(B,RA)×Hom(colimiRKi,RA)=Hom(B×colimiRKi,RA)=Hom(colimiRKi,RAB)which is finally Hom(X,RAB).
In particular, in the case where ℓ is a dense functor A→C with A small, we obtain a functor R:C→ˆA satisfying the correct properties.
Then the case for strict ω-categories can be dealt with by choosing E=Θ.
This isn’t right, I’m afraid: the places where you’ve used Hom(A×B,C)=Hom(A,C)×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→ω-Cat preserves products, which doesn’t already assume the fact that ω-Cat is cartesian closed.
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 n-cat with n-finite is just using induction on the base case, but it’s all based on the explicit construction of the internal function object for 1-cat.
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.
I mean, whether we use Simpson’s Δω0 or Joyal’s Θ, 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 ω-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 “n-cell” is defined to be an element such that n is the smallest ordinal containing all ordinals j for which the element’s j-source and j-target are equal. Indeed, Batanin’s ω-categories are actually what Verity would call ω+-categories.
In fact, the difference is that Crans is looking at the direct limit of the inclusions 0−Cat→1−Cat→2−Cat→…, while Batanin, Street, Verity, and the rest of us are looking at the limit …→2−cat→1−cat→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 x here is meant to mean an element of the category of elements 𝔾↓x, but it is actually meant as “a nondegenerate element” (since these are the elements of the associated graded set).
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?
In fact, the difference is that Crans is looking at the direct limit of the inclusions 0−Cat→1−Cat→2−Cat→…, while Batanin, Street, Verity, and the rest of us are looking at the limit …→2−cat→1−cat→Set
I disagree. Crans’ restriction just means there are no “ω-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 ω-categories (or, rather, nobody would restrict “ω-category” to refer only to that case).
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.
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 ω+-globular sets, which are presheaves over the category obtained by adjoining an object ω to 𝔾, with maps i0,i1:n→ω for each n, satisfying appropriate equations. The ω would represent the “infinite-dimensional globe”, and the structures Street discusses in The Algebra of Oriented Simplexes could be construed as algebraic over ω+-globular sets. But I don’t know that there is much interest in ω+-categories these days – I’d be tempted to treat them for now as historical curiosities.
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.
I would agree with Mike #31. We don’t talk about simplicial sets with ω-simplices. (generally)
Ugh, stop commenting on a stupid thing that I wrote.. I keep getting excited thinking that someone found a good answer.
1 to 33 of 33