So far we’ve been considering the category of vector spaces (over either or ) and adding the structure of an inner product to some selected spaces. But of course there should be a category of inner product spaces.
Clearly the objects should be inner product spaces, and the morphisms should be linear maps, but what sorts of linear maps? Let’s just follow our noses and say “those that preserve the inner product”. That is, a linear map is a morphism of inner product spaces if and only if for any two vectors we have
where the subscripts denote which inner product we’re using at each point.
Of course, given any inner product space we can “forget” the inner product and get the underlying vector space. This is a forgetful functor, and the usual abstract nonsense can be used to show that it creates limits. And from there it’s straightforward to check that the category of inner product spaces inherits some nice properties from the category of vector spaces.
Most of the structures we get this way are pretty straightforward — just do the same constructions on the underlying vector spaces. But one in particular that we should take a close look at is the biproduct. What is the direct sum of two inner product spaces? The underlying vector space will be the direct sum of the underlying vector spaces of and , but what inner product should we use?
Well, if and are vectors in , then they get included into . But the inclusions have to preserve the inner product between these two vectors, and so we must have
and similarly for any two vectors and in we must have
So the only remaining question is what do we do with one vector from each space? Now we use a projection from the biproduct, which must again preserve the inner product. It lets us calculate
Thus the inner product between vectors from different subspaces must be zero. That is, distinct subspaces in a direct sum must be orthogonal. Incidentally, this shows that the direct sum between a subspace and its orthogonal complement is also a direct sum of inner product spaces.