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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics comma complex 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 finite foundation 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 homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory 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 nlab 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 stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft 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.
    • CommentAuthorjesse
    • CommentTimeMay 1st 2017

    At equivalence of categories I added a simple example of a non-adjoint equivalence. Maybe it belongs in the page adjoint equivalence instead?

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeMay 1st 2017

    Hmm, I don’t know.

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 1st 2017

    Why not both?

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 2nd 2017

    The wording of the definition in section 2 bothers me. I think it would be better to say “An equivalence consists of two functors F:CDF: C \to D and G:DCG: D \to C together with natural isomorphisms e:FGId De: F \circ G \cong Id_D and h:Id CGFh: Id_C \cong G \circ F” – in other words make the natural isomorphisms part of the structure.

    By defining it as a pair of functors satisfying a property, the next line about adjoint equivalences doesn’t really make sense, or is an empty statement that would imply that every equivalence is an adjoint equivalence. Because of course the data F,GF, G in any such equivalence form a pair of adjoint functors! Instead you want to say that the chosen isomorphisms e,he, h are the counit and unit of an adjunction.

    One also says that a functor F:CDF: C \to D is an equivalence (by abuse of language) if there are G,e,hG, e, h etc.

    • CommentRowNumber5.
    • CommentAuthorjesse
    • CommentTimeMay 2nd 2017

    I agree with Todd; I hope no one minds that I modified the wording so that the data includes a specification of unit and counit.

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2017

    I have added the missing clause “assuming AC” in this prop.

    • CommentRowNumber7.
    • CommentAuthorTobyBartels
    • CommentTimeMay 3rd 2017

    That clause is not necessary; that's the point of the following remark.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeMay 3rd 2017

    Mike, I'm pretty sure that you had some argument that a mere equivalence of categories should consists only of appropriate FF and GG, while an adjoint equivalence includes the natural isomoprhisms among the data. I'll try to find it.

    • CommentRowNumber9.
    • CommentAuthorTobyBartels
    • CommentTimeMay 3rd 2017
    • (edited May 3rd 2017)

    Actually, it's right there in the page; search for the text ‘fraught with peril’, although the argument as it's written is weak. And apparently that was there in the original version, credited to me. But I don't think that I wrote it; I think that I must have borrowed it from somewhere. ETA: Mind you, the phrasing was probably mine, but I don't think that the idea was.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2017
    • (edited May 4th 2017)

    That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.

    But what I am concerned with is that while you and me know this and can see that it is captured by this remark, a reader who is not already expert on these matters is bound to misunderstand what the entry says.

    I am busy right now, but I’ll try to edit further later today, to make the entry satisfy both concerns.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2017

    That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.

    No it doesn’t. The most radical version of this is that in HoTT the theorem is true if equivalence means “strong equivalence” but not assuming any axiom of choice. The point of the “Variants” section is that in other foundations it is true for weak equivalences (by definition) and anaequivalences (by construction) in arbitrary foundations without assuming any axiom of choice.

    However, I agree that the remark doesn’t actually convey the desired information.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2017

    One example of the peril of considering a non-adjoint equivalence to be data is Steve Lack’s paper “A Quillen model structure for 2-categories”, in which his definition of the “equivalence-lifting property” for fibrations in 2Cat, and the generating acyclic cofibrations of the model structure, was incorrect due to this mistake. In “A Quillen model structure for bicategories” he corrected it.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2017

    That remark still applies, with “axiom of choice” interpreted accordingly in the chosen foundation.

    No it doesn’t. The most radical version of this is that in HoTT the theorem is true if equivalence means “strong equivalence” but not assuming any axiom of choice.

    Exactly, because the relevant axiom of choice is just true in that case.

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2017

    Okay I have edited section “Definition” for clarity, and I have expanded the “Idea”-section to transport more of an idea.

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeMay 4th 2017

    Oh, and in the course of this I created a minimum at equivalence in a 2-category

    • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeMay 4th 2017

    If it’s “just true”, it’s not an axiom.

    • CommentRowNumber17.
    • CommentAuthorTobyBartels
    • CommentTimeMay 8th 2017

    How far we have come in our postmodern relativism to say that something is not an axiom because it's just true!

    But seriously, it is sometimes useful to use a redundant list of axioms, so something isn't barred from being added as an axiom because it's already a theorem. In HAF, Eric Schechter brings up the axiom of Finite Choice (that a finite family of inhabited sets has a choice function) for pedagogical purposes. And I sometimes find it helpful to notice that Excluded Middle is equivalent (in a strong enough set theory, that is one with full separation) to Kuratowski-Finite Choice (that a finitely indexed family of inhabited sets has a choice function), even though it is just true if you're already using classical logic (and even hard to distinguish from Finite Choice if you're not already used to noticing applications of Excluded Middle). So it makes sense to say that certain forms of the axiom of Choice are just true without having to strip them of the title of ‘axiom’ first.

    • CommentRowNumber18.
    • CommentAuthorTobyBartels
    • CommentTimeMay 8th 2017

    Attempting to flesh out the context for the equivalence between equivalence and FF ESO, I searched for category theory in homotopy type theory and found a 2013 Café post by Mike about a contemporary paper with Benedikt Ahrens and Chris Kapulkin. So I linked to that, on the grounds that if there's anything better, then Mike would know.

    • CommentRowNumber19.
    • CommentAuthorMike Shulman
    • CommentTimeMay 9th 2017

    If I’m talking about something that I know to be just true but that is a case of something otherwise called an axiom, I often call it a “principle” instead. For instance, the principle of unique choice, aka the principle of function comprehension, is true in set theory and in HoTT (though in CiC and logic-enriched type theory it is an axiom). Here the relevant principle is “functor comprehension”, which is likewise true in the relevant contexts and I would prefer not to call it an axiom. But even if you still call it an axiom, I think one should not say “assuming the axiom of choice” if one is in a context where it does not need to be assumed.

    The present version of the theorem, though somewhat wordy, looks correct to me. (-:

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2017

    Toby, please don’t put direct external links to references. For convenience of the reader and for robustness under link rot, cross references, errata etc., references should always be collected in a list in the References-section, and hyperlinks to resources included there. Even more so if the reference in question really deserves an nnLab entry of its own: I have changed your link to point to the new entry internal categories in homotopy type theory.

  1. adding proof in the context of homotopy type theory

    Anonymous

    diff, v41, current