1
$\begingroup$

I'm trying to determine whether defining a type of mathematical object requires us to know what we mean by another object being "equal" to it. For example, when we define a type of object like set, function, category, or class, is it also necessary to include within our definition what is meant by, for instance, two sets, functions, categories, or classes being "equal"? I would appreciate any commentary.


For some background:

I came upon this question when I was thinking about vector spaces. For example, if we want to study the real vector space of functions from $\mathbb R$ to $\mathbb R$, not only do we need to define the operations of addition and scalar multiplication, but I think we also need to define the binary relation of equality in order to check that the vector space axioms hold. For example, to check whether or not for all functions $f,g$ from $\mathbb R$ to $\mathbb R$ and for every real number $\lambda$, that $$ \lambda(f + g) = \lambda f + \lambda g, $$ I think it is necessary to also define what we mean by '$=$' in the above equation, i.e., that $$ ``f = g" \text{ if and only if } f(x) = g(x) \text{ for all } x\in \mathbb R. $$ At what point do we define what is meant by equality of functions? Is it something that is necessary to do as soon as we define what a "function" is?

$\endgroup$
  • 3
    $\begingroup$ You certainly need to know what it means for two functions to be equal. We often don't define it, because the definition is inherited from the set theory definition. Your example is such a case - a function $\mathbb R\to\mathbb R$ is a subset of $\mathbb R\times\mathbb R$ with certain properties, and two functions are considered equal if they are equal as sets. $\endgroup$ – Thomas Andrews Mar 28 '16 at 20:54
  • 1
    $\begingroup$ As others have said, set theory gives you a global equality "for free", but I think it is a very good exercise to explicitly define equality on types that you introduce, ideally as constructively as possible. (In Computational Type Theory, a type literally is a partial equivalence relation on preexisting terms.) This will reveal a lot of hidden complexity, but it will also make you appreciate the fact that checking the equality of linear functions between finite-dimensional vector spaces only involves checking a finite number of inputs. Similarly for polynomials. $\endgroup$ – Derek Elkins Mar 29 '16 at 5:26
5
$\begingroup$

In the set theory paradigm, which is the general workframe of today mathematics, everything is supposed to be a set, so equality has a very clear meaning, given by the extensionality axiom : $x=y$ iff they have the same elements.

For instance a function is a set of the form $(A,B,\Gamma)$ where $\Gamma\subset A\times B$ satisfies some axioms. Then equality of functions is just the equality of the corresponding sets.

Of course this is just in set theory, in different paradigms (like type theory) you are supposed to define equality in a specific way for all types.

$\endgroup$
1
$\begingroup$

Sometimes defining only up to canonical isomorphism is preferable. For example, a definition of direct product up to isomorphism makes it associative, where otherwise it is not.

One interesting reference in connection to this sort of thing is Makkai's work on Anafunctors.

$\endgroup$

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.