Timeline for Prof and the completion of Cat under right adjoints
Current License: CC BY-SA 4.0
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 11, 2021 at 23:12 | answer | added | varkor | timeline score: 2 | |
| Oct 5, 2021 at 11:23 | answer | added | varkor | timeline score: 2 | |
| Apr 10, 2021 at 13:07 | comment | added | Roald Koudenburg | Ah the last comment is not quite true... Well I hope this is useful, good luck! :) | |
| Apr 10, 2021 at 12:55 | comment | added | Roald Koudenburg | Applying F to $\psi$ and composing with the counit for $(FP_J)^*$ and the unit for $(FT_K)^*$ gives a cell $F'J = (FQ_J)(FP_J)^* \Rightarrow (FT_K)^* (FS_K) \simeq F'K$... | |
| Apr 10, 2021 at 12:47 | comment | added | Roald Koudenburg | @varkor: yes you're right, defining F' on cells requires some work... What might work: any profuctor J: A -|-> B has, besides its graph <J>, also a cograph [J], with inclusions S:A -> [J] and T: B -> [J], such that $J \simeq T^* S_*$ (this is also in Benabou's 2.3.2). In the double category of functors and profunctors between categories it is clear that composing any transformation $\phi\colon J \Rightarrow K$ of profunctors with the universal cells defining <J> and [K] gives a transformation of functors $\psi\colon S_KP_J \Rightarrow T_KQ_J$. | |
| Apr 9, 2021 at 21:14 | comment | added | varkor | @RoaldKoudenburg: is there also a factorisation property for 2-cells? This also seems to be necessary, but I'm not sure what form it should take. | |
| Mar 4, 2021 at 13:51 | comment | added | varkor | @RoaldKoudenburg: I can also believe this. I had been hoping that, if it was true, it was surely proven explicitly somewhere, because it's such an elegant characterisation – but perhaps I simply ought to take the time to work it out myself. | |
| Mar 4, 2021 at 13:15 | comment | added | Roald Koudenburg | I can believe something like "any (pseudo?) functor F:Cat -> K, with every Ff having a right adjoint in K, factors uniquely (up to isomorphism?) through Cat -> Prof". To construct the factorisation F': Prof -> K you use that any profunctor J: A -|-> B factors as $P_*$: A -|-> <J> followed by $Q^*$: <J> -|-> B, where <J> is the graph of J and P and Q are the projections (See Benabou's proposition 2.3.2.) | |
| Mar 4, 2021 at 4:52 | history | became hot network question | |||
| Mar 3, 2021 at 22:15 | answer | added | Tim Campion | timeline score: 11 | |
| Mar 3, 2021 at 20:54 | comment | added | Maxime Ramzi | I don't know the answer, but that's definitely what the cited passage suggests ! | |
| Mar 3, 2021 at 20:48 | history | asked | varkor | CC BY-SA 4.0 |