Not signed in (Sign In)

Start a new discussion

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 bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics 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 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 homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory kan 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 natural nforum nlab nonassociative 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 string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topological topology topos topos-theory 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.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 7th 2017

    Added some structure and references to Barr embedding theorem.

    • CommentRowNumber2.
    • CommentAuthorjesse
    • CommentTimeJun 7th 2017
    • (edited Jun 7th 2017)

    Amusingly, Makkai has published at least 4 proofs of Barr’s embedding theorem:

    • Full embeddings I, which uses ultraproducts of models of the internal logic of regular categories;

    • Full continuous embeddings of toposes, where he gives two different proofs, first as a corollary of an embedding theorem for coherent prime-generated toposes, and then as model-theoretic recasting of Barr’s proof (interestingly, he says that the key construction in Barr’s proof is analogous to Morley’s construction of prime models for totally transcendental theories);

    • Stone duality for first-order logic, where he obtains the result from Full embeddings I via the machinery of ultracategories.

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 7th 2017

    Which of those is the nicest? :-)

    I’m not sure I’ve ever pored over all the details carefully (it’s in Mac Lane and Moerdijk of course), but I’ve seen it mentioned that you need a classical metalogic to prove it. Which sort of goes under the “no free lunch” principle, I suppose.

    • CommentRowNumber4.
    • CommentAuthorjesse
    • CommentTimeJun 7th 2017

    I’m not sure about nicest, but the most straightforward (and by that I mean the only one I can currently understand) is Full embeddings I.

    It’s looking like my master’s thesis is going to be about Makkai duality, though, so maybe after I understand ultramorphisms the latter two will become clearer :^)

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 8th 2017

    Awodey and Forssell discuss Makkai duality as they propose their own form of duality for first-order logic. Presumably, you take there to be more mileage in Makkai’s approach.

    • CommentRowNumber6.
    • CommentAuthorjesse
    • CommentTimeJun 8th 2017

    I don’t know yet about Makkai’s approach having more mileage. The main application I have in mind is testing if a functor Mod(T)Set\mathbf{Mod}(T) \to \mathbf{Set} is actually evaluation-at-an-object-of-Syn(T)\mathsf{Syn}(T). Preservation of ultraproducts and ultramorphisms seems like a nice way to go about this. Maybe testing if such a functor is actually a formal sheaf (in Awodey and Forssell’s terminology) on the topological groupoid core(Mod(T))\operatorname{core}(\mathbf{Mod}(T)) would be nicer. I should definitely find out!

    • CommentRowNumber7.
    • CommentAuthorPeter Heinig
    • CommentTimeJun 10th 2017

    Many thanks for these valuable comments.

    • CommentRowNumber8.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    The footnote currently at Barr embedding theorem doesn’t look right to me. I understand an “embedding” of categories to mean a fully faithful functor. “Faithful” doesn’t mean injective on morphisms but rather injective on each hom-set as a function hom(A,B)hom(FA,FB)\hom(A, B) \to \hom(F A,F B). Nowadays (although maybe not always in the past), embedding usually means “full embedding”. And I understand the notion of embedding to be agnostic on the issue of injective-on-objects.

    • CommentRowNumber9.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 19th 2017
    • (edited Jul 19th 2017)

    Thanks for raising this point.

    The footnote currently at Barr embedding theorem doesn’t look right to me.

    Would you please clarify whether you mean “not logically right” or “not right in its claim of this being the usual notion of embedding”.

    To me the logical implication stated there seems obviously right. (It FF is a functor whose morphism-class-function F| mor(dom(F))F|_{mor(dom(F))} is injective, then in particular the restriction to any hom-set is injective, hence it is faithful. And even more particularly, the restriction of the morphism-class-function of FF to the class of all identity-morphism is injective, if FF is, because of the bijective correspondence between objects and identity arrows, hence the injective-on-objects claim.)

    Is there something eluding me, logically I mean?

    I agree that the condition given is somewhat stronger than fully-faithful functor.

    To me there seems not to be a logical mistake.

    • CommentRowNumber10.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    Would you please clarify whether you mean “not logically right” or “not right in its claim of this being the usual notion of embedding”.

    The latter: that is simply not what an embedding of categories is, at least not in the language I am used to. Sorry for leaving that ambiguous.

    Yes, I agree that your implication is correct, but I don’t think it’s the right notion.

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJul 19th 2017

    Todd, Barr in his article “Embedding of categories” (pdf) uses at times the term “full embedding”. That seems to mean that for him an embedding is not generally a full functor.

    Unfortunately the article seems to never define “embedding”.

    • CommentRowNumber12.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 19th 2017
    • (edited Jul 19th 2017)

    Re # 10: thanks for clarifying.

    As an exercise, I tried to remember why it was written like that. Oddly, I seem to recall that I consciously decided not to write that embedding is the same is faithful functor, and that I was taking the present version from a publication, but, oddly, I do not recall what a reason was.

    I agree that this looks like something like misleading-emphasis. And the “In category theory […]” is a bit odd in a lab book on category theory. I think that was a result of over-conscientiously trying to wrap the definition into a context.

    It would be good if you improve the footnote.

    Re #8:

    I understand an “embedding” of categories to mean a fully faithful functor.

    This puzzles me. To me, the by far most usual definition “embedding” is “faithful functor”, without “full”. (Cf. e.g. Mac Lane, 2nd ed. p. 15, line 1). I know that some treatments of the Yoneda embedding can lead one to believe that “embedding” in particular implies “full”, but this seems not the default. Whence usages like “full embedding”. Would you please clarify?

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    I’m happy to be corrected, and I agree the term “full embedding” is frequently found in the literature – which does raise the question! But certainly I would think that the injective-on-morphisms is not what is commonly accepted these days.

    I think it’s become more common in recent years to consider an embedding of categories as meaning full by default, but this deserves further discussion.

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    Mac Lane’s book in its first edition is a notable example of the more old-fashioned usage. The 2nd edition was written in the 1990’s, when Mac Lane was rather old (I saw him every week in those days) and there may have been somewhat less editorial oversight than for the first edition. (The book is still deservedly a classic.) The whole business of what we at the nLab have sometimes referred to as “evil” or the principle of equivalence was not prominent in his mind – I am reasonably sure of this, based on conversations I had with him.

    By the way: embedding, while it has some good points, doesn’t really discuss the case of categories yet.

    Let’s hear from a few others before making changes. The whole issue of what we mean by a “subcategory” is an interesting one; see for example this MO discussion.

    • CommentRowNumber15.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 19th 2017

    Thanks for clarifying.

    By the way: embedding, while it has some good points, doesn’t really discuss the case of categories yet.

    Now that you say that: I recall that I visited that nLab page before writing the footnote, found nothing “authoritative” (as they say) in there, and had recourse to some source I do not recall. The “In category theory, …” was sort of a reflex and gives a misleading air of authoritativeness to the footnote.

    • CommentRowNumber16.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 19th 2017
    • (edited Jul 19th 2017)

    Rummaging turned up what probably was my source: TheJoyOfCats has it literally this way: 3.27 says “FF is called an embedding provided that FF is injective on morphisms.”

    Aware that this seems at least wrong-in-spirit, I probably felt I had better comment on “faithful”, and fascinated by objects-are-identity-morphisms I was led to even mention objects.

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    Wow! Okay… that’s interesting. Thanks for digging that up!

    I still think that’s a little weird, and still think further discussion is called for. I mean, up to set-theoretic implementations/hacks, we can arrange for (something isomorphic to) the forgetful functor GrpSetGrp \to Set to be an embedding in this sense. Does anyone find that a good use of language?

    In short, this notion of embedding ignores principle of equivalence, and I think that’s an issue.

    • CommentRowNumber18.
    • CommentAuthorMike Shulman
    • CommentTimeJul 19th 2017

    Yes, an “embedding” of categories should definitely refer to an equivalence-invariant notion, and I would personally define it to mean a fully faithful functor. Joy of Cats is generally not very good with terminology, IMHO.

    • CommentRowNumber19.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017
    • (edited Jul 19th 2017)

    I think we should continue searching the literature.

    In view of Urs’s #11, I decided to look in Toposes, Theories, and Triples. What I found was interesting: Barr and Wells say an embedding is a faithful functor which takes non-isomorphic objects to non-isomorphic objects (page 89, or 102/302 of the pdf). They call it a “common convention”; where else is this attested?

    • CommentRowNumber20.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 19th 2017

    And then there is good old Wikipedia, which lists four conventions.

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2017

    They call it a “common convention”; where else is this attested?

    It can’t be that common; I’ve never heard of it before. It seems bizarre to me (and not just because of the totally unnecessary contrapositive); wouldn’t it be much more natural to talk about a pseudomonic functor that is full on specific isomorphisms rather than merely about the property of being “isomorphic”?

    I only see three conventions on wikipedia: full and faithful, full and faithful and injective on objects, and faithful and injective on objects. Requiring injectivity on objects would mean, in particular, that the “Yoneda embedding” is not necessarily an embedding, or at least that whether or not it is always an embedding depends on the set-theoretic details of how we define “category” — specifically, whether we require distinct hom-sets of a category to be disjoint. If it can happen that two distinct (but necessarily isomorphic) objects XX and YY have C(Z,X)=C(Z,Y)C(Z,X) = C(Z,Y) as sets for all ZCZ\in C, then the Yoneda embedding would not be injective on objects since it would take XX and YY to literally the same presheaf. (This equality of hom-sets is not as weird as it might sound; for instance, when regarding a preordered set as a category it’s natural to define every nonempty homset to be the same terminal set.)

    Injectivity on objects is just not a sensible condition to require of non-strict categories, and “embedding” is a word that we want to apply to non-strict categories. And mere faithfulness doesn’t seem to me strong enough to merit being called an “embedding”. I could perhaps see an argument for pseudomonicness, but in general I think of an “embedding” as meaning “all relevant structure on the domain is induced by the codomain” and to me in the case of categories that structure includes “the hom-sets”.

    In any case, whatever we decide, we should record the reasons and possible variations on the lab for the benefit of future readers.

    • CommentRowNumber22.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 20th 2017
    • (edited Jul 20th 2017)

    Re # 19.

    I think we should continue searching the literature.

    Well, I’ve got a little list.

    But please do not take this as the findings of a night-long literature-search, or anyting like that, I merely surveyed a few well-known sources, without method of search, for a set time of half an hour this morning (and stuck to that, breaking off the compilation when the time had come).

    And, to say a needless-to-say thing, there is not the true definition of a word, and matters of truth are not decided by majority votes. And I am unsure about the point of doing this; but certainly understanding can come of discussing this (a bit), though not necessarily of a rigid survey of definitions in the literature.

    So, here goes:

    • Prouté in his French lecture notes on categorical logic, seems not to give a definition of “plongement” as such, but somehow leads readers to believe that there is an absolute meaning of “plongement” when he says in a footnote “On justifiera le mot “plongement” un peu plus loin.” [We will justify the word “embedding” a little further below.] and then before Proposition 148, which says “Le foncteur de Yoneda est plein et fidèle.” he says “C’est la raison pour laquelle on l’appelle “plongement” “.

    • Schubert, Kategorien I, defines it to mean injectivity of the restrictions to the hom-sets, i.e., if I am not mistaken, Schubert has Mac Lane’s (embedding)==(faithful functor).

    • Brandenburg, Kategorientheorie seems noncommittal; I did not find (not searching long) “Einbettung” being defined absolutely.

    • Shapira, herein takes a micro-local approach to this issue, mentioning the word “embedding” only once, packaged into “Yoneda embedding”.

    • Asperti and Longo, in “Categories, Types and Structures”, apparently define “embedding” only part-and-parcel with “full”: below 3.1.3 Proposition one reads: “A functor F:CDF\colon C\rightarrow D is a full embedding iff it is full and faithful, and it is also injective for objects.” Here, the injectivity-on-objects condition raises its head again. (And “injective for objects” is unusual.

    • Riehl, Category Theory in Context, SEction 1.5 writes “A faithful functor that is injective on objects is called an embedding and identifies the domain category as a subcategory of the codomain;” So this author for some reason was led to go beyond Mac Lane’s (embedding)==(faithful functor) by a somewhat-doubly-**** formulation “injective on objects” (shudder). [I seem to recall that when the fateful footnote was written, I had had a look in Riehl’s book too, and found my doubts about mentioning objects dispelled by finding them mentioned there, too.] [And of course, to be hyper-correct, Riehl only tells readers that if a faithful functor is injective on objects, into the bargain, then it is called “embedding”. Logically, the author does not tell readers how to complete (embedding)=>?, but this is a near-universal abuse of language.] Riehl then goes on to write

    […] identifies the domain category as a subcategory of the codomain; in this case faithfulness implies that the functor is (globally) injective on arrows. A full and faithful functor, called fully faithful for short, that is injective-on-objects defines a full embedding of the domain category into the codomain category. The domain then defines a full subcategory of the codomain.

    In particular, this author takes the global injective-on-morphisms-definition, that JoyOfCats takes to be the definition, to be a consequence of faithfulness.

    I could go on and (try) to condense all of this, but (for the time being), won’t since the set time is up.

    • CommentRowNumber23.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    I only see three conventions

    You’re right. The fourth was a repeat of the first. :-)

    • CommentRowNumber24.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Isn’t this a strange and surprising situation? You’d a’ thunk that a basic-sounding notion like “embedding of categories” had been firmly settled by now. (Obviously, up until yesterday I thought it had been, as a fully faithful functor, although I had the sense that some of the older books had a different convention.)

    I agree with Mike that the nLab, dictionary-like, should dutifully record the variations we see occurring.

    I can’t remember seeing an “embedding theorem” where the embedding wasn’t full though. And this injective-on-objects business continues to be weird and surprising to me. Mike, would it be possible to ask Emily her reasoning?

    Worth bringing up at the Categories list? Although I tune in very rarely myself.

    • CommentRowNumber25.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 20th 2017
    • (edited Jul 20th 2017)

    Just to remind us of something many of us likely know: it might be seen as a (post-)modern approach to not try to “settle” this in the sense of finding—or even decreeing—an absolute definition the term “embedding”, but rather take the stance that it is alway only defined within a context, in particular, to take the stance that “embedding” on its own is simply undefined, and forever will be, and only exists …err…embedded? into a certain context.

    But I personally like this “record”ing/documenting/commenting/situating-the-published-literature-idea that Todd is mentioning, at least because of the educational value of the process of doing so (within reason).

    • CommentRowNumber26.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 20th 2017

    Just to add a bit more context:

    • in [Awodey. Category Theory, OUP, second edition, below 8.1], the injective-on-objects-condition raises its head again: “A functor F:CDF\colon\mathsf{C}\rightarrow\mathsf{D} is called an embedding if it is full, faithful, and injective on objects.”

    • The Elephant seems noncommital on the issue (though it uses the formulation “full embedding”, making it seem that it does not by default take “embedding” to imply fullness), at least it does not trumpet its views on this (neither in its introductory, convention-establishing pages, nor in its index).

    • CommentRowNumber27.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Another lens to be viewing this through is stuff, structure, property. The fully-faithful version is mandated if categorical embeddings are considered as corresponding to, morally speaking (i.e., up to equivalence), a property or set of properties that carve out the subcategory.

    Some of the notions might be justified by viewing CatCat as a 1-category only, ignoring the 2-categorical aspects. What do regular monomorphisms in the 1-category CatCat look like?

    • CommentRowNumber28.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    I find Steve’s definition understandable, especially when viewed in the context of teaching beginners. Embeddings which are non-injective on objects might be hard for beginners to swallow! And (assuming AC) any fully-faithful functor is isomorphic to an Awodey-embedding, so he’s “not far off”. :-)

    • CommentRowNumber29.
    • CommentAuthorPeter Heinig
    • CommentTimeJul 20th 2017

    And (assuming AC) any fully-faithful functor is isomorphic to an Awodey-embedding, so he’s “not far off”.

    Naturally. But would he allow (beginners to use) AC?

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJul 20th 2017
    • (edited Jul 20th 2017)

    I won’t have time for this. But you who care about it should please start adding all this material into embedding of categories.

    To start with, I have removed that footnote at Barr embedding theorem and instead hyperlinked “embedding” right away.

    • CommentRowNumber31.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Re #29: I expect so. It’s part of standard mathematics after all.

    There may be some category theorists who are opposed to AC on “religious grounds”, so to speak, but I expect most aren’t. That said, I think category theorists tend to be highly attuned to when AC and excluded middle are involved, since an argument which doesn’t use these principles will be available in wider categorical contexts than otherwise. That is unquestionably the case for categorical logicians like Steve.

    • CommentRowNumber32.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Thanks for the nudge, Urs. I was going to get to that anyway (and it’s good to collect our thoughts here as well).

    • CommentRowNumber33.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    I changed the wording in the idea section of embedding of categories, added a little to a definitions section, and added two references so far. Quite a bit remains.

    • CommentRowNumber34.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017
    • (edited Jul 20th 2017)

    And (assuming AC) any fully-faithful functor is isomorphic to an Awodey-embedding

    No wait, what am I saying? That’s obviously nonsense.

    • CommentRowNumber35.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2017

    I think every fully faithful functor is equivalent to one that’s injective on objects, without any need for choice. Let f:CDf:C\to D be fully faithful, and let EE be the “mapping cylinder” category, whose objects are the disjoint unions of those of CC and DD, with CC and DD embedded fully-faithfully (and of course injectively on objects), and E(c,d)=D(fc,d)E(c,d) = D(f c,d) and E(d,c)=D(d,fc)E(d,c) = D(d,f c). Full-faithfulness of ff allow us to compose all arrows in EE making it a category. There is a projection EDE\to D that is the identity on DD and acts by ff on CC, and which is an inverse equivalence to the inclusion DED\to E. Thus, f:CDf:C\to D is equivalent, in the 2-category whose objects are functors and whose morphisms are pseudo-commutative squares, to the inclusion functor CEC\to E, which is fully faithful and injective on objects.

    • CommentRowNumber36.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Good. That should be added to the article at some point.

    • CommentRowNumber37.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2017

    What are the regular or extremal monos in the 1-category Cat? Those seem like also a natural candidate for a 1-categorical notion of “embedding of categories”.

    • CommentRowNumber38.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    (I too asked about regular monos in CatCat in #27.)

    • CommentRowNumber39.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2017

    Oh, I missed that, sorry.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJul 20th 2017

    I added #35 and some more possible definitions to embedding of categories, and tried to make it a bit more agnostic as to which definition is “correct”.

    • CommentRowNumber41.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 20th 2017

    Great! Seems to be coming together, although there are still unanswered questions.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)