Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added more details in essentially surjective functor. Please check for details (Mike?).
New entry in my personal lab, somewhat related to the above: compatible idempotent monads (zoranskoda)
Thanks! I reorganized, added links to extant pages, and moved the material about bijective-on-objects functors to bjective on objects functor and bo-ff factorization system. I also removed
if an essentially surjective functor factorizes as where is surjective on objects then is an equivalence of categories.
which doesn’t seem right at all to me, but I’m not sure what you meant to say.
I meant
if an essentially surjective functor factorizes as where is surjective on objects AND fully faithful, then is an equivalence of categories.
Agreeing now ?
By the way – typo in the link in your post above – “bjective”.
Okay, now I agree that it’s true. (-: I wouldn’t be inclined to include it as a “property of essentially surjective functors”, though, since it decomposes into two more “basic” properties: (1) if and is essentially surjective, then so is , and (2) an essentially surjective and fully faithful functor is an equivalence. Note that surjectivity of is not needed.
Well the intention is that b.o. is e.s.o. up to equivalence and that was just making more precise version of one of the directions. I am not sure what is the best thing to organize.
We could say “any functor which is equivalent to a b.o. functor is e.s.o.”?
Of course, but my intention was more, to treat both the strict factorization and weak factorization together and the difference is played precisely by insertint the mentioned equivalence. If b.o. and fully faithful make a strict factorization system then factorizing the same morphism as e.s.o. followed by the fully faithful is not unique as it amounts precisely to the replacement in the previous strict factorization system of the b.o. by any equivalent e.s.o. I agree that the surjectivity of is not needed above, but it is needed to make the factorization unique.
If I am just complicating what in others’ thoughts is useless exercise of trivivialities, never mind.
Side point: the factorization system involving eso functors is not a weak factorization system in the sense usually meant, rather a “2-categorical” or “up-to-isomorphism” factorization system.
I added another paragraph to the page; does this at least partially say what you are getting at?
Right, this looks great. Thanks also for correcting my incorrect wording “weak factorization system”.
Wait, there is nothing specific to homotopy type theory in what you just added. You are essentially just re-stating the usual definition.
It’s great that you are copying material from the HoTT-wiki, but let’s do it a little less mechanically, more with an eye towards retaining logic and cosistency of existing entries.
I seem to remember that at some point Ali Caglyan had created a whole lot of entries on the HoTT wiki which contained essentially nothing but classical definitions. Please do not mechanically copy these all over.
1 to 16 of 16