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 10 of 10
Somebody asks by email:
double categories are cartesian closed and it seems pretty reasonable that n-fold categories are cartesian closed - would you know of a reference for this? It would be good if there was some result that said categories internal to a suitable category E were cartesian closed.
Does anyone easily have a pointer?
Does anyone easily have a pointer?
I don’t, but it doesn’t seem unreasonable to write out a proof for this type of thing. Without having written anything down, I’d guess that if $E$ is finitely complete and cartesian closed, then $Cat(E)$ is also finitely complete and cartesian closed. Then $n$-fold categories would be cartesian closed by induction.
Well, I may as well have a go at writing down a sketch of a proof of the assertion from my previous comment, that if $E$ is finitely complete and cartesian closed, then $Cat(E)$ is also finitely complete and cartesian closed.
First, let $E$ be finitely complete. Then the category of directed graphs $E^{\bullet \stackrel{\to}{\to} \bullet}$ is also finitely complete, and since $Cat(E)$ is monadic over $E^{\bullet \stackrel{\to}{\to} \bullet}$, it follows that $Cat(E)$ is also finitely complete.
Now let $E$ be finitely complete and cartesian closed. Then $E^C$ is cartesian closed for any finite category $C$ (by adapting Mike’s proof, using only finite ends). This applies in particular to the case where $C$ is a suitable truncation of the simplex category, say where $C$ is opposite to the category of nonempty ordinals up to cardinality 3. Now $Cat(E)$ is a full subcategory of $E^C$, and it should be simple to see directly that it is an exponential ideal of $E^C$; in particular, it’s cartesian closed. (When I say “easy to see directly”, I mean that we don’t need to consider colimits in $Cat(E)$ or its being a reflective subcategory of $E^C$ – just use the formula for exponentials in $E^C$ to suggest the correct construction of exponentials in $Cat(E)$.)
Does this seem reasonable?
Thanks, Todd! I have alerted my correspondent of your messages, thanks.
Maybe some of this could be copied to the entry n-fold category.
The closest thing I can think of to a reference for this is the remark following B2.3.15 in the Elephant. But surely someone, somewhere, must have written it down before…
Ehresmann’s original proof, which I alluded to on the page internal category, is really quite awful. It’s working with generalised sketches, and for some reason either this precludes using the simple machinery from Todd’s #3, or Ehresmann just wasn’t in that frame of mind.
Can you add a pointer, or a page number, or something, to identify the alluded-to proof in Ehresmann’s work‘?
Can do.
I got around to writing out a proof at internal category. Please feel free to check for accuracy.
I see that someone already had written there
If the ambient category $\mathcal{C}$ is a cartesian closed category, then the category $Cat(\mathcal{C})$ of categories internal to $\mathcal{C}$ is also cartesian closed.
I have added in a finite completeness assumption (which is a bit of a no-brainer; at a minimum, existence of pullbacks should be assumed).
Ok, edited to include the references alluded to in #6.
1 to 10 of 10