# Do mathematical objects have underlying types?

I came upon this issue while I was trying to think about what "type" of object is $\mathbb R^n$ - is it a set, a vector space, an inner product space, an affine space, a metric space? Perhaps the simplest way is to define $\mathbb R^n$ as simply being an object of type "set", and then construct new objects such as the vector space $\mathbb R^n$, which possesses an additional structure by having the operations of vector addition and scalar multiplication, or the metric space $\mathbb R^n$, which possesses the additional structure of a metric.

It seems often the case, at least in real analysis, however, that we wish to work with an object (denoted $\mathbb R^n$) which possesses both the algebraic structure afforded by being a vector space and the geometric structure afforded by being a metric space. While I can do all of the calculations, treating $\mathbb R^n$ as both a vector space and a metric space, I am troubled by the fact that I'm not sure which type of object I'm working with. Is it a metric space, or is it a vector space? Is it both? Neither? How should I think about this? (for both the "type" of $\mathbb R^n$ and for mathematical objects in general)

I added a few tags that I thought might be relevant (in areas I'm not quite familiar with), but mods should feel free to remove them if they're not appropiate.

• This is symbol overloading, and should be clear from context. If it's not clear, then specify it. – user296602 Jan 27 '16 at 18:49
• You can approach mathematics in many different ways. – Asaf Karagila Jan 27 '16 at 18:50
• Somewhat often, these "joint objects" that have two seemingly disparate structures have a unification between the structures. For instance $\mathbb{R}^n$ can be thought of as a normed vector space. This way, although a metric has nothing to do with algebra, a norm always has something to do with algebra. Similarly, a topological vector space has the addition and scalar multiplication both being continuous, which creates a connection between the algebra and the topology. – Ian Jan 27 '16 at 18:51
• I highly recommend looking at how such things are handled in proof assistants like Agda or Coq. It will give you an appreciation for how much detail is suppressed, for better and worse, in virtually all mathematical presentations. – Derek Elkins Jan 27 '16 at 18:56
• @ThomasAndrews Statements like that are actually where this sort of question usually comes from, in my experience. People hear things like that, and figure "OK, so everything's set theory, cool", and then they wonder why so little mathematics actually looks like set theory, as written. – Ian Jan 27 '16 at 19:00

Putting things together into an answer and expanding significantly.

First, as T. Bongers stated, this is a form of notational overloading that is usually intended to be resolved by context. The context may be either broad conventions ("standards") such as $\mathbb R^n$'s metric structure, canonical choices such as $\mathbb R$'s field structure, or the convention may be defined in the text you're reading.

Still, if we didn't want to rely on context what would we do and what does this overloading "resolve" to anyway? The typical approach to be more explicit in informal (by which I mean "not machine checked") texts is to do the following:

$$\mathbb{R} \text{ is the set of real numbers} \\ (\mathbb{R},+,0) \text{ is the additive monoid of real numbers} \\ (\mathbb{R},\times,+,1,0) \text{ is the semiring of real numbers}$$

This clearly articulates the additional structure a monoid and a semiring have and what choices we are making here. If we want to treat a semiring as a monoid, we'd have to explicitly forget the extra structure: $U_M(t,m,a,u,z) = (t,m,u)$ (note we'd also have $U_A(t,m,a,u,z) = (t,a,z)$, both $U_M, U_A : \mathbf{SemiRing} \to \mathbf{Monoid}$). Similarly, $U : \mathbf{Monoid} \to \mathbf{Set}$ would be $U(t,m,u) = t$. Compare this with typical statements like $U(\mathbb R) = \mathbb R$.

Being this explicit can often be clarifying and helpful. For example, it's much easier to see and articulate the adjunction in $$\mathbf{Monoid}(FS, M) \cong \mathbf{Set}(S, UM)$$ than in $$\mathbf{Monoid}(FS, M) \cong \mathbf{Set}(S, M)$$ The former can easily be expressed with $F \dashv U$, the latter is awkward to write down without introducing $U$.

The tuple notation can also be very handy. Sticking with the above adjunction, if you want to explicitly define the counit, using the normal, implicit notation leads to some awkwardness and difficulty. In the typical notation you'd be asked to define a natural transformation: $\varepsilon_M : FUM \to M$ natural in $M$. The elements of $FUM$ for a monoid $M$ are just lists of elements of $M$. We need to collapse that list into a single element by multiplying them all together by the monoid operation. $\varepsilon_M(ms) = \text{fold}(?,?,ms)$ but what do we put for the question marks? It should be the multiplication and unit of the monoid, but what are they? The free monoid construction has certainly forgotten them. Moving to the more explicit notation, we see: $\varepsilon_{(M,\oplus,e)}(ms) = \text{fold}(\oplus,e,ms)$.

However, even the approach above is suppressing some aspects. For example, what's the difference between a monoid and a commutative monoid? There is no additional structure, just an additional property of the existing structure. Taking a cue from type theory, the additional evidence we need that a monoid is a commutative monoid is a proof that the operation is commutative. Once we make that explicit, we should then make explicit the evidence that the operation is associative and unital. It's extremely rare for mathematicians to treat proofs as mathematical objects, but this is exactly what modern type theories do.

The cost of all this explicitness, of course, is verbosity and bureaucratic distinctions that can clutter up what is trying to be demonstrated.