Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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_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 $a$ and $(a,b)$.
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. I wonder why that could be?
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.
I don’t think that the missing $p_1$ is supposed to be there, just as the corresponding $p_1$ and $p_2$ aren't in the product table. I mean, if I understand what these diagrams are supposed to be.
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.
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.
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…
The $2$-cells are implicit in any diagram called commutative. Perhaps some explicit label is called for, but maybe we can leave it implicit.
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.
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 $\sum_X A$ is the universal object equipped with a map $p_1$ to $X$ and a section $p_2$ of the pullback of the fibration $A\twoheadrightarrow X$ along this map. The pictures are hard to draw with instiki arrays, but here they are in quicklatex:
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 $\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 = X$ and $Q \stackrel{x}{\to} X$is $id_X$, right? Because the dependent term $a$ is simply a section of $A \to X$.
I’m disinclined, because I’d rather emphasize that the base object $X$ 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, $Q$ represents the context $\Gamma$ in which the introduction rule is being applied.
the options come before the package name.
Silly me. Thanks.
It would be nice if quicklatex gave you the LaTeX error messages. (-:
Mike, those diagrams are excellent!
In particular, you clearly separate the projection $p_1\colon \sum_X A \to X$ from the display map $A \twoheadrightarrow X$. These are often the same, but they play different roles.
@Urs #11 first bullet point:
It's $\in \mathcal{C}_{/X}$. One could well write $(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 $A$ for the object in $\mathcal{C}$ rather than for the object in $\mathcal{C}_{/X}$. But if $A$ doesn't mean an object in $\mathcal{C}_{/X}$ rather than just an object in $\mathcal{C}$, then the notation $\sum_X A$ is the abuse.)
1 to 16 of 16