Coincidentally I came across some very useful notes from John on "groupoidification" the other day which spells out this profunctors = matrices thing in more detail. Unfortunately they are sitting on the math.ucr.edu server, which is still kaput, bu…
think there's a typo here:
There's a tensor product \(V \otimes W\) of vector spaces \(V\) and \(W\), which has dimension equal to the dimension of \(\mathcal{V}\) and the dimension of \(\mathcal{W}\).
should read "the dimension of \(\mathcal{…
@Michael – I think we can simplify your answer slightly:
[ (X \times Y) \times Z = \lbrace \langle\langle x, y\rangle, z\rangle : x \in X, y \in Y, z\in Z \rbrace ]
[ X \times (Y \times Z) = \lbrace \langle x, \langle y, z\rangle\rangle : x \in X,…
@John, thanks for that. It strikes me that this looks very much like the comparison functor between monoids (on a set) and T-algebras, in that we start with a set + associative binary operation + unit and end up with a set + an n-ary operation for e…
@Michael – from what I can make out from the proof of the strictification theorem it doesn't actually collapse all isomorphic objects into one object – it just identifies, eg \(A\otimes (B\otimes C)\) and \((A\otimes B)\otimes C\) for all objects \(…
The final bit of the puzzle is proving the second triangle equation from the first one and the pentagon. I'll just sketch a proof here.
The trick here is to tensor the second triangle equation by \(A\) on the left. This looks like it's making it mo…
OK with a few pointers from that paper I've got a proof that \(\lambda_I = \rho_I : I\otimes I\to I\).
First we note that \(\rho\) is natural, so for any \(\phi : I\otimes I\to I\) we have \(\phi\circ\rho_{I\otimes I} = \rho_I\circ(\phi\otimes 1_I)…
Thanks for those pointers @John – fyi the nLab page says the fact we can derive \(\lambda_I = \rho_I\) from the pentagon and triangle was first proved by Kelly in this 1964 paper:
On MacLane's conditions for coherence of natural associativities,…
ok I think I've got a solution to Puzzle 280
Suppose \(f : I \to I\) and \(g : I \to I\) are morphisms in a monoidal category going from the unit object to itself. Show that \(fg = gf\).
We've seen earlier how to prove
[(1\otimes f)\circ(k…
re Puzzle 281
Going from left to right we have three main blocks:
\(\qquad\Phi \otimes 1_b : a \otimes b \to (c \otimes d) \otimes b\)
\(\qquad1_c \otimes \Psi : c \otimes (d \otimes b) \to c \otimes (e \otimes f)\)
\(\qquad\Theta \otimes 1_f : …
I have a question: how is the "strictification" related to "coherence" (in the sense of the "coherence theorem" in Mac Lane's CWM for instance) – is it a stronger version of coherence? or a modern reworking of coherence? or are the two concepts quit…
re Puzzle 280 I think @Reuben is right that we can solve this using the Eckmann-Hilton argument mentioned earlier in this course. Here's as far as I've got.
First note that Puzzle 278 is basically an "exchange law":
[(f\otimes g)\circ(h\otimes k) …
yes that's true. but tbh I don't really have much of a feel for what a relation is, beyond the formal definition. I mean the relations I'm familiar with are peculiar ones like ordering and equivalence. What's a relation in general tho? umm... err...…
One of the things I've found slightly tricky about profunctors is avoiding the temptation to imagine \(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\) as some sort of map taking things in \(\mathcal{X}\) to things in \(\mathcal{Y}\). This picture kick…
hm well the smallest such \(a\) is \(\text{max}(2b - 3b', 0)\). and I suppose this represents the minimum revenue we need to recycle if we want to get at least \(b\) out while putting at most \(b'\) in.
eg we have $5 to put into the system, can we …
David wrote:
So, the big feasability relation is always \(\mathrm{True}\) (for valid input values). This makes sense if one views the feasability relation as saying what possible stationary states the system can have.
This is what I ended up g…
OK, recapitulating the composition of conjoints rule one last time using opposite profunctors...
We've shown that \(\check{F}(y, z) = \widehat{F^\text{op}}(z, y)\). This is equivalent to \((\check{F})^\text{op} = \widehat{F^\text{op}}\).
From whic…
And on a similar note:
Given a profunctor \(\Phi : \mathcal{X} \nrightarrow \mathcal{Y}\), define \(\Phi^\text{op} : \mathcal{Y}^\text{op} \nrightarrow \mathcal{X}^\text{op}\) by \(\Phi^\text{op}(y, x) = \Phi(x, y)\). It's easy to prove \(\Phi^\tex…
Addendum to the above:
Given a \(\mathcal{V}\)-functor \(F : \mathcal{Z} \to \mathcal{Y}\), define \(F^\text{op} : \mathcal{Z}^\text{op} \to \mathcal{Y}^\text{op}\) by \(F^\text{op}(z) = F(z)\). It's easy to prove \(F^\text{op}\) is indeed a \(\mat…
@John wrote:
Here's a thought: you could try to define the associator and its inverse as companions of enriched functors that are clearly inverses of each other, and then prove \(\widehat{FG} = \widehat{F}\circ\widehat{G}\)... This might require…
Pedantic addendum to @Matthew's solution to Puzzle 224 – we need to prove the associator really is a profunctor.
Suppose \(\langle\langle a, b\rangle, c\rangle \leq \langle\langle x, y\rangle, z\rangle\) and \(\langle x', \langle y', z'\rangle\rang…
This is great proof but I can't help noticing that the argument doesn't work in Top because it's not cartesian closed. Nevertheless the result holds. Now I'm wondering why!
Thought I'd update/fix my previous attempt at proving the first snake inequality given the conventions we've settled on for cap and cup. I've also restricted it to the case where \(\mathcal{V} = \textbf{Bool}\), although the proof works in the gener…
@Keith – surely we already have an isomorphism of \(\mathcal{V}\)-categories \(X \times Y \cong Y \times X\) given by \((x, y) \mapsto (y, x)\). We can check that this is in fact a \(\mathcal{V}\)-functor:
\[ (Y \times X)((y, x), (y', x')) = Y(y, y…
thing is directed graphs have loops in them, but I'm a bit unsure what it would mean to plug the output of a blob directly into one of its inputs. for instance suppose you had \(\Phi : X \nrightarrow Y\) and \(\Psi : Y \nrightarrow Z\) – you could t…