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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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).

nLab > Latest Changes: anafunction

Bottom of Page

1 to 7 of 7

  1.  
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeApr 27th 2019

    Clarified the relationship between anafunctions and graphs (thanks for the pointer).

    diff, v2, current

    • CommentRowNumber2.
    • CommentAuthorsamwinnick
    • CommentTimeDec 20th 2022
    • (edited Dec 20th 2022)

    This article references a context in which the “axiom of unique choice” fails, (which I am not familiar with), but I am wondering about how or whether the usual axiom of choice comes into play here. I recently learned from the page on anafunctors that there is a way to circumvent the axiom of choice in proving the forward direction of the following statement, and this is to use anafunctors in place of functors:

    a functor is fully faithful and essentially surjective if and only if it is (part of) an equivalence.

    If I understand correctly, this page on anafunction basically argues that (in a typical setup, say ZF) one does not need anafunctions, because this point doesn’t matter in Set as it did in Cat, since in Set, the forward direction “every bijection is an isomorphism” does not require AC, since we recover the inverse of f from the converse of the graph of f. While this is true, the situation pertaining to injections and embeddings is different. The statement “every injection has a left inverse” (as well as the statement “every surjection has a right inverse”) requires AC.

    Question 1: Does the notion of “anafunction” eliminate the need for AC here? If it does, does this mean that “anafunction” is actually a useful concept, say in ZF?

    Actually, I am interested in a slightly different characterization of “embedding” in Set than “having a left inverse”, (but I guess it might be equivalent to “having a left inverse” even without AC so the slight difference is perhaps not so important). I am not as interested in characterizing it as “having a left inverse” because this is not how embeddings work in Cat, and ultimately, I am only here to get intuition on the notion of anafunctor as it pertains to embeddings in Cat. Consider the following two “factorization properties” of Set:

    i. Every function f:X→Yf:X\to Y can be written as f=i∘f′f=i\circ f' where i:Y′→Yi:Y'\to Y is an inclusion and f′:X→Y′f':X\to Y' is surjective, and

    ii. ff is injective if and only if f′f' is a bijective.

    Since the image of a functor is not necessarily a category, statement i does not “categorify” to a statement about Cat, but ii does, and this shows how one must define “embedding of categories” to get a statement analogous to “f is an injection iff f is an embedding”, namely:

    a functor is fully faithful if and only if it is an embedding

    where I would call F:A→BF:A\to B an embedding if there is a natural isomorphism F≅I∘F′F\cong I\circ F', where I:B′→BI:B'\to B is an inclusion functor, and F′F' lies in an equivalence (F,G,η,ε)(F,G,\eta,\epsilon).

    Again the forward direction requires AC, but this time so does the analogous statement about Set. So the notion of “embedding” I am focusing on for Set is basically point ii above: say ff is an embedding if f=i∘f′f=i\circ f' where ii is an inclusion and f′f' is an isomorphism.

    Question 2: Does the notion of “anafunction” fix this? Ie. make it so that the statement “every injection is an embedding” no longer require choice, (with “embedding” as I just defined)?

    If it would be preferable for me to ask this somewhere else like stackexchange or something please let me know. Thank you!

  3. adding reference

    • Mike Shulman, Mathematics without the principle of unique choice. Mathoverflow. Jun 5, 2018. (web

    Anonymous

    diff, v4, current

    • CommentRowNumber4.
    • CommentAuthorDmitri Pavlov
    • CommentTimeDec 21st 2022

    Fixed the broken link.

    diff, v5, current

  5. starting section on anafunctions in dependent type theory

    Anonymous

    diff, v6, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2023
    • (edited Jan 5th 2023)

    hyperlinked more of the technical terms (e.g. type family and categorical semantics)

    where you write of “elements” of a type I hyperlinked to term

    where you had references to “dependent type theory” I suppose it needs “homotopy type theory” or at least “Martin-Löf dependent type theory”, for definiteness, and so I added that, with hyperlinks.

    diff, v8, current

    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeJan 7th 2023

    “Every injection with inhabited domain and decidable codomain has a left inverse” is true without AC. You can even drop the assumption of decidability on the codomain, as long as the image is complenented.

1 to 7 of 7

  1.