Similarly, the double cover $D$ of $S^1$ *is* B-finite in the truncated internal sense of “there (merely) exists a natural number $n$ and an isomorphism $[n]\cong D$”.

The double-cover of $S^1$ is definitely a covering space with finite fibres, but I don’t see which $n$ to take to get a surjection $n\to A$.

The cover of $S^1$ by two overlapping intervals has the property that over it the double cover of $S^1$ is locally (indeed globally) constant at $2$, which is what the characterization is asking for. I’m not sure what $n$ you are talking about.

The Möbius strip is not a free module in the external sense of there being a global section as basis element, but might it be different internally, that at the level of stalks it is free?

I think it depends on whether we formulate “$V$ is free” with a truncated $\exists$ or with an untruncated $\Sigma$. If “$V$ is free” means “there exists a set $S$ and a function $f:S\to V$ such that every $v\in V$ can be expressed uniquely as $v = r_1 f(s_1) + \cdots + r_n f(s_n)$” and “there exists” is truncated, then it allows passing to a cover, and the Mobius strip is free over the cover of $S^1$ by two overlapping intervals. But if it’s not truncated then we have to give a global $S$ and $f:S\to V$, and I don’t think that’s possible.

]]>The Möbius strip is not a free module in the external sense of there being a global section as basis element, but might it be different internally, that at the level of stalks it is free? I seem to remember a statement somewhere that Kaplansky’s theorem, that projective modules over local rings are free, carries over in some degree to some toposes like sheaves over a compact space; see this excerpt from Johnstone’s Topos Theory.

]]>The standard biased definition of vector space, in which you can add two elements and zero elements, is the correct one constructively as well. The unbiased version that this generates allows you to sum (Bishop-)finite families of elements.

That’s nice. Taking the strictest possible notion of “sets you are allowed to sum over” gives you the most general possible definition of vector space. I suppose this means that the construction of the free vector space on the set $A$ is given by the formal sums of B-finite subsets of $A$.

Actually that only works if the subset is decidable, otherwise you can’t define a function by cases to be “as given inside and 0 outside”. And a decidable subset of a finite set is still finite, so this doesn’t give you anything extra.

Ah yes, that makes sense. I worried a bit about that before I wrote it, but I managed to convince myself that it’s possible to define the complement (just pullback along the “false” map $1\to 2$ rather than the “true” one). But the problem isn’t that you can’t define the complement; it’s that you can’t prove every element is either in the original set or the complement.

I don’t offhand see a reason that every finitely-generated projective vector space would be free.

Yeah, that sounds false. My understanding is that for any topological space $X$ we can recover the category of vector bundles over $X$ as the category of vector spaces over the Dedekind reals inside the topos of sheaves on $X$. And a vector bundle is dualisable iff it’s locally finite-dimensional. So consider the “Möbius-strip” 1-dimensional real vector bundle over the circle. It’s not free, but it’s dualisable.

In fact I think this gives us an example of a set that isn’t B-finite, but whose free module is dualisable. Again working in the topos of sheaves of $S^1$, let $A$ be the sheaf of sections of the nontrivial double-cover of $S^1$. Then $A$ is K-finite but not B-finite. But the free module on $A$ is dualisable, because as a bundle it’s locally 2-dimensional.

(Actually I don’t quite understand this. The nLab says at finite object that

In the category of sheaves $\mathrm{Sh}(X)$ over a topological space, the decidable K-finite objects are those that are “locally finite;” i.e. there is an open cover of $X$ such that over each open in the cover, the sheaf is a locally constant function to $N$. These are essentially the same as covering spaces of $X$ with finite fibres.

but I don’t see how this works in the case of $A$. The double-cover of $S^1$ is definitely a covering space with finite fibres, but I don’t see which $n$ to take to get a surjection $n\to A$.)

]]>The tricky thing is that constructively, not every vector space is free (has a basis). In particular, a finitely-generated subspace of a vector space is not necessarily finite-dimensional in the sense of having a finite basis. If we apply the argument in #2 to the cone of finitely-generated subspaces of $V$, we conclude that every dualizable vector space is finitely generated. If we apply it instead to the cone of finite-dimensional vector spaces mapping *to* $V$ (not necessarily injectively), we conclude that $V$ is a retract of a finite-dimensional vector space, i.e. it is “finitely generated and projective”. Note that the latter is the correct abstract characterization of dualizable modules over general rings; constructively, vector spaces are often less different from modules over non-fields than they are classically.

I don’t offhand see a reason that every finitely-generated projective vector space would be free. And I also don’t see any reason for the free vector space on even a finitely-indexed set to be projective (finitely indexed sets are not necessarily projective). So I suspect that only finite sets can be shown constructively to have dualizable free vector spaces, though I don’t at the moment know how to prove it. If a finitely-generated projective vector space is free, is it necessarily finite-dimensional (free on a finite set)?

]]>The standard *biased* definition of vector space, in which you can add two elements and zero elements, is the correct one constructively as well. The unbiased version that this generates allows you to sum (Bishop-)finite families of elements.

Clearly if you allow sums over a set then you also allow sums over its subsets (since otherwise you could define the sum over that subset by summing over the original set a function that was 0 outside the subset).

Actually that only works if the subset is decidable, otherwise you can’t define a function by cases to be “as given inside and 0 outside”. And a decidable subset of a finite set is still finite, so this doesn’t give you anything extra.

I’m not actually sure offhand what sort of “finite” sets have dualizable free vector spaces constructively; it might be just finite ones, but sometimes this sort of “compactness” criterion gives you finitely indexed (K-finite) sets instead.

]]>I guess this is about free vector spaces on finite objects in toposes? If $n$ is a fibre of the generic natural number $\mathcal{N} \to \mathbb{N}$, then I believe the free vector space over the field $k$ on $n$ is just $k^n$. Otherwise there’s a bit more work (especially if, for instance, the topos doesn’t have an NNO - at which point $k$ would probably be a finite field, whatever that means)

]]>Thanks to Todd for his help and the answer.

Regarding the notion of *finite* from Oscar: given a natural number object $(N, +, 0)$ (= initial object in the category of internal algebras with a single nullary and a single unary and their homomorphisms) would calling an object $A$ *finite* if there exists a monomorphism from $A$ to $N$ but no isomorphism from $A$ to $N$ suffice?

(Moved this discussion from the ’Scrap paper’ category, which can only be seen when people are logged in, to a different category).

]]>While we’re here, I’ve been wondering about which definition of “finite” in a topos corresponds to dualisability. Which sets have dualisable free vector spaces?

After thinking about it for a bit I realised I didn’t even know the definition of “vector space”. I think of vector spaces as places where you can take arbitrary finite linear combinations. But this definition itself involves the word “finite”. So the generalisation to toposes isn’t immediately clear. Exactly which internal sets do we allow sums over? Clearly if you allow sums over a set then you also allow sums over its subsets (since otherwise you could *define* the sum over that subset by summing over the original set a function that was $0$ outside the subset). But except for that I have absolutely no intuition for which the correct definition is. Is there a standard choice?

A vector space $V$ is a directed colimit of the cone consisting of its finite-dimensional subspaces and inclusions between them (every element of $V$ is contained in a finite-dimensional subspace). If $V$ is dualizable, then $\hom(V, -) \cong V^\ast \otimes -$ and hence $\hom(V, -)$ is a left adjoint and thus preserves that directed colimit. But if the canonical map $\Gamma: colim_{f.d.\; subspace\; F_\alpha} \hom(V, F_\alpha) \to \hom(V, V)$ is an isomorphism, then there is some $\alpha: V \to F_\alpha$ that maps to $id_V$, i.e., $id_V: V \to V$ factors through a finite-dimensional subspace.

]]>I could not understand the proof of the fact that if a vector space $V$ over a field $k$ is dualisable in the monoidal category $\mathbf{Vect}_k$ then it should be finite dimensional. I understand that the image of $k$ under the unit is a $1$-dimensional subspace, but why should this imply the finite dimensionality of $V$? I would be thankful if someone could provide me the complete proof or a pointer to it.

With my regards,

partha

]]>