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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2011
    • (edited Sep 25th 2012)

    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 hom(x,y)hom(x,y) then the internal hom when it exists is HOM(x,y)HOM(x,y). In particular we have the exponential law for categories

    Cat(x×y,z)Cat(x,CAT(y,z)).Cat(x \times y,z) \cong Cat(x,CAT(y,z)).

    Then one can get versions such as CAT a(y,z)CAT_a(y,z) if y,zy,z are objects over aa.

    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 CAT\CAT as the 22-category of categories but Cat\Cat 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 II), 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 abca b c only when stating the associative law.

    Ronnie: In the case of crossed complexes it would be possible to use Crs *(B,C)Crs_*(B,C) for the internal hom and then Crs 0(B,C)Crs_0(B,C) is the actual set of morphisms, with Crs 1(B,C)Crs_1(B,C) being the (left 1-) homotopies.

    But if GG is a groupoid does xGx \in G mean xx is an arrow or an object? The group example is special because a group has only one object.

    If GG is a group I like to distinguish between the group Aut(G)Aut(G) of automorphisms, and the crossed module AUT(G)AUT(G), some people call it the actor, which is given by the inner automorphism map GAut(G)G \to Aut(G), and this seems convenient. Similarly if GG is a groupoid we have a group Aut(G)Aut(G) of automorphisms but also a group groupoid, and so crossed module, AUT(G)AUT(G), which can be described as the maximal subgroup object of the monoid object GPD(G,G)GPD(G,G) in the cartesian closed closed category of groupoids.

    Toby: ’But if GG is a groupoid does xGx \in G mean xx is an arrow or an object?’: I would take it to mean that xx is an object, but I also use BG\mathbf{B}G for the pointed connected groupoid associated to a group GG; I know that groupoid theorists descended from Brandt wouldn't like that. I would use xArr(G)x \in \Arr(G), where Arr(G)\Arr(G) is the arrow category (also a groupoid now) of GG, if you want xx to be an arrow. (Actually I don't like to use \in at all to introduce a variable, preferring the type theorist's colon. Then x:Gx: G introduces xx as an object of the known groupoid GG, f:xyf: x \to y introduces ff as a morphism between the known objects xx and yy, and f:xy:Gf: x \to y: G introduces all three variables. This generalises consistently to higher morphisms, and of course it invites a new notation for a hom-set: xyx \to y.)

    continued in next comment…

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeDec 7th 2011

    …continuation from previous comment

    Ronnie: I would use, and have used, BG\mathbf{B}G 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 GG is a crossed complex or multiple groupoid, I would want BG\mathbf{B}G to be a space, and Nerv(G)Nerv(G) to be some combinatorial object, such as simplicial or cubical set, or multi versions of these. Actually, Nerv(G)Nerv(G) 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 BB before and somewhat tentatively decided to use BG\mathbf{B}G for the groupoid and G\mathcal{B}G for the space (and maybe 𝒩G\mathcal{N}G 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 GG from BG\mathbf{B}G.

    Probably it was a mistake to use the letter BB 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 CatCat for the (1- or 2-)category of small categories and CATCAT 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 C(x,y)C(x,y) for the set of morphisms from xx to yy, leaving hom(x,y)hom(x,y) for the internal hom if you like. Another nice option is to underline CC when writing C(x,y)C(x,y) 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 II need not be faithful. Take simplicial sets, for instance, or even CatCat.

    end of forwarded discussion

    • CommentRowNumber3.
    • CommentAuthorzskoda
    • CommentTimeDec 8th 2011
    • (edited Dec 8th 2011)

    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 ??).

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeSep 25th 2012

    have expanded at internal hom the first two subsections of the Examples-section a little: In a sheaf topos and In smooth spaces.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeSep 25th 2012
    • (edited Sep 25th 2012)

    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 nnLab 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 nnLab 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 nnLab entries to at least the level of decent course material.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeSep 26th 2012

    I kept adding some things to internal hom. It's not done yet, but I need to quit now.

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2012

    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.

    • CommentRowNumber8.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 13th 2017
    • (edited Jul 13th 2017)

    internal hom contained a (trivial) mistake in the sentence

    Formally this says that the functor ()×X(-) \times X of taking the cartesian product with the set SS has a right adjoint given by the construction [X,][X,-].

    I mean, it is obvious from this sentence, at least when taken out of context like above, that the SS is wrong and should be XX.

    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 [X,Y]={f:XY}[X,Y] = \{f : X \to Y\} of functions between two sets XX and YY: that is uniquely characterized by the fact that for any other set SS the functions S[X,Y]S \to [X,Y] are in natural bijection with the functions S×XYS \times X \to Y out of the cartesian product of SS with XX. Formally this says that the functor ()×X(-) \times X of taking the cartesian product with the set SS has a right adjoint given by the construction [X,][X,-].

    in view of the “formal variable” SS, 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:”)

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJun 10th 2018
    • (edited Jun 10th 2018)

    I gave the entry a section Basic properties with statement and proof of some of the basic properties:

    1. X()[X,]X \otimes (-) \dashv [X,-] for each XX is sufficient to have bifunctor [,][-,-];

    2. hom adjunction internalizes as [,[,]][,][-,[-,-]] \simeq [-\otimes -,-];

    3. [,][-,-] preserves limits in second argument and sends colimits in first to limits

    I also did some editorial edits:

    1. Made explicit that the def as stated is for symmetric monoidal categories.

    2. Moved the definition of evaluation map and composition map from “Properties” to “Definition”.

    diff, v56, current

    • CommentRowNumber10.
    • CommentAuthorSixuan Lou
    • CommentTimeJul 4th 2018
    • (edited Jul 4th 2018)

    I think there's a typo in the first equation of proposition 3.3, colimit notation should be changed to the limit notation.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2018

    Thanks for catching this. Fixed now.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2018

    added a small paragraph on and pointer to stable splitting of mapping spaces.

    diff, v61, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2018

    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…

    diff, v61, current

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 28th 2018

    This is not doubting you, but what aspects of “mapping space” spill outside this redirect?

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2018
    • (edited Oct 28th 2018)

    The topological mapping spaces should have a dedicated article of their own, not inside the much broader entry on internal homs.

    • CommentRowNumber16.
    • CommentAuthorTodd_Trimble
    • CommentTimeOct 28th 2018

    Possibly I could be of assistance, if I knew what you’d want included.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeOct 28th 2018
    • (edited Jan 18th 2020)

    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.

  1. Clarification; ’taking … out of’ has an existing and contradictory meaning in English.


    diff, v63, current

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeJan 18th 2020

    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 XX in any sense). And “function out of XX” is a standard mathematical usage for “function with domain XX”, more standard in my idiolect than “function on XX”.

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 19th 2020

    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 XX” or “functions from XX” both work for me (both with the implication of arrows pointing away from, not toward, XX).

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 21st 2020

    Changed to “functions with domain X”, which seems maximally unambiguous.

    diff, v64, current

    • CommentRowNumber22.
    • CommentAuthoraleks
    • CommentTimeJun 3rd 2020

    Fixed typo.

    diff, v65, current

    • CommentRowNumber23.
    • CommentAuthorvarkor
    • CommentTimeSep 7th 2021

    Added link to residual, though I’m not sure these pages ought to be distinct.

    diff, v70, current

    • CommentRowNumber24.
    • CommentAuthorrafayaashary01
    • CommentTimeJul 23rd 2022
    • (edited Jul 23rd 2022)

    Given a monoidal category (𝒞,)(\mathcal{C},\otimes), the usual “provisional” definition of ‘right internal hom of (𝒞,)(\mathcal{C}, \otimes)’ is a (unique in the appropriate sense, if it exists) collection indexed over objects cc of 𝒞\mathcal{C} of functors [c,]:𝒞𝒞[c, -] \colon \mathcal{C} \to \mathcal{C} along with adjunctions c()[c,]c \otimes (-) \dashv [c, -].

    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 (𝒞,)(\mathcal{C},\otimes)’ that we ultimately desire is a bifunctor [,]:𝒞 op×𝒞𝒞[-, -] \colon \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{C} that satisfies

    Hom 𝒞(c 0c,c 1)Hom 𝒞(c,[c 0,c 1])Hom_{\mathcal{C}}(c_{0} \otimes c', c_{1}) \simeq Hom_{\mathcal{C}}(c', [c_{0}, c_{1}])

    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 c 0c_{0}, c 1c_{1} of 𝒞\mathcal{C}, the functor cHom 𝒞(c 0c,c 1)c' \mapsto Hom_{\mathcal{C}}(c_{0} \otimes c', c_{1}) 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 (𝒞,)(\mathcal{C}, \otimes)’ is defined to be a bifunctor [,]:𝒞 op×𝒞𝒞[-, -] \colon \mathcal{C}^{op} \times \mathcal{C} \to \mathcal{C} equipped with a natural (in cc, c 0c_{0}, and c 1c_{1}) isomorphism

    κ:Hom 𝒞(c 0c,c 1)Hom 𝒞(c,[c 0,c 1])\kappa \colon Hom_{\mathcal{C}}(c_{0} \otimes c', c_{1}) \to Hom_{\mathcal{C}}(c', [c_{0}, c_{1}])

    and then to prove as propositions

    1. 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

    2. Thus that a right internal Hom of (𝒞,)(\mathcal{C}, \otimes) is unique if it exists)

    3. That the existence of such a right internal hom is equivalent to the practically weaker condition that for all pairs (c 0,c 1)(c_{0}, c_{1}) of objects of 𝒞\mathcal{C}, the functor cHom 𝒞(c 0c,c 1)c' \mapsto Hom_{\mathcal{C}}(c_{0} \otimes c', c_{1}) is representable.

    In particular, we would be eliding adjunction from the discussion in favor of applying Yoneda’s lemma directly.

    • CommentRowNumber25.
    • CommentAuthorHurkyl
    • CommentTimeJul 23rd 2022
    • (edited Jul 23rd 2022)

    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 c 0,c 1c_0, c_1, define an internal hom to be a representing object* for hom(c 0,c 1)\hom(c_0 \otimes -, c_1) 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 [c 0,c 1][c_0, c_1] and the natural isomorphism hom(,[c 0,c 1])hom(c 0,c 1)\hom(-, [c_0, c_1]) \cong \hom(c_0 \otimes -, c_1) is part of the data.

    • CommentRowNumber26.
    • CommentAuthorvarkor
    • CommentTimeJul 23rd 2022

    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.

  2. removing the previous edit


    diff, v74, current

    • CommentRowNumber28.
    • CommentAuthorRodMcGuire
    • CommentTimeJun 30th 2023


    removing the previous edit

    No you didn’t. You still removed the parenthesis which are needed to understand the composite morphism, which I have restored.

    [Y,Z]×[X,Y]×X(id [Y,Z],eval X,Y)[Y,Z]×Yeval Y,ZZ. [Y, Z] \times [X , Y] \times X \stackrel{(id_{[Y,Z]}, eval_{X,Y})}{\to} [Y,Z] \times Y \stackrel{eval_{Y,Z}}{\to} Z \,. [Y,Z]×([X,Y]×X)(id [Y,Z],eval X,Y)[Y,Z]×Yeval Y,ZZ. [Y, Z] \times ([X , Y] \times X) \stackrel{(id_{[Y,Z]}, eval_{X,Y})}{\to} [Y,Z] \times Y \stackrel{eval_{Y,Z}}{\to} Z \,.

    diff, v75, current