Unification of functions

category-theoryfunctionslambda-calculuslogictype-theory

The operator '$\circ$', denoting function composition, takes two functions, $f$, and $g$, satisfying $\text{rng}\ f \subseteq \text{dom}\ g$, and returns a function $g\circ f$, satisfying that $\text{dom}\ g\circ f = \text{dom}\ f$, and that $(g\circ f)(x) = g\big(f(x)\big)$, for every $x \in \text{dom}\ f$.

Consider the following, related operator, which we shall denote by '$\langle\rangle$'. This operator takes $n$ functions, $f_1, \dots, f_n$, for any $n \in \{1,2,\dots\}$, and returns a function, $\langle f_1, \dots, f_n\rangle$, satisfying that $\text{dom}\ \langle f_1, \dots, f_n\rangle = (\text{dom}\ f_1)\times \cdots \times(\text{dom}\ f_n)$, and that, for every $x_i \in \text{dom}\ f_i$, $\langle f_1, \dots, f_n\rangle(x_1, \dots, x_n) = \big(f_1(x_1), \dots, f_n(x_n)\big)$.

For instance, if $f_1:\mathbb{N}^2\rightarrow\mathbb{N}$ is the function $f_1(a,b) = a + b$, and if $f_2:\mathbb{N}\rightarrow\mathbb{N}$ is the function $f_2(c) = c^2$, then $\langle f_1, f_2\rangle$ is the function with domain $\mathbb{N}^2\times\mathbb{N}$, which returns $\langle f_1, f_2\rangle\big((a,b),c\big) = (a+b, c^2)$ for every $a, b, c \in \mathbb{N}$.

Does this operator have a standard name and notation, the way the composition operator has a standard name (namely 'composition') and notation (namely '$\circ$')?

Best Answer

Personally I denote the function as: $$f_1\times\cdots\times f_n$$ If $f_i:A_i\to B_i$ for $i=1,\dots,n$ then: $$f_1\times\cdots\times f_n:A_1\times\cdots\times A_n\to B_1\times\cdots\times B_n$$

It is characterized by the following property:

If $p_i:A_1\times\cdots\times A_n\to A_i$ and $q_i:B_1\times\cdots\times B_n\to B_i$ are the projections for $i=1,\dots,n$ then: $$q_i\circ(f_1\times\cdots\times f_n)=f_i\circ p_i$$for every $i\in\{1,\dots,n\}$.

If $F:\mathbf{Set}^n\to\mathbf{Set}$ is a functor sending objects $(A_1,\dots,A_n)$ to $A_1\times\cdots\times A_n$ then it sends morphisms $(f_1,\dots,f_n)$ to $f_1\times\cdots\times f_n$.

Related Question