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

Discussion Tag Cloud

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.
    • CommentAuthorUrs
    • CommentTimeSep 28th 2012
    • (edited Sep 28th 2012)

    I started creating the following tables for the entry geometry of physics. After having created them there I found that these deserve to be put into the related entries, too. So therefore I put them into their own pages now and included them in related entries via

      [[!include .... - table]]
    

    These are the tables that I have so far:

    These need a bit mor attention. But I have to quit now for the time being. Also, I am afraid I may be running here again against Mike’s preference for notation here and there.

    But I am not dogmatic about this, I just created these tables as they happened to occur to me. I try to polish them later.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 29th 2012

    No, I think I’m fine. (I’m sorry that I come across as so inflexible; I should probably relax some.) I removed some extra right parentheses in the product table, and added what seemed to me to be a missing p 1p_1 in the dependent sum table — although to be honest, I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn’t really distinguish very well between the terms aa and (a,b)(a,b).

    Strangely, in my browser the equation p 2(a,b)=bp_2(a,b)=b in the last row of the product table runs out of its cell and into the next one. I wonder why that could be?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeSep 29th 2012
    • (edited Sep 29th 2012)

    I find the diagrams to be of questionable use in the case of dependent sums, because the category theory doesn’t really distinguish very well between the terms a and (a,b).

    Yes. I had the same thought. So I had first created the table for the products, of course, and then naively started doing the one for dependent sum “along the same lines” only to notice while doing so that it doesn’t quite come out as nicely. The problem is of course that while its a “universal construction” of sorts, it’s not quite (co)-limiting diagram over a simple finite diagram. But maybe it’s still useful, anyway, for the reader to see the morphisms labled as far as it goes.

    Strangely, in my browser the equation p 2(a,b)=b in the last row of the product table runs out of its cell and into the next one.

    Interesting. Same for me. I’ll try to add some whitespace, like

      $\,$
    

    sometimes that helps.

    • CommentRowNumber4.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012

    I don’t think that the missing p 1p_1 is supposed to be there, just as the corresponding p 1p_1 and p 2p_2 aren't in the product table. I mean, if I understand what these diagrams are supposed to be.

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeOct 1st 2012
    • (edited Oct 1st 2012)

    I don’t think

    Ah, that’s right. Now I have looked at it.

    I had tried to mimic in the diagrams what happens in term introduction/elimination/computation by drawing only those arrows that interpret the given step. So

    • for term introduction only the arrows into the new object;

    • for term elimination those out of the object;

    • for computation both of them, hence the commuting diagram they form.

    But, as we said, for dependent sum this doesn’t work quite as well as for products.

    • CommentRowNumber6.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012

    for computation both of them, hence the commuting diagram they form

    In fact, I would say: for computation, the commuting diagram (a 2-cell) they form, hence (necessarily as forming the boundary of that diagram) both of them.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeOct 1st 2012
    • (edited Oct 1st 2012)

    Yes, good point. Maybe we should indicate the 2-cell. But that will blow up the size of the diagram a good bit…

    … unless of course somebody feels inspired to create some SVG…

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeOct 1st 2012

    The 22-cells are implicit in any diagram called commutative. Perhaps some explicit label is called for, but maybe we can leave it implicit.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeOct 1st 2012
    • (edited Oct 1st 2012)

    The 2-cells are implicit in any diagram called commutative.

    Yeah, that’s why I did the diagrams the way I did them. But I thought you had just been suggesting in #6 to make them explicit.

    But never mind, I guess we agree either way.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012

    Mulling this over some more, I think there is a better way to describe dependent sums categorically in this style. The universal property we should be using is that XA\sum_X A is the universal object equipped with a map p 1p_1 to XX and a section p 2p_2 of the pullback of the fibration AXA\twoheadrightarrow X along this map. The pictures are hard to draw with instiki arrays, but here they are in quicklatex:

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012
    • (edited Oct 2nd 2012)

    Thanks! I have added that into dependent sum natural deduction - table

    Some questions:

    • In the formation rule would it be better to label the vertical arrow by 𝒞 /A\in \mathcal{C}_{/A} than by 𝒞\in \mathcal{C}?

    • How do I make quicklatex display xymatrices? I did add

      \usepackage{xy}[all]
      

      in the quicklatex preamble, but that didn’t help.

    • in the term introduction rule, strictly speaking Q=XQ = X and QxXQ \stackrel{x}{\to} X is id Xid_X, right? Because the dependent term aa is simply a section of AXA \to X.

    • CommentRowNumber12.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012
    • I’m disinclined, because I’d rather emphasize that the base object XX is part of the input data too.

    • the options come before the package name.

    • I think by analogy with what you wrote in the other tables, QQ represents the context Γ\Gamma in which the introduction rule is being applied.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeOct 2nd 2012

    the options come before the package name.

    Silly me. Thanks.

    • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeOct 2nd 2012

    It would be nice if quicklatex gave you the LaTeX error messages. (-:

    • CommentRowNumber15.
    • CommentAuthorTobyBartels
    • CommentTimeOct 17th 2012
    • (edited Oct 17th 2012)

    Mike, those diagrams are excellent!

    In particular, you clearly separate the projection p 1: XAXp_1\colon \sum_X A \to X from the display map AXA \twoheadrightarrow X. These are often the same, but they play different roles.

    • CommentRowNumber16.
    • CommentAuthorTobyBartels
    • CommentTimeOct 17th 2012
    • (edited Oct 17th 2012)

    @Urs #11 first bullet point:

    It's 𝒞 /X\in \mathcal{C}_{/X}. One could well write (A𝒞 /X)( XA𝒞)(A \in \mathcal{C}_{/X}) \Rightarrow (\sum_X A \in \mathcal{C}), if the slice category is understood to consist only of display maps. (Later we abuse notation and use AA for the object in 𝒞\mathcal{C} rather than for the object in 𝒞 /X\mathcal{C}_{/X}. But if AA doesn't mean an object in 𝒞 /X\mathcal{C}_{/X} rather than just an object in 𝒞\mathcal{C}, then the notation XA\sum_X A is the abuse.)