Normally, for a cartesian product between sets $A$ and $B$, we have the notation $$A\times B$$

But what if the set $B$ depends on the first element of the cartesian product? i.e., for each $a\in A$, we have a set $B_a$, such that for all elements of our cartesian product $(a,b)$, we have $b\in B_a$.

Is there a concise notation for this?

  • $\begingroup$ I am not sure I am following, from where $b$ in the $(a,b)$? $\endgroup$ – ℋolo Jul 26 '18 at 13:51
  • $\begingroup$ I think this is what is usually called a "multivalued function" or "set-valued function". $\endgroup$ – Kusma Jul 26 '18 at 14:03
  • $\begingroup$ @Kusma multivalued function is defined using the 2-tuple $(a,\{b\in B\mid aRb\})$ for some well defined $R$ over $A\times B$, there is a single tuple for each $a$ so it does not the same as OP asking(I think) $\endgroup$ – ℋolo Jul 26 '18 at 14:08
  • $\begingroup$ This is exactly the disjoint union of the $B_a$. $\endgroup$ – Malice Vidrine Jul 26 '18 at 15:56

Since you are talking about dependent types, I suggest $(a:A) \to B_a$ or $(a \in A) \to B_a,$ where the former is more "typish" and the latter more mathematical.

If you think "that's a function, not a pair", remember that in mathematics, a function $f : X \to Y$ is defined as a subset of $X \times Y$ such that for all $x \in X$ there exists a unique $y \in Y$ such that $(x,y) \in f.$

But if you want it to look more like a Cartesian product, you could write it as $(a \in A) \times B_a.$

These notations are not standard in mathematics, so make sure to define them in whatever you write.

  • $\begingroup$ "These notations are not standard in mathematics". Do you mean that they are "sometimes used" but not standard, or do you mean that you've just made them up? Either way, I like the notation. $\endgroup$ – user56834 Jul 27 '18 at 6:12
  • $\begingroup$ In Agda dependent types are written as $(a : A) \to B\ a$. The notations in the post are made up by me based on the one in Agda. $\endgroup$ – md2perpe Jul 27 '18 at 6:25
  • $\begingroup$ If we're talking about type theory, the notation $\sum_{a:A}B_a$ is entirely standard, and makes clearer the difference between an indexed family of types and the object the poster is taking about. $\endgroup$ – Malice Vidrine Jul 27 '18 at 17:01

This is the particular case, where $A \times B$ cannot be used, since the set does not have a product structure. Thus, there is not really a notation since it wouldn't make sense. As such a notation would always imply a product structure.

You can always define $$C = \{(a,b) : a \in A, b \in B_a\}$$

  • $\begingroup$ But $B_a$ is not well defined $\endgroup$ – ℋolo Jul 26 '18 at 14:40
  • $\begingroup$ This is indeed what I mean. Is there not a more compact , concise way of writing this? $\endgroup$ – user56834 Jul 26 '18 at 15:44

Given an indexed family of sets $(B_a)_{a\in A}$, the set $\{\langle a,b\rangle\;|\;a\in A\wedge b\in B_a\}$ is just the disjoint union of the indexed family. Depending on context, you may see this as $$\biguplus_{a\in A}B_a$$ or $$\coprod_{a\in A}B_a$$ or $$\sum_{a\in A}B_a.$$

  • $\begingroup$ Also noting that the last of these is more often associated with viewing the structure as a collection of pairs than the others, since in dependent type theories the pair-hood of the elements matters. The other notations tend to appear more often without the connotations of pairhood and with more emphasis on "sets gathered in a non-overlapping manner". But this is an informal comment on the notation, and may be skewed by the specific material I'm familiar with. $\endgroup$ – Malice Vidrine Jul 26 '18 at 16:57
  • $\begingroup$ What I've probably seen most frequently is $\bigsqcup_{a\in A} B_a$. $\endgroup$ – Daniel Schepler Oct 4 '18 at 19:06
  • $\begingroup$ Just in case you're wondering what's going on, take a look at this non-math post for some evidence. $\endgroup$ – user21820 Dec 3 '18 at 4:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.