A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i)

A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i)

A proof of \(\mathcal K \otimes V \cong V\) using the universal property of the tensor product (Category theory in context Edition 1, 2.3.ii.i)

I found this little exercise super fun, but it took me some days to finally see it. The question is this

Let \(V\) be a vector space over a field \(\mathcal K\). Prove that \(V \cong \mathcal K \otimes V\).

I will take a non-dry formal approach on how to see this is true. We will do this without the explicit construction of what we specifically mean is a tensor space.

1. Uncle Yoneda will give you the basic framework

Tensor products are intimately related to bi-linear forms 1. If we study the functor \[ \text{Bilim}(V,W; -) : \text{Vect} \to \text{Set} \] under the Yoneda lemma we get the following natural isomorphism \[ \forall C, \text{Nat} \left( \text{Vect}(C, -) ; \text{Bilim}(V,W; -) \right) \underbrace{\cong}_{ \leftarrow \psi } \text{Bilim}(V,W; C) \] On top of Yoneda, we get a universal property for Bilim, as when \(C = V \otimes W\) the universal object and \(\otimes : V \times W \to V \otimes W\), \(\otimes \in \text{Bilim}(V,W; V \otimes W)\) the universal element. Basically this means that \[ \psi \left( \otimes \right) : \text{Vect}(V \otimes W, -) \to \text{Bilim}(V,W; -) \] it not just a natural transformation between functors, it is in fact a natural isomorphism between these functors. \[ \text{Vect}(V \otimes W, -) \cong \text{Bilim}(V,W; -) \] where \(V, W\) are arbitrary.

So what? where is going this anyways? Well the book had a previous example of how this can be useful. We will see how the identity morphism of some space will deform through these functors and natural transformations to establish the result we want.

2. You should look at the functor \( \text{Vect}(\mathcal K \otimes W, -) \)

Here \(\mathcal K\) is seen as a trivial vector space over itself. By the previous section we know that \[ \text{Vect} \left( k \otimes V, - \right) \cong \text{Bilim}(k,V; -) \cong \text{Bilim}(V,k; -). \] So far so good. Here is something interesting, by currying, Bilim can be seen a two stacked Vect functors: \[ \text{Bilim}(V,k; -) \cong \text{Vect} \left(V,\ \text{Vect}(k , -) \right) \] this is clear from the definition of what bi-linearity means, linear of each variable by each own.

3. That \(\text{Vect}(k , -)\) is interesting tho

Yeah, if you know some functional programming you will know that \[ \forall a. \text{Unit} \to a \cong a. \] This is the equivalent for linear function

3.1. Lemma: for all \(Y\) vector spaces, \( \text{Vect}(k, Y) \cong Y \) as a vector space.

This is informal, but here is the intuition. Let us take an \(f \in \text{Vect}(k, Y)\) freely. Given that is a linear function, we have that \[ \forall z \in \mathcal K, f(z) = z \cdot f(1). \] So this means that the element \[ \vec y = f(1) \] has all the special info needed to identify \(f\). This is a way to establish the isomorphism that we are declaring.

4. How does this help us?

Oh yeah, remember that \[ \text{Vect} \left(V,\ \text{Vect}(k , -) \right)? \] I declare that this is isomorphic to \[ \text{Vect} \left(V,\ \text{Vect}(k , -) \right) \cong \text{Vect} \left(V,\ - \right) \] by the previous lemma.

Joining all the previous natural isormophisms we reach that \[ \text{Vect} \left( k \otimes V, - \right) \underbrace{\cong}_{\to p} \text{Vect} \left(V,\ - \right) \]

5. OK cool, but that does not establish the result!

We are just missing the final step. We know for a previous section of the book that homset are a really nice kind of functors. The Yoneda lemma says that \[ F : \mathcal C \to \text{Set}^{C^{\text{op}}} \] \[ X \mapsto \text{Hom}(X, -) \] are fully and faithful functors. A nice consequence of this is that these functors reflect isomorphisms.

What we have proved is that there is an isomorphism \[ p: \text{Vect} \left( k \otimes V, - \right) \to \text{Vect} \left(V,\ - \right). \] More explicitly \[ p: F \left( k \otimes V \right) \to F (V). \] By the previous paragraph this is a full and faithful functor, thus it reflect to an isomorphism \[ b: k \otimes V \to V \] \[ F(b) = p \] which is a proof that \( k \otimes V \cong V \). \(\blacksquare\)

6. In the end

Notice how this proof did not rely on the explicit construction of tensor spaces. We did not use any identities on the dimensions either, as it is know that \[ \text{dim}(k) = 1,\ \text{dim}(k \otimes V) = \dim(k) \cdot \text{dim}(V) = \text{dim}(V) \] We just dealt with natural isomorphisms between functors and universal properties. It is a high-level view on how different mathematical object relate to each others without looking at the specific. In this sense, category theory does not give you new results, it gives you a new language (hopefully succinct) on how to express known results.

Footnotes:

1

This is confusing, a bi-linear function is not some kind of super-linear function. In fact it is a form of anti-linearity. Bi-linear functions are not linear on both variables at the same time.

Created: 2023-04-16 dom 00:16

Validate

Comentarios

Publicar un comentario

Entradas más populares de este blog

An apologia for lazy evaluation

An apologia of lazy evaluation As a programming language, laziness is the definitive feature of Haskell. Every other quality such as: higher order functions, Hindler-Milner type system or being lambda calculus based is present on other languages. In fact Haskell was born as a committee initiated language to avoid a proliferation of non-strict languages at the end of the 80's, putting all the effort before the same cart. If you take some time, and look at what HN , stack overflow or reddit has to say about the general sentiment of non Haskell programmer on laziness, it could be resumed on a single word: anxiety . It seems that space leaks due to laziness are unavoidable and that Haskell programmers choose to live with them. The methods of detecting them come from dynamic analysis of compiled programs . There is no general advice on how to avoid them apart from experience; an even then it not enough, as expert Haskell programmers still trip over them time to time. What hope do
Read more »

How to avoid correctness space leaks on a lazy setting in haskell

How to avoid space leaks on lazy setting How to avoid space leaks on lazy setting Table of Contents 1. A classification of space leaks 2. Avoiding strictness leaks 2.1. Repeatedly used functions over the same expressions 2.2. Using cost centres and one weird trick to catch them at run-time 3. Avoiding Liveness leaks 4. Avoiding excessive sharing leaks 4.1. Merge multiple passes over the data structure on a single pass 4.2. Move the creation of the generator inside the function and wrap it on a dumb function 4.3. Bite the bullet and use linear types 5. Conclusion Some posters on HN on made the observation that on my previous post I did not give general advice on how to avoid space leaks. This is specially important given that I ceded the point that exists a cluster (b) of space leaks that are of a correctness concern. The tools at our disposal come in two varieties: Defensive coding patterns Running program profiling I think the first
Read more »

Presenting data-forced, an alternative to bang patterns for long lived data structures

Presenting data-forced, an alternative to bang patterns for long lived data structures Table of Contents 1. The problem 2. The data-forced approach 3. UnliftedDatatypes have a different calling convention (CBV) 4. Conclusion As a consequence of my previous post , I crafted a new way to deal with liveness leaks : data-forced . It relies on CBV functions and tagging values when we know they have been evaluated. It is not complete, it is possible to be mis-used and not get any benefits, but it shows promise and gives stronger guarantees than the current status quo. Also, I am starting a new job next week, so I will have less time for hacking and writing. 1. The problem Long lived data structures that store thunks will keep the references needed to evaluate those thunks alive for a long time. This is a consequence of not pairing the denotation of the values with a good consumer. Current ways to deal with this on Haskell are: Use Bang patterns and/or se
Read more »