Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorTodd_Trimble
• CommentTimeAug 25th 2012

More propositions and stuff entered at bicategory of relations.

• CommentRowNumber2.
• CommentAuthorFinnLawler
• CommentTimeOct 22nd 2012

Started trying to finish off the proof that a bicategory of relations is the same thing as a unitary pre-tabular allegory. What I’ve put there is pretty vague for now; I think the basic idea is solid, but it needs a bit more work.

• CommentRowNumber3.
• CommentAuthorMike Shulman
• CommentTimeOct 23rd 2012

Thanks! I don’t have time to read this over right now (though I’m looking forward to it later) but I just wanted to point out that we do have cartesian bicategory spelled in lowercase. I added a redirect for the capitalized version.

• CommentRowNumber4.
• CommentAuthorFinnLawler
• CommentTimeOct 24th 2012

OK, I’m pretty happy with this now. See what you think.

• CommentRowNumber5.
• CommentAuthorTodd_Trimble
• CommentTimeOct 24th 2012

It might be nice to summarize the long calculation in terms of things like string diagrams. (But I’d have to think about what I mean by that, exactly, since there is an obvious objection here that this would be circular.)

• CommentRowNumber6.
• CommentAuthorFinnLawler
• CommentTimeOct 25th 2012

I agree, it’s not very pretty, but of course string diagrams only make sense if the tensor is functorial. If you like I could draw out the diagrams I used and upload them – I don’t have a scanner, but maybe a photograph of the page would do.

• CommentRowNumber7.
• CommentAuthorTodd_Trimble
• CommentTimeOct 25th 2012

That might help! Thanks.

• CommentRowNumber8.
• CommentAuthorMike Shulman
• CommentTimeNov 3rd 2012

When you say “string diagrams only make sense if the tensor is functorial” I presume you’re referring to string diagrams for a monoidal (bi)category. But mightn’t there be some other kind of string diagram that would work here? It seems like the string diagrams here would need to talk about local finite products rather than the tensor, anyway.

• CommentRowNumber9.
• CommentAuthorFinnLawler
• CommentTimeNov 4th 2012

@Todd: I’ve uploaded a PDF to my personal web instead: here. Sorry about the delay — I found a tiny mistake that meant I had to throw out and re-prove a bunch of stuff.

@Mike: Not the way I did it, no. The difficult bits don’t stay in a single hom set, as you can see in the PDF. But of course I may just have done it in an over-complicated way.

• CommentRowNumber10.
• CommentAuthorMike Shulman
• CommentTimeNov 4th 2012

Couldn’t we prove this in a slicker way like this? Any unital pretabular allegory embeds into a unital tabular allegory by splitting its coreflexives. But every unital tabular allegory is the allegory of relations in a regular category, which we know is a bicategory of relations, and any full sub-bicategory of a bicategory of relations that’s closed under the tensor product (both binary and nullary) is again such.

• CommentRowNumber11.
• CommentAuthorFinnLawler
• CommentTimeNov 4th 2012
• (edited Nov 5th 2012)

Oh, yes, good idea. That’s much simpler. I might end up using that instead (with credit, of course).

Edit: OK, I’ve changed bicategory of relations accordingly. Much nicer.

• CommentRowNumber12.
• CommentAuthorMike Shulman
• CommentTimeNov 5th 2012

It’s at least simpler if we assume as known the properties of splitting coreflexives in allegories, and the equivalence of unital tabular allegories with regular categories. It’s not clear to me that those proofs, written out in full, are any shorter than your direct proof — but perhaps this way is more intuitive.

Although I have to admit I feel a little dirty whenever I prove anything by invoking an embedding theorem….

• CommentRowNumber13.
• CommentAuthorFinnLawler
• CommentTimeNov 6th 2012

That’s a fair point, but your way is definitely more intuitive and ’structural’ generally. As for using an embedding theorem, it does feel a bit like cheating, doesn’t it? But then it’s hardly any different to, say, proving things about real numbers using complex analysis, or hyperreals. In fact, the basic argument in the original direct proof is essentially the same as the one in the proof that $Rel C$ is a bicategory of relations. So if we unwound or ’beta-reduced’ the slick proof far enough, we’d probably arrive at something quite like the direct one.

• CommentRowNumber14.
• CommentAuthorMike Shulman
• CommentTimeNov 6th 2012

A good point.

It’s striking how much I find myself thinking about “beta-reducing” proofs, now that I’ve more or less internalized proofs-as-programs. I wonder whether it’s something I did as much before but just without having a name for it.