Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: recommendations

Topic: Linear algebra in Vect

Nathaniel Virgo (Apr 14 2020 at 12:06):

I know a reasonable amount of linear algebra (for finite spaces at least, with not-necessarily-Hermitian matrices), and I'd like to see how that knowledge relates to category theoretical concepts in Vect or FinVect. This is partly as a nice way to get a feel more of a feel for category-theoretical reasoning in general, and partly because I'm working on something that seems like it ought to end up as a category quite similar to Vect.

Does anyone know a kind of "gentle introduction to Vect" type of resource, showing how linear algebra concepts relate to category theoretic ones in that category? Or failing that, maybe an introductory text on category theory that assumes a linear algebra background and has lots of nice examples? Either way, huge bonus points if it uses string diagrams.

I'm currently confused about quite basic questions like "how do you think about scalars?" and "what should I really be imagining when I see wires bending around in Vect?", but ultimately it would be nice also to understand how to get at concepts like trace, determinant, eigenvectors etc. from a category theoretic perspective as well.

Philip Zucker (Apr 14 2020 at 14:14):

I think this is pretty good http://www.cs.ox.ac.uk/people/jamie.vicary/IntroductionToCategoricalQuantumMechanics.pdf

Nathaniel Virgo (Apr 15 2020 at 20:18):

It is pretty good, and I'm enjoying going through it, but there isn't very much about Vect in here, it's all Hilb. This is maybe not a massive issue - I guess the differences should mostly be clear - but in general I rarely work in Hilbert spaces and often work with non-symmetric matrices, so I'm still on the lookout for a good introduction to linear algebra in Vect specifically.

John Baez (Apr 15 2020 at 20:25):

I bet they're talking about FinHilb rather than Hilb - that is, the category of finite-dimensonal Hilbert spaces and linear maps.

John Baez (Apr 15 2020 at 20:26):

FinHilb is equivalent as a category to FinVect - that is, the category of finite-dimensional complex vector spaces and linear maps.

John Baez (Apr 15 2020 at 20:27):

The main thing FinHilb has that FinVect doesn't is the "dagger structure". So if you avoid using that (and its ilk) you might as well be in FinVect.

Nathaniel Virgo (Apr 15 2020 at 20:29):

That's useful to know!

Nathaniel Virgo (Apr 15 2020 at 20:39):

Though when it comes to eigendecomposition it should be a bit different, shouldn't it? (This book doesn't seem to cover eigenvectors, but it's one thing I'd like to understand from this perspective.) (Anyway I'll press on and ask specific questions when the need arises.)

Fabrizio Genovese (Apr 15 2020 at 20:41):

Yes, it's all finite dimensional

Fabrizio Genovese (Apr 15 2020 at 20:42):

Infinite dimensional hilbert spaces are a mess, mainly because it's not true anymore that you have a 1-1 correspondence between choices of bases and frobenius structures.

Fabrizio Genovese (Apr 15 2020 at 20:42):

Concretely, in Hilb the co-unit of a frobenius structure may not exist, since it's defined by using a sum that may be divergent

Fabrizio Genovese (Apr 15 2020 at 20:44):

We tried to circumvent this problem by considering Hilb* instead, that is, the category of non-standard Hilbert spaces. In this category there isn't a real difference between infinite and finite dimensional spaces: counits are divergent but "divergent" is just a non-standard natural number, which is nothing special in this framework. So you can pretty much do what you could do in finite dimensional Hilbert spaces.

John Baez (Apr 15 2020 at 21:16):

Nathaniel Virgo said:

Though when it comes to eigendecomposition it should be a bit different, shouldn't it? (This book doesn't seem to cover eigenvectors, but it's one thing I'd like to understand from this perspective.)

As far as eigenvectors go, a difference between FinHilb and FinVect is that only in FinHilb can we discuss the dagger $A^\dagger : K \to H$ of a linear map $A: H \to K$ so only in FinHilb can we can talk about "self-adjoint" and "unitary" operators. You can then show any self-adjoint or unitary operator has an orthonormal basis of eigenvectors... where the eigenvalues are real or of length 1, respectively.

In categorical quantum mechanics we capture the concept of an orthonormal basis using the concept of commutative dagger-Frobenius algebra, which is a concept that makes sense in any symmetric monoidal dagger-category.

But note, all these difference between FinHilb and FinVect arise because the former has a dagger structure: without that, the concepts of "self-adjoint" and "unitary" make no sense.

Todd Trimble (Apr 15 2020 at 21:33):

John Baez said:

The main thing FinHilb has that FinVect doesn't is the "dagger structure". So if you avoid using that (and its ilk) you might as well be in FinVect.

Perhaps this should be put more sharply? Since there is an equivalence between FinVect and FinHilb, the dagger structure on FinHilb could be transported across any such equivalence to a dagger structure on FinVect.

Might one say that the real issue is the essential nonuniqueness of such equivalences, so that there's no preferred (or canonical) way of putting a dagger structure on FinVect? Indeed, unless I'm confused, we should be able to "twist" a self-equivalence (like the identity functor on FinVect) by an automorphism on the ground field, like conjugation.

Fabrizio Genovese (Apr 15 2020 at 21:42):

Todd Trimble said:

John Baez said:

The main thing FinHilb has that FinVect doesn't is the "dagger structure". So if you avoid using that (and its ilk) you might as well be in FinVect.

Perhaps this should be put more sharply? Since there is an equivalence between FinVect and FinHilb, the dagger structure on FinHilb could be transported across any such equivalence to a dagger structure on FinVect.

Might one say that the real issue is the essential nonuniqueness of such equivalences, so that there's no preferred (or canonical) way of putting a dagger structure on FinVect? Indeed, unless I'm confused, we should be able to "twist" a self-equivalence (like the identity functor on FinVect) by an automorphism on the ground field, like conjugation.

This is true. Basically every time you have a semiring with an involution then the category S-Mat of free finite dimensional S-modules is dagger compact

Fabrizio Genovese (Apr 15 2020 at 21:43):

So if you work in complex FDVect you can just use the involution of the complex numbers to get your dagger (basically you are really working in C-Mat). This is not really a problem from the CQM perspective.

John Baez (Apr 15 2020 at 22:31):

Todd wrote:

Since there is an equivalence between FinVect and FinHilb, the dagger structure on FinHilb could be transported across any such equivalence to a dagger structure on FinVect.

Umm, I'm always nervous about statements like this...

John Baez (Apr 15 2020 at 22:33):

Just to point out a subtlety hiding in what Fabrizio said: if someone hands you FinVect (the category of finite-dimensional complex vector spaces and linear maps) and reminds you that C has an involution, that's not enough to canonically determine a dagger structure on FinVect.

John Baez (Apr 15 2020 at 22:35):

On the other hand if someone hands you FinVect and arbitrarily chooses a basis for every finite-dimensional complex vector space, that is enough to canonically determine a dagger structure on FinVect.

Fabrizio Genovese (Apr 15 2020 at 22:39):

John Baez said:

On the other hand if someone hands you FinVect and arbitrarily chooses a basis for every finite-dimensional complex vector space, that is enough to canonically determine a dagger structure on FinVect.

Yes, this is why I wrote "Basically you are working in C-Mat". What you say it is true, you need the involution and a basis. But you can always pick one, and C-Mat and C-FDVect are equivalent. To my knowledge, this is not considered harmful nor a dangerous thing to do in standard CQM practice.

Fabrizio Genovese (Apr 15 2020 at 22:43):

Basically the difference between Hilbert spaces and vector spaces doesn't seem to be a big problem in the finite dimensional cases. Mainly because their notion of basis coincides. But in the infinite dimensional case you can use the extra topological structure of Hilbert spaces to define a countable basis even in situations where the basis of the underlying vector space is uncountable (simply put you can trade a formal sum for a series). This is the point where things start breaking up and the reason why one has to be super-extra-careful in doing CQM in Hilb

John Baez (Apr 15 2020 at 22:46):

Right... that "basically" is the lurking danger I was talking about. C-Mat and C-FinVect are equivalent, but not isomorphic, etc.

All the people I have admired since childhood try to avoid basis-dependent constructions in quantum mechanics, and you certainly don't need a choice of basis to define the dagger of an operator, you just need an inner product, so I prefer to talk about the dagger structure in FinHilb without first choosing a basis for every finite-dimensional vector space.

Fabrizio Genovese (Apr 15 2020 at 22:50):

That makes sense. I guess our crowd was at ease with the C-Mat thing because many people in the group work on actively implementing this stuff. So in a way or another they'll need to pick a basis at some point :P

John Baez (Apr 15 2020 at 22:51):

Yes, those annoyingly practical people who actually multiply matrices - I've heard of them. :upside_down:

Fabrizio Genovese (Apr 15 2020 at 22:54):

Unfortunately it's more the annoying computers that require the people to do so... In any case I hate calculations too, and increadibly enough, even if I do math for a living I still have a _hard_ time in getting the right result while performing even simple arithmetic calculations T_T

Todd Trimble (Apr 15 2020 at 23:16):

John Baez said:

Todd wrote:

Since there is an equivalence between FinVect and FinHilb, the dagger structure on FinHilb could be transported across any such equivalence to a dagger structure on FinVect.

Umm, I'm always nervous about statements like this...

Oh, I see the problem: you want $\dagger$ to be the identity on objects, etc. It's that "evilness" (I suppose that word is safe around here, isn't it?) that gets in the way of such a straightforward transport.

I still wonder if the problem is that insurmountable... but I'd have to think about it.

John Baez (Apr 15 2020 at 23:21):

Mike Shulman has a comment on the nLab page about the evilness of dagger structures, which I still haven't taken the time to understand.

John Baez (Apr 15 2020 at 23:23):

Actually, I believe that a †-structure on a category can be transported along an equivalence of categories! [etc.]

https://ncatlab.org/nlab/show/principle+of+equivalence#daggers

Todd Trimble (Apr 15 2020 at 23:29):

John Baez said:

Mike Shulman has a comment on the nLab page about the evilness of dagger structures, which I still haven't taken the time to understand.

I mean, the first stupid idea that comes to mind is simply to use a global axiom of choice (in whatever suitable set theory, maybe Morse-Kelley or something) to choose a basis for every object in FinVect, and do the obvious thing. I'm sure others have thought about this, but I'm not sure what could go wrong here.

Edit: Just glanced at Mike's comment. Without having worked through details, I half-believe it (and if it works, it would be a more elegant way to go).

John Baez (Apr 15 2020 at 23:46):

Todd Trimble said:

I mean, the first stupid idea that comes to mind is simply to use a global axiom of choice (in whatever suitable set theory, maybe Morse-Kelley or something) to choose a basis for every object in FinVect, and do the obvious thing. I'm sure others have thought about this, but I'm not sure what could go wrong here.

If you do that, you thus give every finite-dimensional vector space a Hilbert space structure, so you give FinVect a dagger structure. But if this is what you're doing, you might as well just give every finite-dimensional vector space an inner product!

Todd Trimble (Apr 15 2020 at 23:54):

John Baez said:

Todd Trimble said:

I mean, the first stupid idea that comes to mind is simply to use a global axiom of choice (in whatever suitable set theory, maybe Morse-Kelley or something) to choose a basis for every object in FinVect, and do the obvious thing. I'm sure others have thought about this, but I'm not sure what could go wrong here.

If you do that you give every finite-dimensional vector space a Hilbert space structure so you give FinVect a dagger structure. But if this is what you're doing, you might as well just give every finite-dimensional vector space an inner product!

Well, yeah! So?

There seems to be a pretty good discussion over at MathOverflow, where it seems to be universally accepted that you can put a $\dagger$ structure on FinVect, but that there's still a live question about whether the evilness of the notion can be overcome. The answer by Peter LeFanu Lumsdaine (linked above) is too long to give here, but where a key phrase "so strict dagger structure is non-evil as a structure on “cats with a distinguished all-objects subgroupoid” " appears.

John Baez (Apr 15 2020 at 23:59):

where it seems to be universally accepted that you can put a † structure on FinVect

It darn well better be universally accepted - you just explained how to do it by picking a basis for it, and I just explained that it's enough to pick an inner product.

John Baez (Apr 16 2020 at 00:01):

Well, yeah! So?

That's a hard question to answer. But if we're gonna make FinVect become a dagger-category like FinHilb, it seems the most "honest" way is to make every finite-dimensional vector space into a Hilbert space.

Todd Trimble (Apr 16 2020 at 00:02):

John Baez said:

where it seems to be universally accepted that you can put a † structure on FinVect

It darn well better be universally accepted - you just explained how to do it by picking a basis for it, and I just explained that it's enough to pick an inner product.

Yes, that was my thought too where I said "do the obvious thing", which meant "make that an orthonormal basis".

Of course, I see now that the same point had been made above, more than once.

But while I'm yapping away, I'll riff on my automorphism comment above. If you start with $\mathbb{C}$ as a one-object category enriched in Ab, then any self-equivalence on $\mathbb{C}$ (which is the same as an automorphism on $\mathbb{C}$) automatically extends to a self-equivalence on its (enriched) Cauchy completion, which is $Mat_{\mathbb{C}}$. Conversely, that's where every self-equivalence on $Mat_{\mathbb{C}}$ must come from.

Nathaniel Virgo (Apr 17 2020 at 08:08):

Hi, sorry for another dumb question, but it seems worth having some intuition for this early on: are the $\mathbb{R}$ versions of these things much different from the $\mathbb{C}$ ones? The things I work on tend to involve real-valued asymmetric matrices, so I'm interested to know how much of the theory of those has been worked out.

E.g. could one state and prove the Perron-Frobenius theorem using categorical / string diagram language, or the result that an eigenvalue of a real matrix is either real or part of a complex pair? And where could I go to read about that kind of thing?

(Not that I need these things right now, I'm just curious how much of it has been done.)

Fabrizio Genovese (Apr 17 2020 at 09:34):

The main difference between RFDVect e CFDVect is that in the first case the dagger structure is trivial, since every real number is its own adjoint. All the string-diagrammatic reasoning you can do (spider fusion etc) still holds.

Fabrizio Genovese (Apr 17 2020 at 09:34):

"[...]or the result that an eigenvalue of a real matrix is either real or part of a complex pair?" This seems difficult to me. The thing is that I wouldn't know how to get the complex numbers in a setting like this

John Baez (Apr 18 2020 at 03:04):

Nathaniel Virgo said:

E.g. could one state and prove the Perron-Frobenius theorem using categorical / string diagram language, or the result that an eigenvalue of a real matrix is either real or part of a complex pair? And where could I go to read about that kind of thing?

I've never seen anyone try to state or prove the Perron-Frobenius theorem using categories or string diagrams. I think of this as a result that crucially uses the real numbers and the concept of positivity. You could try to prove it for any "real closed field" or more generally any field with a concept of positive elements as Fong and I defined it... I'm more sanguine about the first than the second here... but anyway: you've taken two concepts (string diagrams and Perron-Frobenius) that I like but have never tried to blend, and you're trying to blend them!

Martti Karvonen (Apr 22 2020 at 18:26):

On dagger structures on $\mathbf{FVect}$: as noted above, $\mathbf{FVect}$ can be equipped with a dagger structure (using global AC) - the problem is that this can't be done in a way that makes the forgetful functor $\mathbf{FHilb}\to \mathbf{FVect}$ into a dagger functor. The argument I learned from Selinger goes as follows: equip the same vector space $V$ with two different inner products, and consider the map $v\mapsto v$ between them in $\mathbf{FHilb}$. This is by construction not unitary, but applying the forgetful functor to it results in the identity on $V$, which is unitary for every dagger structure on $\mathbf{FVect}$.

John Baez (Apr 22 2020 at 18:27):

That's a nice "no-go theorem".

Martti Karvonen (Apr 22 2020 at 18:35):

This doesn't mean that the task of promoting equivalences into dagger equivalences is hopeless, as there's positive results in that direction. In general, one can promote an equivalence between (the underlying category of) a dagger category and a category into a dagger equivalence assuming that the structure iso on the dagger side is unitary and the other one maps to a unitary iso in already existing dagger category (and this is clearly necessary). In case of an adjoint equivalence, it is enough to check that the structure iso on the dagger side is already unitary. So in a sense, the problem is with the forgetful functor: there's no way to choose an inverse for it such that the composite is unitarily isomorphic to id on FHilb. One could also replace the forgetful functor (also using AC, so not in a canonical/explicit manner) with a naturally isomorphic one and get a full dagger equivalence between FHilb and FVect, but there's something messy/non-explicit going on either way.

Chris Barrett (Jun 22 2020 at 17:48):

Fabrizio Genovese said:

Concretely, in Hilb the co-unit of a frobenius structure may not exist, since it's defined by using a sum that may be divergent

I'm really curious about the problem(s) with lifting CQM to infinite dimensions. Is this the main problem? Perhaps another potential problem: loops in the string diagrams can be divergent. The co-multiplication ("broadcasting") map of a Frobenius algebra looks like it would be bounded, but what about the multiplication map and what about the unit? And what about cups and caps in general: is Hilb even closed? I'm pretty sure its not compact closed, but is there any chance it is *-autonomous?

John Baez (Jun 22 2020 at 18:00):

I doubt Hilb is *-autonomous. What would the dualizing object be, if not the unit for the tensor product?

Cole Comfort (Jun 22 2020 at 18:26):

Chris Barrett said:

Fabrizio Genovese said:

Concretely, in Hilb the co-unit of a frobenius structure may not exist, since it's defined by using a sum that may be divergent

I'm really curious about the problem(s) with lifting CQM to infinite dimensions. Is this the main problem? Perhaps another potential problem: loops in the string diagrams can be divergent. The co-multiplication ("broadcasting") map of a Frobenius algebra looks like it would be bounded, but what about the multiplication map and what about the unit? And what about cups and caps in general: is Hilb even closed? I'm pretty sure its not compact closed, but is there any chance it is *-autonomous?

Some people coming from the CQM crowd have made attempts to extend the \dag-compact closed structure of FHilb to a larger category; however Hilb itself is not compact closed.
Because of this, there is kind of a cottage industry of finding toy models.

There are *-autonomous categories, that "feel kind of like Hilb" . For example in finiteness modules one has "infinite dimensional matrices" with some specific finiteness condition. And in another direction one also has Chu construction (where the chosen object is the tensor unit) which gives you a way to talk about adjoints (kind of).

On the other hand people have also tried to use nonstandard analysis instead of *-autonomous categories to tackle this problem, but none of these approaches are as elegant as plain old FHilb.

Fabrizio Genovese (Jun 22 2020 at 18:51):

I do agree. It's not really that all these things do not work, it's more that they feel somehow "ugly" for some reason

Fabrizio Genovese (Jun 22 2020 at 18:52):

We started the non-standard analysis stuff because we really didn't like the *-autonomous categories solution. We ended up having something that still didn't look slick and polished like we wanted to

Fabrizio Genovese (Jun 22 2020 at 18:52):

Stefano Gogioso told me that he's still working on it tho, so never say never :slight_smile:

Chris Barrett (Jun 22 2020 at 18:57):

Thanks for the responses. Is Hilb closed, and are the multiplication and unit morphisms bounded? Sorry for the basic questions, but my CT knowledge is far better than my functional analysis.

One of the reasons I'm asking is because I'm interested in lifting CQM to a logical setting, i.e. generalizing to *-autonomous categories. It seems in this setting one avoids some of the problems I listed in my original post. For example, cut-elimination guarantees no cycles and so no need to worry about divergence from this cause. I suspected this might be useful for the problem of infinite dimensional CQM, however if Hilb is not *-autonomous, then maybe not. If Hilb is closed, there might still be the possibility of an intuitionistic approach to the "problem".

@Fabrizio Genovese, out of interest, why didn't you like this approach?

Cole Comfort (Jun 22 2020 at 19:02):

Chris Barrett said:

Thanks for the responses. Is Hilb closed, and are the multiplication and unit morphisms bounded? Sorry for the basic questions, but my CT knowledge is far better than my functional analysis.

One of the reasons I'm asking is because I'm interested in lifting CQM to a logical setting, i.e. generalizing to *-autonomous categories. It seems in this setting one avoids some of the problems I listed in my original post. For example, cut-elimination guarantees no cycles and so no need to worry about divergence from this cause. I suspected this might be useful for the problem of infinite dimensional CQM, however if Hilb is not *-autonomous, then maybe not. If Hilb is closed, there might still be the possibility of an intuitionistic approach to the "problem".

Fabrizio Genovese, out of interest, why didn't you like this approach?

The biggest problem with doing CQM stuff in *-autonomous categories is that asking that asking for a dagger structure forces the tensor to be par, so there is not always a way to ask if a morphism is an isometry/unitary.

Chris Barrett (Jun 22 2020 at 19:03):

In https://arxiv.org/abs/1809.00275 they suggest that the correct way to generalize the dagger is to drop the requirement of identity-on-objects and take it to be more like the (-)* duality of *-autonomous categories, i.e. to switch tesnor and parr. No collapse necessary in this case

Fabrizio Genovese (Jun 22 2020 at 19:04):

If I'm not wrong unit morphisms weren't a problem, counit could be divergent instead. In any case there isn't a real reason why I didn't like it. I guess I just wanted to stay as far away from functional analysis as I could, and nonstandard analysis allowed us to treat everything like it was finite dimensional

Chris Barrett (Jun 22 2020 at 19:04):

Oh hang on, it turns out you're an author on that paper... which presumably means I must have read it wrong!

Fabrizio Genovese (Jun 22 2020 at 19:05):

It just seemed the right way to go if you prefer algebra over everything else :confused:

Cole Comfort (Jun 22 2020 at 19:19):

Chris Barrett said:

Oh hang on, it turns out you're an author on that paper... which presumably means I must have read it wrong!

The thing is that if you just have an involution F which is not the identity on all of the objects then you cant always compose F(f);f and f;F(f). You can't have both 1) tensor not be par and 2) that the involution is the identity on objects at the same time.

John Baez (Jun 22 2020 at 19:22):

Chris Barrett said:

Thanks for the responses. Is Hilb closed, and are the multiplication and unit morphisms bounded?

When we talk about Hilb we usually insist that the morphisms are bounded linear operators, because it's tricky to compose unbounded ones: in practice those are always partially defined, at best densely defined.

So for me Hilb means complex Hilbert spaces and bounded linear operators.

I don't know if Hilb is monoidal closed with respect to the usual tensor product of Hilbert spaces. I strongly doubt it. I've never heard anyone say it is, and people would love for something like that to be true.

Given Hilbert spaces $H$ and $H'$ how do we get a Hilbert space $[H,H']$, a candidate for the internal hom? The space of all bounded linear maps from $H$ to $H'$ is not a Hilbert space (except in the finite-dimensional case). So, we usually look at all bounded linear maps $T: H \to H'$ such that

$\mathrm{tr}(T^\dagger T) \lt \infty$

These are called Hilbert-Schmidt maps and they form a Hilbert space with

$\langle S, T \rangle = \mathrm{tr}(S^\dagger T)$

But the identity on $H$ is not a Hilbert-Schmidt map from $H$ to $H'$, so if we try to make Hilbert monoidal closed with $[H,H']$ being the space of Hilbert-Schmidt maps from $H$ to $H'$, I don't think that will work.

Chris Barrett (Jun 22 2020 at 19:24):

@Cole Comfort Right, I see. So you can drop the id-on-objects requirement, but that means that the usual way you'd define an isometry as dag(f);f = id doesn't work (is not well-typed), thus we can't (at least, in the naive way) talk about things we need to talk about to do QM.

Chris Barrett (Jun 22 2020 at 19:29):

@John Baez Thanks, that's really helpful!

Martti Karvonen (Jun 23 2020 at 17:53):

Hilbert spaces and bounded linear maps is enriched over Banach spaces and bounded linear maps (and if you take this pov, the underlying category of Hilb is then given by Hilbert spaces and non-expansive linear maps). The category of Banach spaces and bounded linear maps is monoidal closed (+ complete and cocomplete), but alas it doesn't quite solve the problem for Hilb.

Cole Comfort (Jun 24 2020 at 05:19):

Martti Karvonen said:

Hilbert spaces and bounded linear maps is enriched over Banach spaces and bounded linear maps (and if you take this pov, the underlying category of Hilb is then given by Hilbert spaces and non-expansive linear maps). The category of Banach spaces and bounded linear maps is monoidal closed (+ complete and cocomplete), but alas it doesn't quite solve the problem for Hilb.

So in particular Chu(Ban,I) is a *-autonomous category.

Oscar Cunningham (Jul 31 2020 at 16:12):

I'm reviving this thread to ask a question. I was thinking about the fact that the free vector space on $\mathbb N$ is not dualizable (a.k.a. compact), and I realised I didn't know how to prove this without choice. Is it consistent with $\sf{ZF }$ that $\mathbf{Vect}$ is compact closed?

Oscar Cunningham (Jul 31 2020 at 16:12):

I'm worried that this might be super obvious.

Cole Comfort (Jul 31 2020 at 16:18):

Oscar Cunningham said:

I'm reviving this thread to ask a question. I was thinking about the fact that the free vector space on $\mathbb N$ is not dualizable (a.k.a. compact), and I realised I didn't know how to prove this without choice. Is it consistent with $\sf{ZF }$ that $\mathbf{Vect}$ is compact closed?

Vect isn't compact closed, it is just monoidal closed

Oscar Cunningham (Jul 31 2020 at 16:51):

Yeah, but why?

Cole Comfort (Jul 31 2020 at 16:52):

Oh, I see the question now

Martti Karvonen (Jul 31 2020 at 17:01):

Where are you currently using choice? It seems to me that, writing $F$ for the free vector space functor, an iso (which doesn't require choice) $1+\mathbb{N}\cong\mathbb{N}$ gives an iso $F(1)\oplus F(\mathbb{N})\cong F(\mathbb{N})$, and I don't see where Lemma 3.64 in the Heunen-Vicary textbook uses choice either. This lemma states some properties of dimension as defined in terms of traces, and in particular implies that if $F(\mathbb{N})$ was dualizable, its dimension would be a scalar $x$ satisfying $x=x+1$, which is impossible. This doesn't rule out the possibility that some messy vector space without a basis might have a dual, but seems to say that all of Vect can't be compact closed even if you omit choice.

Oscar Cunningham (Jul 31 2020 at 17:15):

Ah yes, that works. Thank you!

Oscar Cunningham (Jul 31 2020 at 17:16):

I had been trying to show that it wasn't isomorphic to its double dual. Considering the (internal) dimension is much easier.

Martti Karvonen (Jul 31 2020 at 17:33):

Yeah afaik dual spaces (and double dual spaces) can behave very weirdly without AC.

Todd Trimble (Aug 14 2020 at 15:08):

Long time since I visited here; only just saw this question.

Suppose $V$ is a vector space with a monoidal dual, $V \dashv V^\ast$ (treating a monoidal category as a bicategory). Then both $\hom(V, -)$ and $V^\ast \otimes -$ are right adjoint to $V \otimes -$, hence $\hom(V, -) \cong V^\ast \otimes -$ and $\hom(V, -)$ therefore preserves colimits. In particular it preserves the colimit over the directed system of finite-dimensional subspaces $V_\alpha \subseteq V$ and inclusions between them. In other words, $\hom(V, V)$ is the directed colimit of the system of $\hom(V, V_\alpha)$, and therefore the identity element $1_V \in \hom(V, V)$ is in the image of some $\phi \in \hom(V, V_\alpha)$. That is to say, $1_V$ is of the form $V \to V_\alpha \subseteq V$ for some finite-dimensional $V_\alpha$. Conclude that $V$ is finite-dimensional.