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

nLab > Latest Changes: identity-on-objects functor

Bottom of Page

1 to 30 of 30

  1.  

  1. starting discussion page

    Anonymous

    diff, v4, current

    • CommentRowNumber2.
    • CommentAuthorGuest
    • CommentTimeAug 22nd 2022

    Not every category theorist would agree that the objects of a category form a set.

    What happens if one works in a class theory and the objects of a category forms a class? What happens if one works in a type theory and the objects of a category forms a type? (The morphisms still form sets indexed by pairs of objects) Does the identity on objects still break equivalence invariance in those cases?

  3. added section about definition of an identity-on-objects function in type theory, and how the definition differs from the definition in set theory

    Anonymous

    diff, v4, current

    • CommentRowNumber4.
    • CommentAuthormaxsnew
    • CommentTimeAug 22nd 2022

    I really think we should emphasize what’s written in the “On the other hand,” paragraph. I’ve never seen a usage of identity-on-objects functor that didn’t fit into that description. So just like dagger categories the holy “principle of equivalence” isn’t actually violated when these are used in practice.

  5. first definition not valid in structural set theories like SEAR and ETCS with elements

    Anonymous

    diff, v9, current

  6. renaming page since a proper definition of identity-on-objects which does not violate the principle of equivalence results in something that is not actually a functor.

    Anonymous

    diff, v11, current

  7. reverting the rename: one uses displayed categories instead of identity-on-objects functors if one is concerned about violating the principle of equivalence.

    Anonymous

    diff, v13, current

    • CommentRowNumber8.
    • CommentAuthormaxsnew
    • CommentTimeAug 23rd 2022

    Is this an edit war between two anonymous ppl?

    • CommentRowNumber9.
    • CommentAuthorGuest
    • CommentTimeAug 23rd 2022

    The article states

    However, both these definitions still nevertheless violate the principle of equivalence, for the same reason that the translation of the usual definition of a Grothendieck fibration or strict creation of limits into type theory violates the principle of equivalence

    How does definition 1.3 violate the principle of equivalence? Unlike the case for Grothendieck fibrations, it doesn’t talk about equality of objects at all.

    Unless I suppose one wants to require the correct notion of equality of objects in categories to explicitly be the isomorphisms of the core groupoid of the categories, in which case then categories still violate the principle of equivalence and one really needs univalent categories in the definitions.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeAug 23rd 2022
    • (edited Aug 23rd 2022)

    maxsnew wrote:

    Is this an edit war between two anonymous ppl?

    Probably not, but I second the sentiment: The edit history makes a confusing impression. Anonymous, would you mind choosing a distinguishable pseudonym? You’ll still remain operationally as anonymous as before (if this is really so important??) but we have a better chance to interact with you.

    I really think we should emphasize what’s written in the “On the other hand,” paragraph.

    That seems like a very good point. Unfortunately, just this paragraph was deleted in rev 11.

  11. fixing example: every isomorphism of categories is a fully faithful identity-on-objects functors. Equivalences of categories are only identity-on-objects functors if the two categories are univalent.

    Anonymous

    diff, v14, current

  12. adding source for definition of isomorphism of categories

    Anonymous

    diff, v14, current

  13. the equivalence of categories is specifically adjoint equivalence

    Anonymous

    diff, v14, current

    • CommentRowNumber14.
    • CommentAuthorRodMcGuire
    • CommentTimeAug 24th 2022

    I started this page back in 2017 because I was confused by the newly created page Freyd category.

    There is a bunch of discussion at: nForum: freyd-category

  15. cross linked with bijective-on-objects functor

    Anonymous

    diff, v14, current

    • CommentRowNumber16.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    So, do we restrict the definition of identity-on-objects functor to definition 1.1, and say that structural set theories like ETCS and SEAR cannot define identity-on-objects functors, only bijective-on-objects functor?

    • CommentRowNumber17.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    If we say that definition 1.2 is only a bijective-on-objects functor and not an identity-on-objects functor, then we could create another article equivalent-on-objects functor for definitions 1.3 and 1.4, and say that an isomorphism of categories as defined in the HoTT book is a fully faithful equivalent-on-objects functor.

    • CommentRowNumber19.
    • CommentAuthorGuest
    • CommentTimeAug 24th 2022

    Conjecture: In type theory, identity-on-objects dagger functors, which are a particular kind of identity-on-objects functor between dagger categories which additionally preserve the dagger structure of the dagger categories, between univalent dagger categories in a univalent universe are equivalent to dagger equivalences of univalent dagger categories.

  20. examples moved to equivalent-on-objects functor

    Anonymous

    diff, v17, current

    • CommentRowNumber21.
    • CommentAuthorRodMcGuire
    • CommentTimeAug 24th 2022
    • (edited Aug 24th 2022)

    Can whichever Anomymous who started this thread edit their first comment to include a link to

    https://nforum.ncatlab.org/discussion/7808/freyd-category/

    where this page was created and includes a lot of discussion?

    EDIT: or is it probable that Anonymous/Guests posting in these threads are unable to edit their comments and a Lab Elf needs to do the edit?

    If so this is another reason for Guests to pick some pseudonym to use when posting.

    • CommentRowNumber22.
    • CommentAuthorMike Shulman
    • CommentTimeAug 29th 2022
    • (edited Aug 29th 2022)

    If the intent of definition 1.1 is to be interpreted in univalent type theory where “F obF_{\mathrm{ob}} is the identity” means ∏ x:ObId(F ob(x),x)\prod_{x:\mathrm{Ob}} {\mathrm{ Id}}(F_{\mathrm{ ob}}(x),x), then I suppose you can say that this doesn’t violate the principle of equivalence, but it’s also not a correct definition of “identity on objects functor”, because it’s not equivalent to definition 1.2 in that context. I think Definition 1.2 is the only correct definition, in any foundations, that satisfies the principle of equivalence.

  23. I rewrote the initial few paragraphs on the definitions to take into account Mike Shulman’s comment. Also definition 1.2 was missing the fact that the functions F(x,y):A(x,y)→B(x,y)F(x,y):A(x, y) \to B(x, y) of the “identity-on-object functor” should preserve composition of morphisms and the identity morphism, so I added those in

    Anonymous

    diff, v19, current

  24. copied some relevant information from categories with the same collection of objects

    Anonymous

    diff, v19, current

  25. first source has no relevance to this article anymore since the relevant material was moved to equivalent-on-objects functor

    Anonymous

    diff, v20, current

  26. second source doesn’t actually ever talk about identity-on-objects functors.

    Anonymous

    diff, v20, current

    • CommentRowNumber27.
    • CommentAuthorDaemondave
    • CommentTimeJun 8th 2023
    Hello;

    First time suggester, long time reader.

    I learned many maths in school. including complex calculus, but no category theory, so forgive my misunderstandings.

    I believe there are errors on lines of identity-on-objects functor:

    for each object x:Ob and y:Ob and morphism f:
    Mor(x,y) f o sub(x,y,z) id(x) =f and id(y) o sub(x,y,z) f=f

    Shouldn't it read ?

    for each object x:Ob and y:Ob and morphism f:
    Mor(y,z) f o sub(x,y,z) id(x) =f and id(z) o sub(x,y,z) f=f


    I placed location dots and went through the compositions because I'm not sure I understand, but as written there are discontinuities from source to destination with it as written.
    • CommentRowNumber28.
    • CommentAuthorDaemondave
    • CommentTimeJun 8th 2023
    for each object z:Ob and y:Ob and morphism f:
    Mor(y,z) f o sub(x,y,z) id(x) =f and id(z) o sub(x,y,z) f=f

    One more correction?
    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2023

    I think they’re fixed now – thanks for bringing this to attention.

    diff, v22, current

    • CommentRowNumber30.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 8th 2023

    By the way, if you know LaTeX, then you can use that in comments. Just be sure to select the filter Markdown+Itex (below the comment box) before adding your comment.

1 to 30 of 30

  1.