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 comma 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 finite 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 k-theory lie-theory limits linear linear-algebra locale localization logic mathematics 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).
    • 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 RelCRel 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.

  1. Added link to Knowledge Representation in Bicategories of Relations paper

    henry.story@bblfish.net

    diff, v21, current

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJun 15th 2020

    Improved the references a little.

    diff, v22, current