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.
at internal hom the following discussion was sitting. I hereby move it from there to here
Here's some discussion on notation:
Ronnie: I have found it convenient in a number of categories to use the convention that if say the set of morphisms is then the internal hom when it exists is . In particular we have the exponential law for categories
Then one can get versions such as if are objects over .
Of course to use this the name of the category needs more than one letter. Also it obviates the use of those fonts which do not have upper and lower case, so I have tended to use mathsf, which does not work here!
How do people like this? Of course, panaceas do not exist.
Toby: I see, that fits with using as the -category of categories but as the category of categories. (But I'm not sure if that's a good thing, since I never liked that convention much.) I only used ’Hom’ for the external hom here since Urs had already used ’hom’ for the internal hom.
Most of the time, I would actually use the same symbol for both, just as I use the same symbol for both a group and its underlying set. Every closed category is a concrete category (represented by ), and the underlying set of the internal hom is the external hom. So I would distinguish them only when looking at the theorems that relate them, much as I would bother parenthesising an expression like only when stating the associative law.
Ronnie: In the case of crossed complexes it would be possible to use for the internal hom and then is the actual set of morphisms, with being the (left 1-) homotopies.
But if is a groupoid does mean is an arrow or an object? The group example is special because a group has only one object.
If is a group I like to distinguish between the group of automorphisms, and the crossed module , some people call it the actor, which is given by the inner automorphism map , and this seems convenient. Similarly if is a groupoid we have a group of automorphisms but also a group groupoid, and so crossed module, , which can be described as the maximal subgroup object of the monoid object in the cartesian closed closed category of groupoids.
Toby: ’But if is a groupoid does mean is an arrow or an object?’: I would take it to mean that is an object, but I also use for the pointed connected groupoid associated to a group ; I know that groupoid theorists descended from Brandt wouldn't like that. I would use , where is the arrow category (also a groupoid now) of , if you want to be an arrow. (Actually I don't like to use at all to introduce a variable, preferring the type theorist's colon. Then introduces as an object of the known groupoid , introduces as a morphism between the known objects and , and introduces all three variables. This generalises consistently to higher morphisms, and of course it invites a new notation for a hom-set: .)
continued in next comment…
…continuation from previous comment
Ronnie: I would use, and have used, for a (the) classifying space of the group, usually the realisation of the simplicial nerve of the group, and would often identify a group with its corresponding one-object groupoid. If is a crossed complex or multiple groupoid, I would want to be a space, and to be some combinatorial object, such as simplicial or cubical set, or multi versions of these. Actually, has in this case the structure of T-complex, so is also a form of higher category.
Of course Brandt initiated the groupoid idea, coming from the composition of quaternary quadratic forms, generalising ideas of Gauss, but other later traditions come via Reidemeister in algebraic topology and much wider from Charles Ehresmann, for fibre bundles, Lie groupoids, foliations, and other geometric applications, and these need to be considered for notational decisions.
I guess the needs of geometry, algebra, analysis, logic and computer science, and even physics, will never be completely reconciled.
Toby: We ran into the conflict with before and somewhat tentatively decided to use for the groupoid and for the space (and maybe for the nerve). You can read some of that discussion at category algebra (where it is as out of place as it is here), including reasons for distinguishing from .
Probably it was a mistake to use the letter again. I think that the idea was to identify all versions of a homotopy 1-type (groupoid, simplicial set satisfying certain conditions, nice topological space with no nontrivial higher homotopy groups, etc), but that is not very helpful to other fields. I would be happy to use a different letter but would want to use something.
By ’groupoid theorists descended from Brandt’ I really meant all those who see groupoids as generalised groups (a single set with a partial binary operation satisfying various conditions) rather than those who see them as special kinds of categories (a set of objects, a set —or even doubly-indexed family of sets— of isomorphisms, and so on; while it is perfectly possible to view general categories in the Brandt-like way, that seems pretty rare).
Mike Shulman: I prefer to use for the (1- or 2-)category of small categories and for the (1- or 2-)category of large categories, with 1-categories in bold typeface and 2-categories in script typeface. And I always write for the set of morphisms from to , leaving for the internal hom if you like. Another nice option is to underline when writing for the internal hom, although that doesn’t appear to work here (although the itex2MML commands summary claims that \underline
is accepted).
By the way, it’s not true that every closed category is concrete: homming out of need not be faithful. Take simplicial sets, for instance, or even .
end of forwarded discussion
Thank you for nice formatted archiving version. I have left a link at the internal hom to this discussion (I think we should nearly always do that when archiving). We need also a canonical reference for this entry (maybe Kelly ??).
have expanded at internal hom the first two subsections of the Examples-section a little: In a sheaf topos and In smooth spaces.
afterwards I realized that Idea-section at internal hom was not in good shape. I have now spent some minutes on trying to improve it.
I notice this generally, and it is a bit of a pity: of all entries on the Lab specifically those related to basic category are often poor… and not touched for a long while. This is because we created many of them right when the Lab was very young, and didn’t yet have a more “professional” perspective on writing entries. But it’s still a pity. I wish somebody would give a course on basic category theory and use the occasion to boost the relevant Lab entries to at least the level of decent course material.
I kept adding some things to internal hom. It's not done yet, but I need to quit now.
Todd pointed out at the Cafe that two of the examples at internal hom used different notation from the rest of the page (and, arguably, poorer notation as well), so I changed them to make the page consistent. I also rewrote the section on internal-homs of super vector spaces to make sense in terms of the definition of a graded vector space as an indexed family of vector spaces, which is the category-theoretically sensible one.
internal hom contained a (trivial) mistake in the sentence
Formally this says that the functor of taking the cartesian product with the set has a right adjoint given by the construction .
I mean, it is obvious from this sentence, at least when taken out of context like above, that the is wrong and should be .
It becomes sort-of-less-wrong in context, i.e. in its former version,
One way to make this precise is to mimic the basic property of a function set of functions between two sets and : that is uniquely characterized by the fact that for any other set the functions are in natural bijection with the functions out of the cartesian product of with . Formally this says that the functor of taking the cartesian product with the set has a right adjoint given by the construction .
in view of the “formal variable” , which is presumably the cause for the slight inaccuracy. I therefore simply took out the repeating-what-the-notation-already-says phrase “taking the cartesian product […]” from the statement of the adjunction, but somehow conserved it by giving it a place inside a verbal repetition of the adjunction, in the spirit of the known functors-are-verbs-metaphor.
While I was at it, I made various stylistic changes to the paragraph, all of which I think are improvements. I will not run through all of them here. I found fault with “the basic property” and “Formally this says” (I mean, wasn’t the sentence before rather formal already; I changed it to a simple “That is:”)
I gave the entry a section Basic properties with statement and proof of some of the basic properties:
for each is sufficient to have bifunctor ;
hom adjunction internalizes as ;
preserves limits in second argument and sends colimits in first to limits
I also did some editorial edits:
Made explicit that the def as stated is for symmetric monoidal categories.
Moved the definition of evaluation map and composition map from “Properties” to “Definition”.
Thanks for catching this. Fixed now.
added a small paragraph on and pointer to stable splitting of mapping spaces.
just a reminder to myself and anyone who cares:
currently mapping space is still just redirecting to internal hom. Clearly this is not sustainable. Ought to be improved on…
This is not doubting you, but what aspects of “mapping space” spill outside this redirect?
The topological mapping spaces should have a dedicated article of their own, not inside the much broader entry on internal homs.
Possibly I could be of assistance, if I knew what you’d want included.
I am sorry that I apparently consistently come across as being mysterious, I wish I knew what is causing it. All I am saying is that eventually the material on topological mapping spaces should be split off from the entry on internal homs to a stand-alone entry. It’s a comment on formatting/entry layout. It seems completely obvious to me, which may be the cause of me not communicating it properly.
What? The only other meaning I can think of is “taking things out of a box” but that doesn’t even make any sense as an interpretation here (“the set of all functions” is not “inside” of in any sense). And “function out of ” is a standard mathematical usage for “function with domain ”, more standard in my idiolect than “function on ”.
I think “function on” is familiar to me, but mostly when it’s something like real- or complex-valued functions. It would be nice to know what “contradictory” meaning linkhyrule5 has in mind here. I think “functions out of ” or “functions from ” both work for me (both with the implication of arrows pointing away from, not toward, ).
Given a monoidal category , the usual “provisional” definition of ‘right internal hom of ’ is a (unique in the appropriate sense, if it exists) collection indexed over objects of of functors along with adjunctions .
While this agrees with the ultimately desired bifunctorial notion on objects and on morphisms in the second argument, it is not a priori functorial in the first. In particular, the definition of ‘right internal hom of ’ that we ultimately desire is a bifunctor that satisfies
naturally in all three arguments.
Accordingly, Proposition 3.1 establishes that a right internal hom in the former provisional sense can always be (uniquely, in the appropriate sense) upgraded to a right internal hom in the latter bifunctorial sense.
But Yoneda’s lemma implies that the weaker condition that for all pairs of objects , of , the functor is representable suffices to imply the existence of the aformentioned bifunctor.
I guess my question is whether it would it be of any utility to rewrite Definition 2.1 so that ‘a right internal hom of ’ is defined to be a bifunctor equipped with a natural (in , , and ) isomorphism
and then to prove as propositions
That there is a unique natural transformation from any one such right internal hom to any other such internal hom that is compatible with its Currying isomorphism
Thus that a right internal Hom of is unique if it exists)
That the existence of such a right internal hom is equivalent to the practically weaker condition that for all pairs of objects of , the functor is representable.
In particular, we would be eliding adjunction from the discussion in favor of applying Yoneda’s lemma directly.
I suspect the motivation for that framing is that it’s often interesting to talk about exponentiable objects even when not every object is exponentiable, which leads to one talking about the situation where every object is exponentiable.
I would actually suggest rewriting this definition in the opposite way: define the internal hom pointwise – i.e. for each pair , define an internal hom to be a representing object* for if one exists – and then invoke yoneda to prove that it’s uniquely functoral on the full subcategory where they exist for any global choice of internal homs for each pair. That way it’s more general; you can talk about internal homs even when they don’t exist for every pair. I suppose taking the functor as part of the definition sweeps the “once you make a choice” under the rug, for better or for worse.
*: For the sake of precision, by “representing object” I mean to include both the object and the natural isomorphism is part of the data.
Re. #24. Just to point out that the structure you are describing is a two-variable adjunction. The internal hom can be phrased in both ways, but I agree with Hurkyl that in practice one is often interested in the setting in which the hom exists only for some objects.
1 to 28 of 28